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 Limit Display of Orange Checks in Polyspace Platform User Interface.

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	Configure Library Verification
Define ranges for global variables and function arguments.	Find Variable to Constrain 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.

In the Polyspace Platform user interface, use the options that 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 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 for MISRA Coding Standards
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 objective subset 1, select `Mandatory` and `Required`. To select software quality objective 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.

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.