In short, it's a tool that predicts possible run-time errors in code without actually executing it. This provides an insight into the quality of the code and catches run-time issues in the early stages of development.
Two tools come under the brand name Polyspace. Polyspace Code Prover and Polyspace Bug Finder. Although the end goal for both tools is the same, they differ in their approach. It has been neatly summarized by the following excerpt from a Q&A post on the MathWorks website.
Bug Finder quickly analyzes your code and detects many types of defects. Code Prover checks every operation in your code for a set of possible run-time errors and tries to prove the absence of the error for all execution paths. For instance, for every division in your code, a Code Prover analysis tries to prove that the denominator cannot be zero. Bug Finder does not perform such exhaustive verification. For instance, Bug Finder also checks for a division by zero error, but it might not find all operations that can cause the error."
Although not that important, you can read more about it here. Differences Between Polyspace Bug Finder and Polyspace Code Prover - MATLAB & Simulink - MathWorks China
Detailed documentation of Code Prover and Bug Finder can be found here. Documentation
We will stick to only the Polyspace Code Prover tool for our purpose. MathWorks describes it as
Polyspace Code Prover™ proves the absence of overflow, divide-by-zero, out-of-bounds array access, and certain 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 static analysis and abstract interpretation based on formal methods. You can use it on handwritten code, generated code, or a combination of the two. Each operation is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven. Polyspace Code Prover also displays range information for variables and function return values, and can prove which variables exceed specified range limits. Results can be published to a dashboard to track quality metrics and ensure conformance with software quality objectives.
Check out more about Polyspace Code Prover here. Polyspace Code Prover - MATLAB & Simulink (Mathworks.cn) Find all the documentation and PDFs for Polyspace Code Prover here, Polyspace Code Prover Documentation - MathWorks China
There are different approaches to using Polyspace. It comes with its own GUI and also provides plugins for different IDEs like Eclipse. As a developer or someone responsible for ensuring code quality, you may encounter Polyspace results in formats supported by web browsers, Excel sheets or Word docs. It all depends on your CX pipelines. Nevertheless, what is important is fixing the issues reported by the tool.
On that note, here is an extensive list of all the checks performed by Polyspace Polyspace Results (Mathworks.cn) This includes all the checks done both by Bug Finder and Code Prover. Here is a more readable, categorized list of checks Complete List of Polyspace Code Prover Results - MATLAB & Simulink - MathWorks China
We will focus on only the checks performed by Code Prover and refer to it as Polyspace for convenience.
3 broad categories of checks are performed by Polyspace, Run-Time checks, Code Metrics checks and checks on Global variables. These are then divided into a class of checks like Data Flow Checks, Numerical Checks etc. These checks are the most common issues that one encounters in a codebase.
Here's the list of checks, as described by MathWorks. Open the link and see the description on the MathWorks website.
- Function not called
- Function not reachable
- Global variable not assigned a value in initialization code
- Non-initialized local variable
- Non-initialized pointer
- Non-initialized variable
- Return value not initialized
- Unreachable code
- Incorrect object oriented programming
- Invalid C++ specific operations
- Function not returning value
- Null this-pointer calling method
- Uncaught exception
- AUTOSAR runnable not implemented
- Correctness condition
- Invalid result of AUTOSAR runnable implementation
- Invalid use of AUTOSAR runtime environment function
- Invalid use of standard library routine
- Non-compliance with AUTOSAR specification
- User assertion
- Minimum Stack Usage
- Maximum Stack Usage
- Program Maximum Stack Usage
- Program Minimum Stack Usage
- Higher Estimate of Size of Local Variables
- Lower Estimate of Size of Local Variables
These checks provide valuable feedback on the quality of the source code. Fixing these can avoid pesky run-time errors that are hard to detect during the development lifecycle. Certain errors encountered in the wild can be hard to debug. Nipping them in the bud at this stage is the easy way forward.
Each reported error of Polyspace has a bunch of attributes. The actual output depends on how your Polyspace is configured. This is a list of all attributes that Polyspace can provide. Results List in Polyspace Desktop User Interface - MATLAB & Simulink - MathWorks China
This is how the results can be interpreted. Interpret Results - MATLAB & Simulink - MathWorks China
Errors are reported under this family of errors.
- Red: proven run-time error
- Orange: possible run-time error
- Green: proven absence of run-time errors
- Grey: unreachable code.
More on how to interpret these families of error. Code Prover Result and Source Code Colors - MATLAB & Simulink - MathWorks China
- The "Check" attribute.
- This attribute is the name of the check that has generated the error.
- This name can be found in the list of Polyspace checks listed in the previous section.
- Polyspace provides detailed explanations and steps to review and fix the errors.
- The "Detail" attribute.
- This provides additional information on the result.
- This works in conjugation with the check performed.
- If the check is Overflow, this attribute will tell you which operation caused that overflow.
Now that we know how to make sense of a Polyspace result. Let's see how to fix these errors. Here is a handy link (probably the most useful link in this whole document). This can help you understand an error and then provide steps to fix them. Code Prover Run-Time Checks - MATLAB & Simulink - MathWorks China
- Refer to the Check and Details attribute to figure out exactly what caused the error.
- Refer to the previous link for steps on fixing the error.
- Often, the error may not be on the line that has been reported. You may have to hunt down the root cause in the execution branches that lead up to the line.
- Look for other errors that can be related to the line that has the error.
- Superseding of check colors
- Polyspace uses approximations to predict the behavior. This can cause a check color to supersede other colors.
- A check that should have been either Red or Green can become Orange.
- Fixing this orange error can then reveal the presence of a definite run-time Red error or no error Green. This is an important behavior to know.
- Read more about it here. Code Prover Analysis Following Red and Orange Checks - MATLAB & Simulink - MathWorks China
- It is highly recommended to fix Orange errors, as they might be hiding a Red error underneath.
- A good approach could be to target the Red error first. If the Red error does not make sense, then target fixing the Orange errors in all the related execution paths.
Happy coding !!
Note: You need to create an account with the MathWorks website to access all the links. The registration is free.