I have some experience with a static (or quasi-dynamic) code-checker named PolySpace.
And since several requests have reached me to comment on the usefulness of PolySpace, sometimes in comparison with PC Lint, I decided to share some of my experiences with my (hopefully large) audience.

I used version 2.6 IIRC more than two years ago. However, the observations noted here were written down less than a year after that, and backed-up with a complete experience report written in parallel to my activities as a sort of diary. Memory lapses therefore unlikely.

I have made following observations on the deployment and use of PolySpace for embedded systems:

PolySpace starts its operation with a GNU-compiler run locally on the user's machine, and being far more picky than most compilers:
- Macro redefines (without #undef) are not allowed
- An unused macro parameter is not allowed
- Function call without parentheses is not allowed (this is a real error, resulting in a function pointer; however, some compilers just warn, and “do the right thing”, like the GreenHills compiler)
- a macro assert is not allowed, since this would redefine an ANSI macro/function
- Too many braces in struct-initializers are not allowed, i.e. int myArr[2] = { { 5, 1 } };
- Bit field unsigned long bf:32 is not allowed; just unsigned int bf:32; for widths less than 32 (long size?), no such limitation seems present
- Include filenames with a trailing space are not allowed, i.e. #include "abc.h "
- All prototypes must be available, correct and visible on use
- Inlining can be tedious, especially when inline is implicitly taken to mean static as with some compilers possible. Be aware: PolySpace warnings/errors in these cases are in no way always to the point and useful. In several cases it has proven necessary to dig quite deep into PolySpace innards and/or to refer to PolySpace support in order to understand why processing wasn’t successful
Several concepts are tedious to accommodate with PolySpace, and may lead to red errors (errors stopping the processing at that point)
- All variables must be initialized in a way recognizable for the GNU compiler
- Backward goto‘s must be instrumented with special PolySpace macros (changes in source code unavoidable!)
- Some forms of assembler need to be stubbed, since just disabling the assembly code may lead to a missing or empty function
- assert(false) or assert(0) is not allowed, not even in conditional code, and leads to red errors, stopping the processing of the rest of the function
- Functions known not to terminate must be conscientiously indicated
- All task entry points (in addition to main) must be indicated, as well as the ISR entry points
- Only functions with the prototype void <function>(void) are allowed as entry points for PolySpace
- Assignment of enum values to bit fields (even if the value range basically fits) can only be performed masked to the width of the bit field, even if the bit field has been declared with the enum-type as base
- If specific input conditions are implicitly assumed, and violation of those could/would lead to red/abort errors in PolySpace, these conditions must be made explicit by using assert
Aside from the long running times required (more than four days on ‘Software Safety Analysis level 2′ with ‘-O2′), the welcomed option “continue-with-red-errors”, which enables one to find multiple aborting errors in one PolySpace run, may cause spurious red errors also, and makes it tedious to find the source of a series of red errors
Deployment: If the client version and the server version differ even in minor parts of the version number, finding the cause of inevitable failures is very difficult, since the only clear-text error message is deposited in a cryptic log file normally ignored as part of the PolySpace noise
Deployment: PolySpace on Windows needs its own version of the Cygwin environment; one cannot install PolySpace without also installing Cygwin. Since it is problematic to have more than one Cygwin installation on one machine, other tools and environments cannot be used on the same machine. To my experience this includes the Standard Core development environment from BMW/3SOFT as well as the testing tool Tessy, among others. And since PolySpace will not run with a different version of Cygwin, this might limit its deployment options. Full runs on a (Linux?) server are possible only if and when the server has access to the original sources, through Samba, FTP, NFS, or whatever. Depending on the regular development environment, this may be tedious but possible.
Most important in my opinion: Mutual exclusion primitives must always appear in pairs within the same scope, like e.g. DI/EI. However, with an operating system like OSEK or VxWorks (or similar), sometimes constructs exist that do not appear in pairs (like ‘osSaveDisableGlobal’ only uses ‘DI’, whereas ‘osRestoreEnableGlobal’ only uses ‘EI’), or one has three primitives, two for setting and one for clearing (like ‘setLocal’ and ‘setGlobal’ vs. ‘clearAll’). Such combinations cannot be accommodated in PolySpace. The idea was to add extra (empty) macros for use as PolySpace guards. However, only code reviews could ascertain that such guards had only be placed at the appropriate code lines, and nowhere else. Recommendation even from PolySpace support (!!) was to concentrate on the code reviews, and refrain from implementing such primitives in the code to have PolySpace check the multitasking accesses. Thus, I have no experience with the problematic cases PolySpace would be able to find.

I have worked with PolySpace for some three months on a project with roughly estimated 50 kLOC C code (Counted semicolons outside of comments/strings, but fair enough). I cannot assume to have seen all potential road blocks using PolySpace, as I cannot assume that all described road blocks will prove relevant for your C code. Using PolySpace for C++ was outside my scope. Therefore, these observations are just that: observations.

And please be aware: This was version 2.6, PolySpace has not halted development, and it might very well be that some of the issues mentioned here have been resolved already.

And on the other hand, the things that PolySpace finds can be amazing: If a function creates a divide-by-zero runtime error when called with a parameter value of, say, 32, PolySpace will find that. It will find effectively unused code, even if the conditions are far from trivial, and many other things.
OK, Lint will find much for you. If your code is Lint-clean, and both PolySpace and Lint have been properly configured, PolySpace will find few (but probably serious) errors, if any. So, if you have the money, resources and time to use PolySpace, use both: Lint on a daily basis, available to all developers, with a clear message that code shall be clean before being checked-in. And well in advance of the next release, do a full PolySpace check, and take the warnings seriously.

Happy debugging!

March 5th, 2008