Polyspace Code Prover™ uses the color orange to highlight operations that can't be automatically proven to be error free under all circumstances. You can then review potential run-time issues that might lead to robustness or reliability concerns.
For example, here we have an array with the size of 127, but the index can have values ranging from 0 to 555. This is highlighted orange because the operation can neither be proven safe under all possible run-time conditions (what if the index takes a value of 128?), nor is it proven to be an error for every run (what if the index is 10?). If you overlook such an operation, you might end up with unexpected software failure that is often difficult to reproduce and debug. Therefore, it is a robustness issue.
Array with the size of 127 highlighted orange.
So it is important to review the orange checks. Not only does it help identify run-time issues, but it is a useful artifact for code review discussions and unit testing efforts. Learn more about understanding the causes of orange checks.
Bar chart showing the code covered by verification.
However, before reviewing your verification results, you should pay attention to the Polyspace dashboard. It provides useful information to ensure that you have configured the analysis appropriately. It highlights how much of the code was analyzed; for example, if you incorrectly configure the main generator or the multitasking options, you might end up only analyzing small parts of the code.
Polyspace dashboard of check distribution.
In addition, look at the check distribution before reviewing the orange. Make sure to review the red and gray checks first. If more than 10% of the checks are orange, you should step back and look at whether the verification was set up with the right context. You can look at the top sources of the checks in the dashboard (as shown in the image below), and you can click on a particular source to see a filtered list of oranges. This can help address a collection of orange checks (for example, you could look at all checks that are caused by an unconstrained input or lack of verification context).
Orange sources bar chart.
Once you have looked at the Polyspace dashboard, here are couple of tips and best practices to consider when prioritizing the orange checks. Please refer to following documentation for more details on how to filter the critical orange checks.
- One of the categories that critical orange checks fall under are path related issues that can result in run-time errors. These are highlighted as a dark orange and are denoted by a mark. Address these first, as they are the most likely to cause software issues.
- After reviewing the dark orange checks, you should then review the critical orange checks that are caused by unconstrained inputs. This information is also highlighted in the dashboard as shown below. For more information on setting up constraints appropriately, refer to the documentation.
Dashboard showing constraint setup.
Learn more about reducing the overall number of orange checks by complying with coding guidelines and following other tips.
