Reduce Orange Checks in Polyspace Code Prover

An orange check indicates that Polyspace^® detects a possible run-time error but cannot prove it. To help Polyspace produce more proven results, you can:

Specify appropriate verification options.
Follow appropriate coding practices.

You can also limit the number and family of orange checks displayed on Results List. For more information, see:

You can take one or more of the following actions for orange check reduction.

Provide Context for Verification

This example shows how to provide additional information about run-time execution of your code. Sometimes, the code you provide does not contain this information. For instance:

You do not have a main function
You have a function that is declared but not defined.
You have function arguments whose values are available only at run-time.
You have concurrently running functions that are intended for execution in a specific sequence.

Without sufficient information, Polyspace Code Prover™ cannot verify the presence or absence of run-time errors.

Constrain Orange Sources

You can often address the bulk of orange checks by constraining relatively fewer number of orange sources.

In your verification results, you can see a list of sources such as volatile variables and stubbed functions that can cause multiple orange checks. To see this list, click the button on the Result Details pane. Constrain these sources so that you can remove most orange checks from overapproximation. In the longer term, instead of reacting to orange sources during review and constraining them for a later run, devise an efficient strategy for constraining likely orange sources during the first run itself.

See Sources of Orange Checks for types of orange sources and how to constrain them.

Commonly Used Context Specifications

To provide more context for verification and reduce orange checks, use these methods.

Method	Example
Define how the `main` generated by Polyspace initializes variables and calls functions	Code Prover Verification
Define ranges for global variables and function arguments.	Create Constraint Template from Code Prover Analysis Results
Define execution sequence for multitasking code.	Configuring Polyspace Multitasking Analysis Manually
Map an imprecisely analyzed function to a standard function for precise results at the function call sites.	`-code-behavior-specifications`

Improve Verification Precision

This example shows how to improve the precision of your verification. Increased precision reduces orange checks, but increases verification time.

Use the following options.

In the Polyspace user interface, the options appear on the Configuration pane under the Precision node.
In the Polyspace Platform user interface, the options appear on the Static Analysis tab under Run Time Errors > Precision.

Option	Purpose
`Precision level (-O0 \| -O1 \| -O2 \| -O3)`	Specify the verification algorithm.
`Verification level (-to)`	Specify the number of times the Polyspace verification process runs on your source code.
`Improve precision of interprocedural analysis (-path-sensitivity-delta)`	Propagate greater information about function arguments into the called function.
`Sensitivity context (-context-sensitivity)`	If a function contains a red and green check on the same instruction from two different calls, display both checks instead of an orange check.

Follow Coding Rules Using Polyspace Bug Finder

Using Polyspace Bug Finder™ to enforce coding rules can help Polyspace Code Prover prove the presence or absence of run-time errors. If your code follows certain subsets of MISRA™ coding rules, Polyspace can verify the presence or absence of run-time errors more easily.

Check whether your code follows the relevant subset of a MISRA coding rules. In the user interface of the Polyspace desktop products, on the Configuration pane, select one of the options in the Coding Standards & Code Metrics node.

Type of Code	Option for Enabling MISRA Coding Rules	How to Select a Subset
Handwritten C code	Check MISRA C:2012, Check MISRA C:2023	From the drop down menu, select `SQO-subset1` or `SQO-subset2`. For details about these subsets, Software Quality Objective Subsets for MISRA Coding Standards.
Generated C code	Check MISRA AC AGC	From the drop down menu, select `SQO-subset1` or `SQO-subset2`. .For details about these subsets, see Software Quality Objective Subsets (AC AGC)
Handwritten C++ code	Check MISRA C++:2008	From the drop down menu, select `SQO-subset1` or `SQO-subset2`. For details about these subsets, Software Quality Objective Subsets for MISRA Coding Standards.
Handwritten C++ code	Check MISRA C++:2023	To select software quality subset 1, select `mandatory-required`. To select software quality subset 2, select `all`.

In the Polyspace Platform user interface, you can select these options when using a custom checkers file. Open your project configuration and select Use custom checkers file on the Static Analysis tab under Defects and Coding Standards. Then select the icon to open the checkers selection window and choose the following options.

Type of Code	Option for Enabling MISRA Coding Rules	How to Select a Subset
Handwritten C code	Select MISRA C:2012 or MISRA C:2023 from the sidebar.	At the top of the window, select `SQO Level 1` or `SQO Level 2`. For details about these subsets, Software Quality Objective Subsets for MISRA Coding Standards.
Generated C code	MISRA AC AGC	At the top of the window, select `SQO Level 1` or `SQO Level 2`. For details about these subsets, see Software Quality Objective Subsets (AC AGC)
Handwritten C++ code	MISRA C++:2008	At the top of the window, select `SQO Level 1` or `SQO Level 2`. For details about these subsets, Software Quality Objective Subsets for MISRA Coding Standards.
Handwritten C++ code	MISRA C++:2023	At the top of the window, to select software quality subset 1, select `Mandatory` and `Required`. To select software quality subset 2, select `All`.

After selecting an appropriate software quality objective subsets, run a Polyspace Bug Finder analysis and review your results.
Fix the coding rule violations.

Reduce Application Size

Sometimes, the application size causes a loss of precision.

In a relatively smaller application, Code Prover retains more precise information about variable ranges. For instance, suppose a variable takes these values: {-2,-1,2,10,15,16,17}. If this variable is the denominator in a division, Code Prover shows a green Division by zero as long as it retains this precise information. If the application size grows beyond a certain point, to reduce computational complexity, Code Prover approximates this range to, for instance, {-2,2} U {10} U {15,17}. Now, if the variable is used for division, Code Prover shows an orange Division by zero.

To improve precision, you can divide the application into multiple modules. Verify each module independently of the other modules. You can review the complete results for one module, while the verification of the other modules are still running.

You can let the software modularize your application. The software divides your source files into multiple modules such that the interdependence between the modules is as little as possible. To begin, select Tools > Run Modularize. This option is not available in the Polyspace Platform user interface.
If you are running verification in the user interface, you can create multiple modules in your project and copy source files into those modules. This option is not available in the Polyspace Platform user interface.
You can perform a file-by-file verification. Each file constitutes a module by itself. See Verify files independently (-unit-by-unit).

Follow Verification Setup Suggestions

In some cases, Polyspace Code Prover can provide suggestions for better verification setup. At the end of each verification, Code Prover runs an advisor on the verification results. The advisor queries the results and looks for issues that can increase verification time and reduce precision. If the advisor can find issues (based on built-in rules), it suggests analysis options that can be used to work around the issues in future runs.

For instance:

If you are generating a main that calls too many functions already called elsewhere, you might see a suggestion to reduce the number of called functions.
If most orange checks are coming from global variables, you might see a suggestion to add constraints on those global variables.

You see these suggestions at the end of the verification log. The suggestions look like the following:

**********************************************************
***
*** Beginning Advisor
***
**********************************************************
Suggestion (polyspace.advisor.MainGeneratorCustomNeeded): 
 Issue: The generated main calls 54 functions, which might be too many and lead to loss of
        performance and precision.
 Cause: 49 functions are called both by the generated main and pointers to functions. These
        functions are not unused and need not be called by the generated main.
 Fix: Use -main-generator-calls custom=__bswap_16,__bswap_32,__bswap_64,apply_threshold,get_sum


**********************************************************
***
*** Advisor done
***
**********************************************************

If the fix suggestion mentions a Polyspace analysis option, you can copy the option and paste into your Polyspace options file. Even when the fix suggestions do not involve options that can be directly copied, you can use the suggestions as starting points for orange check reduction.