Polyspace Client for C/C++0 pages
Polyspace Client for C/C++
Prove the absence of run-time errors in source code
Polyspace Client™ for C/C++ provides code verification that proves the absence of overflow, divide-by-zero,
out-of-bounds array access, and certain other run-time errors in source code using static code analysis that does
not require program execution, code instrumentation, or test cases. Polyspace Client for C/C++ uses formal
methods-based abstract interpretation techniques to verify code. You can use it on handwritten code, generated
code, or a combination of the two, before compilation and test.
Support for industry standards is available through IEC Certification Kit (for IEC 61508 and ISO 26262) and DO
Qualification Kit (for DO-178).
Key Features
■ File- and class-level software component verification
■ Formal methods-based abstract interpretation
■ Display of run-time errors directly in code
■ MISRA-C®:2004, MISRA-C++:2008, and JSF++ coding standard enforcement, with direct source file links
■ Cyclomatic complexity and other code metrics
■ Eclipse™ and Microsoft® Visual Studio® IDE integration
Green: reliable
static void pointer_arithmetic (void) {
int array[100];
int *p = array;
may be unsafe for some
conditions v
i - get bus status();
Purple: violation
MISRA-C/C++ or JSF++
code rules -----------------
if (i >= 0) (
■ME - iff- 10;
Range data
tool tip
Polyspace Viewer, showing color-coding for each file, procedure, and line of C/C+ + code.
^MathWorks-
Accelerating the pace of engineering and science
"