Sources of Orange Checks

The Orange Sources pane shows unconstrained sources such as volatile variables and stubbed functions that can lead to multiple orange checks (unproven results) in a Code Prover analysis. If you constrain an orange source, you can address several orange checks together. To see the Orange Sources pane, click the button on the Result Details pane.

The sources essentially indicate variables whose values cannot be determined from your code. The variables can be inputs to functions whose call context is unknown or return values of undefined functions. Code Prover assumes that these variables take the full range of values allowed by their data type. This broad assumption can lead to one or more orange checks in the subsequent code.

For instance, in this example, if the function random_float is not defined, you see three orange Overflow checks.

static void Close_To_Zero(void)
{
    float xmin = random_float();
    float xmax = random_float();
    float y;

    if ((xmax - xmin) < 1.0E-37f) { /* Overflow 1 */
        y = 1.0f;
    } else {
        /* division by zero is impossible here */
        y = (xmax + xmin) / (xmax - xmin); /* Overflows 2 and 3 */
    }
}

The function random_float is therefore an orange source that causes at most three orange checks.

Using the Orange Sources pane, you can:

• Review all orange checks originating from the same source.

  In the preceding example, if you select the function random_float, the results list shows only the three orange checks caused by this source. See Filter Using Orange Sources.

• Constrain variable ranges by specifying external constraints or through additional code. Constraining the range of an orange source can remove several orange checks that come from overapproximation. The remaining orange checks indicate real issues in your code.

  In the preceding example, you can constrain the return value of random_float.

For efficient review, click the Max Oranges column header to sort the orange sources by number of orange checks that result from the source. Constrain the sources with more orange checks before tackling the others.

Constrain Orange Sources

How you constrain variable ranges and work around the default Polyspace^® assumptions depends on the type of orange source:

Stubbed function

If the definition of a function is not available to the Polyspace analysis, the function is stubbed. The analysis makes several assumptions about stubbed functions. For instance, the return value of a stubbed function can take any value allowed by its data type.

See Assumptions About Stubbed Functions for assumptions about stubbed functions and how to work around them.

Volatile variable

If a variable is declared with the volatile specifier, the analysis assumes that the variable can take any value allowed by its data type at any point in the code.

See Assumptions About Volatile Variables to work around around this assumption.

Extern variable

If a variable is declared with the extern specifier but not defined elsewhere in the code, the analysis assumes that the variable can take any value within its data type range before it is first assigned.

Determine where the variable is defined and why the definition is not available to the analysis. For instance, you might have omitted an include folder from the analysis.

Function called by the main generator

If your code does not contain a main function, a main function is generated for the analysis. By default, the generated main function calls uncalled functions with inputs that can take any value allowed by their data type.

See:

• Constrain Function Inputs to constrain the function inputs.

• Verify C Application Without main Function or Verify C++ Classes to change which functions are called by the generated main.

Variable initialized by the main generator

If your code does not contain a main function, a main function is generated for the analysis. By default, in each function called by the generated main, a global variable can take any value within its data type range before it is first assigned.

See Assumptions About Global Variable Initialization for how the generated main initializes global variables.

Variable set in a permanent range by the main generator

If you explicitly constrain a global variable to a specific range in the permanent mode, the analysis assumes that the variable can take any value within this range at any point in the code.

See External Constraints for Polyspace Analysis for more information on how a variable gets a permanent range. Check if you assigned a permanent range by mistake or your range must be narrower to reflect real-world values.

Absolute address

If a pointer is assigned an absolute address, the analysis assumes that the pointer dereference leads to a range of potential values determined by the pointer data type.

See Absolute address usage for examples of absolute address usage and corresponding Code Prover assumptions. To remove this assumption and flag all uses of absolute address, use the option -no-assumption-on-absolute-addresses.

Sometimes, more than one orange source can be responsible for an orange check. If you plug an orange source but do not see the expected disappearance of an orange check, consider if another source is also responsible for the check.

Related Topics

• Orange Checks in Code Prover
• Filter Using Orange Sources
• Reduce Orange Checks