Main Content

Polyspace Bug Finder and Code Prover Documentation

Polyspace Bug Finder

Polyspace® Bug Finder™ identifies run-time errors, concurrency issues, security vulnerabilities, and other defects in C and C++ embedded software. Using static analysis, including semantic analysis, Polyspace Bug Finder analyzes software control, data flow, and interprocedural behavior. By highlighting defects as soon as they are detected, it lets you triage and fix bugs early in the development process.

Polyspace Bug Finder checks compliance with coding rule standards such as MISRA C®, MISRA C++, JSF++, CERT® C, CERT C++, and custom naming conventions. It generates reports consisting of bugs found, code-rule violations, and code quality metrics, including cyclomatic complexity. Polyspace Bug Finder can be used with the Eclipse™ IDE to analyze code on your desktop.

For automatically generated code, Polyspace results can be traced back to Simulink® models and dSPACE® TargetLink® blocks.

Support for industry standards is available through IEC Certification Kit (for ISO 26262 and IEC 61508) and DO Qualification Kit (for DO-178).

Full Bug Finder documentation

See all workflows, for instance:

  • Setting up analysis.

  • Reviewing results and generating reports.

Analysis options (Polyspace Bug Finder)

Look up options to configure before analysis, for instance:

  • Target & compiler options.

  • Defects to look for.

Results (Polyspace Bug Finder)

Look up results that you get from an analysis, for instance:

  • Defects.

  • Coding rules.

Release notes (Polyspace Bug Finder)

See what’s new for each release.

For desktop-specific workflows, see:

See also Choose Between Polyspace Bug Finder and Polyspace Code Prover.

Polyspace Code Prover

Polyspace Code Prover™ is a sound static analysis tool that proves the absence of overflow, divide-by-zero, out-of-bounds array access, and other run-time errors in C and C++ source code. It produces results without requiring program execution, code instrumentation, or test cases. Polyspace Code Prover uses semantic analysis and abstract interpretation based on formal methods to verify software interprocedural, control, and data flow behavior. You can use it to verify handwritten code, generated code, or a combination of the two. Each code statement is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven.

Polyspace Code Prover displays range information for variables and function return values, and can prove which variables exceed specified range limits. Code verification results can be used to track quality metrics and check conformance with your software quality objectives. Polyspace Code Prover can be used with the Eclipse IDE to verify code on your desktop.

Support for industry standards is available through IEC Certification Kit (for IEC 61508 and ISO 26262) and DO Qualification Kit (for DO-178).

Full Code Prover documentation

See all workflows, for instance:

  • Setting up analysis.

  • Reviewing results and generating reports.

Analysis options (Polyspace Code Prover)

Look up options to configure before analysis, for instance:

  • Target & compiler options.

  • Options related to verification assumptions.

Results (Polyspace Code Prover)

Look up results that you get from an analysis, for instance:

  • Run-time checks.

  • Global variable usage.

Release notes (Polyspace Code Prover)

See what’s new for each release.

For desktop-specific workflows, see:

See also Choose Between Polyspace Bug Finder and Polyspace Code Prover.

Polyspace Bug Finder Server

Polyspace Bug Finder Server™ is a static analysis engine that identifies common classes of bugs in C and C++, including run-time errors, concurrency issues, and other coding defects. Polyspace Bug Finder Server also checks source code for adherence to coding rules (MISRA C, MISRA C++, JSF++), security rules (CWE, CERT-C, CERT-C++, ISO/IEC 17961), and custom rules.

With Polyspace Bug Finder Server you can monitor code metrics including cyclomatic complexity, stack usage, and HIS metrics at the project, file, and function levels. You can configure the server for use with various compilers, target processors, and RTOS environments, and automate execution with continuous integration systems using tools such as Jenkins. Code analysis results can be published to Polyspace Bug Finder Access™ for triage and resolution.

Support for industry standards is available through IEC Certification Kit IEC Certification Kit (for IEC 61508 and ISO 26262) and DO Qualification Kit (for DO-178).

For server-specific workflows, see:

Polyspace Code Prover Server

Polyspace Code Prover Server is a sound static analysis engine that proves the absence of overflow, divide-by-zero, out-of-bounds, array access, and certain other run-time errors in C and C++ code. It performs interprocedural analysis of all possible control and data flows, including multi-threaded code, to identify each operation as always safe, always faulty, unreachable, or vulnerable. Polyspace Code Prover Server identifies code segments that are free of run-time errors, proven to fail, unreachable, or unproven.

Polyspace Code Prover Server can run on a server-class machine and can be integrated into build and continuous integration systems for automated verification using tools such as Jenkins. The analysis results can be published to Polyspace Code Prover Access for triage and resolution.

Support for industry standards is available through IEC Certification Kit (for IEC 61508 and ISO 26262) and DO Qualification Kit (for DO-178).

For server-specific workflows, see:

Polyspace Bug Finder Access

Polyspace Bug Finder Access provides a web browser interface for reviewing static code analysis results. It also provides Polyspace as You Code, a plug-in and analysis engine for performing static code analysis from within an integrated development environment (IDE) such as Visual Studio®, Visual Studio Code, or Eclipse.

The web browser interface lets you review, assign, and resolve code analysis results produced by Polyspace Bug Finder Server. The interface provides project dashboards displaying information that you can use to monitor software quality, project status, number of defects, and code metrics such as lines of code, cyclomatic complexity, and recursion. You can also use the web browser interface to create and assign tickets in defect-tracking systems such as Jira and Redmine.

Polyspace as You Code checks compliance with coding rule standards such as MISRA C, MISRA® C++, JSF++, CERT C, CERT C++, and custom naming conventions while you code. It enables you to identify critical defects and security vulnerabilities early in development and without leaving your IDE.

For web-browser-specific workflows, see:

For IDE-specific workflows, see:

Polyspace Code Prover Access

Polyspace Code Prover Access provides a web browser interface to Polyspace code verification results proving the absence of critical run-time errors in source code. It includes a central repository for analysis results that enables team-based collaboration. Results from Polyspace Code Prover Server can be published to Polyspace Code Prover Access for triage and resolution. With Polyspace Code Prover Access you can create and assign tickets in defect-tracking systems such as Jira.

Polyspace Code Prover Access dashboards display information that you can use to monitor software quality. The dashboards help you graphically track overall project status in terms of run-time errors and measure progress against Software Quality Objectives (SQO) thresholds.

For web-browser-specific workflows, see: