Polyspace Code Prover performs code verification of C and C++ embedded software that must operate at the highest levels of quality, safety, and security. It is a sound static analysis tool that uses a formal methods technique called abstract interpretation to produce sound verification results. Polyspace Code Prover identifies where run-time errors may occur and code that is proven to be safe from run-time errors. You use Polyspace Code Prover as part of a high quality assurance process to exhaustively verify all possible combinations of inputs, paths, and variable values. Polyspace Code Prover uses color-coding to indicate the status of each element in the code. It integrates with Simulink® to offer traceability of code level run-time results back to the Simulink models.
With Polyspace Code Prover, you can:
You can access Polyspace Code Prover from the command line, graphical user interface, or via plugins to Visual Studio® and Eclipse™. You use it to support all critical activities in a software development workflow, including:
Polyspace Code Prover works with Polyspace Bug Finder to find safety-critical defects, such as divide by zero or security critical buffer overflows, in your source code and check compliance to coding standards such as MISRA. These products offer an end-to-end static analysis capability for early stage development use, spanning bug-finding, coding rules checking, and proof of run-time errors. This capability ensures the reliability of embedded software that must operate at the highest levels of quality and safety.
Polyspace Code Prover uses abstract interpretation with static code analysis to prove, identify, and diagnose run-time errors such as arithmetic overflows, divide by zero, and buffer overflows. This technique completely and comprehensively verifies all possible run-time conditions and automatically provides a diagnostic of proven, failed, unreachable, or unproven for each code operation. In the verification results produced by Polyspace Code Prover, each C or C++ operation is color-coded to indicate its status:
Green: proven free of run-time errors
Red: proven faulty each time the operation is executed
Gray: proven unreachable (may indicate a functional issue)
Orange: unproven operation may be faulty under certain conditions
Errors detected include:
Polyspace Code Prover tracks control and data flow through the software and displays range information associated with variables and operators. By placing your cursor over an operator or variable, a tooltip message displays the range information. The formal method known as abstract interpretation enables determination of accurate range information for the purpose of proving that the software is free of certain run-time errors such as divide by zeros and buffer overflows. You can use range information to track the control and data flow precisely to debug your software or to ensure that certain variables or operations do not violate specified range limits.
In the example below, Polyspace Code Prover has determined that the division operation consists of a range between -1701 to 3276 for the left operand; right operand is 9. The resulting range after division is -189 to 364.
You can further visualize the control flow using the call hierarchy and the call flow graphs or view the accesses for your global variable data
Explore gallery (3 images)
You can define a centralized quality model to track run-time errors, code complexity, and coding rules violations. Using these metrics you can track your progress toward predefined software quality objectives as your code evolves from the first iteration to the ultimate delivery version. By measuring the rate of improvement in code quality, Polyspace Code Prover enables developers, testers, and project managers to target and deliver high quality code.
You can use Polyspace Code Prover to verify generated code or mixed code which contains both generated and handwritten code. Code-level defect results in the automatically generated code are traced back to the model in Simulink. You can identify which parts of the model are reliable; and correct design problems that will cause errors in the code. You can also identify potential problems between the interface of generated and handwritten code. For example, the mixing of hand-written S-Function code with generated code could result in a problem where incorrect ranges of signals in the interface cause a run-time error.
Polyspace Code Prover also supports tracing run-time results to dSPACE® TargetLink® blocks and IBM Rational Rhapsody models.
You can use Polyspace Code Prover as part of a continuous integration process by incorporating Polyspace into your build process. You can automate verification job scheduling and set up email notifications. You can assign Polyspace Code Prover to schedule the posting of a verification job to a cluster computer (using MATLAB Distributed Computing Server), and receive email notifications when the results are available. Results contain the differences compared with the previous version of your code, which the server computes automatically.
You can define the frequency of these analyses, the quality model you want to apply for a given portion of your code base, and the emails you want your users to receive when the results are available. Also, you can define which characteristics of the build process you want the automated verifications to encompass.
You can use Polyspace Bug Finder and Polyspace Code Prover with IEC Certification Kit (for IEC 61508 and ISO 26262) and DO Qualification Kit (for DO-178B) in the certification process for projects based on these industry standards.
Reports and artifacts show the final quality of the code, highlight sections that have been reviewed, generate code metrics, and document the application of coding rules and run-time error status. You can create these reports in PDF, HTML, RTF, and other formats.