Polyspace Bug Finder and Code Prover Documentation

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^®++, 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 and integrated into build systems.

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

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.

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

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.

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.

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

Other Polyspace Products

Other Polyspace products include:

• Polyspace Products for Ada:

  Performs an analysis similar to Code Prover but on Ada code.

• Polyspace Bug Finder Server and Polyspace Code Prover Server:

  Allows incorporating Bug Finder and Code Prover in continuous integration with automated runs on server class machines.

• Polyspace Bug Finder Access and Polyspace Code Prover Access:

  Provides a common web interface for collaborative review of Bug Finder and Code Prover results within a team, project or organization.

You can view this documentation on the web or from the respective products.