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