| Mathworks PolySpace |
|
PolySpace is a tool for analyzing C, C++, and Ada source code for semantic errors and ambiguities. Through use of a proven pseudo-dynamic analysis technique that is currently unique to PolySpace, this tool can actually prove and document the absence of certain classes of hard to find errors. PolySpace tests code for errors such as occur with pointer out-of-bounds, array out-of-bounds, and divide-by-zero using a technique known as abstract interpretation. The technique is very powerful, and while the analysis is guaranteed to catch every possibility of error in the class sought; false positives are somewhat common. Each is reported, and easily viewed in context using the viewer tool. False positives can be greatly reduced by use of configuration options and modeled stubs, and further reduced by adhering to certain programming practices. This last point makes it beneficial to integrate PolySpace into your development process as early in the coding as possible. Other features of PolySpace include limited lint-like abilities, and MISRA rule checking. It also generates complete control-flow and data-flow information.PolySpace has recently received certification under IEC-61508 for use in verification of safety-critical software. SafeCode, LLC proudly recommends PolySpace and can offer training, analysis, and assistance in the use of PolySpace; as well as helping you develop a strategy to integrate this powerful tool into your process. |
