Polyspace Client for C/C++

Introduction

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.

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

Polyspace Viewer, showing color-coding for each file, procedure, and line of C/C++ code.