Main Content

Orange Checks in Polyspace Code Prover

Polyspace® Code Prover™ checks each operation in your C/C++ code for certain run-time errors and displays the result as a red, green or orange check. For more information, see Code Prover Result and Source Code Colors. This topic describes orange checks in the results of a Polyspace Code Prover analysis.

When Orange Checks Occur

An orange check indicates that Polyspace detects a possible run-time error but cannot prove it. A check on an operation appears orange if both conditions are true:

First conditionSecond conditionExample
The operation occurs multiple times on an execution path or on multiple execution paths.During static verification, the operation fails only a fraction of times or only on a fraction of paths.

The operation occurs in:

  • A loop with more than one iterations.

  • A function that is called more than once.

The operation involves a variable that can take multiple values.During static verification, the operation fails only for a fraction of values.The operation involves a volatile variable.

During static verification, Polyspace can consider more execution paths than the execution paths that occur during run time. If an operation fails on a subset of paths, Polyspace cannot determine if that subset actually occurs during run time. Therefore, instead of a red check, it produces an orange check on the operation.

Orange Checks from Multiple Paths

Consider this example:

void main() {
  func(1);
  func(0);
}

double func(int value) {
  return (1.0/value); //Orange check
}

func is called twice with two arguments. Only one of the calls results in a division by zero in the body of func. Code Prover shows this result as an orange Division by zero check.

Orange Checks from Unknown Values

Consider this example:

double func(int value) {
  int reducedValue = value%21 - 10; // Result in [-10,10]
  return 1.0/reducedValue; //Orange check
}

If the call context of func is unknown, Code Prover assumes that its argument value can take any int value. As a result, reducedValue can take any value in [-10,10]. One of these values is zero, which causes a division by zero in func. Code Prover shows this result as an orange Division by zero check.

Unknown values and the subsequent broad Code Prover assumptions can occur because of the following reasons:

  • Function with no definition: Functions that are not defined can lead to unknown values.

    If a function definition is not available during analysis, a Code Prover analysis stubs the function. The analysis makes certain assumptions about the return value of the stubbed function and other side effects at the points where the function is called. See also Code Prover Assumptions About Stubbed Functions.

  • Function with no call context: Functions that are not called elsewhere in the analyzed code can lead to unknown values.

    If the analyzed program does not contain a main function, Code Prover generates a main. By default, the generated main calls otherwise uncalled functions with arguments that can have any possible value allowed by their data types. See also:

  • Global variables: Global variables can lead to unknown values when there is no main function.

    If the analyzed program does not contain a main function, Code Prover generates a main. By default, the generated main assumes at the beginning of each called function that global variables can have any possible value allowed by their data types. See also Code Prover Assumptions About Global Variable Initialization.

You typically see more orange checks when analyzing file by file, because each individual analysis unit containing a file (along with included headers) is unlikely to have a main function. Therefore, all assumptions required for a no-main analysis are triggered in this mode. For more information on file by file analysis, see Verify files independently (-unit-by-unit).

Why Review Orange Checks

Considering a superset of actual execution paths is a sound approximation because Polyspace does not lose information. If an operation contains a run-time error, Polyspace does not produce a green check on the operation. If Polyspace cannot prove the run-time error because of approximations, it produces an orange check. Therefore, you must review orange checks.

Examples of Polyspace approximations include:

  • Approximating the range of a variable at a certain point in the execution path. For instance, Polyspace can approximate the range {-1} U [0,10] of a float variable by [-1,10].

  • Approximating the interleaving of instructions in multitasking code. For instance, even if certain instructions in a pair of tasks cannot interrupt each other, Polyspace verification might not take that into account.

How to Review Orange Checks

To ensure that an operation does not fail during run time:

  1. Determine if the execution paths on which the operation fails can actually occur.

    For more information, see:

  2. If any of the execution paths can occur, fix the cause of the failure.

  3. If the execution paths cannot occur, enter a comment in your Polyspace result or source code, describing why they cannot occur. See:

    In a later verification, you can import these comments into your results. Then, if the orange check persists in the later verification, you do not have to review it again.

How to Reduce Orange Checks

Polyspace performs approximations because of one of the following.

  • Your code does not contain complete information about run-time execution. For example, your code is partially developed or contains variables whose values are known only at run time.

    If you want fewer orange checks, provide the information that Polyspace requires. For more information, see Provide Context for Verification.

  • Your code is very complex. For example, there can be multiple type conversions or multiple goto statements.

    If you want fewer orange checks, reduce the complexity of your code and follow recommended coding practices. For more information, see Follow Coding Rules Using Polyspace Bug Finder.

  • Polyspace must complete the verification in reasonable time and use reasonable computing resources.

    If you want fewer orange checks, improve the verification precision. But higher precision also increases verification time. For more information, see Improve Verification Precision.

Related Topics