Code Prover Result and Source Code Colors

This topic explains the various colors used in displaying the results of a Polyspace® Code Prover™ analysis.

Result Colors

Polyspace displays the different verification results with specific icons and colors on the Results List and Result Details pane.

Results list showing icons and colors for red checks, gray checks, orange checks, and green checks

Run-Time Checks

Polyspace Code Prover checks each operation in your code for particular run-time errors. The software assigns a color to the operation based on whether it proved the existence or absence of a run-time error on all or some execution paths.

Check ColorPurposeExampleIcon

Red

Operation is proven to cause a particular error on all execution paths.

Polyspace Code Prover verification determines errors with reference to a language standard. Though some of the errors can be acceptable for a particular compilation environment, they violate the language standard. To allow some of the environment-dependent behavior, use appropriate analysis options. For more information, see Configuration.

Red Overflow check:

z = x + y;

The operation + overflows for every value of x and y that the verification considers.

Filled red circle
Gray

Code is unreachable.

Gray Unreachable code check:

if(x > 0)
{}
else
{}

For all values of x that the verification considers, the else branch is unreachable.

Gray X
Orange

Operation can cause an error on certain execution paths.

For more information, see Orange Checks in Polyspace Code Prover.

Orange Overflow check:

z = x + y;

The verification cannot prove whether the operation + overflows.

The most common reason is that the operation overflows only for some values of x and y that the verification considers. You can use the tooltips on the variables x and y to see the range of values that the verification considers.

Orange question mark
Dark orange

Operation is proven to cause a particular error on certain execution paths only.

Dark orange checks may appear when you use the option Sensitivity context (-context-sensitivity) to store call context information or the option Inline (-inline) to internally clone each function call. When you use one of these options, dark orange checks appear where the operation is red on at least one execution path, and is orange or green on at least one other execution path.

Dark orange checks are a type of orange check that you should review first because they could contain definite run-time errors in some contexts. Dark orange checks appear in the Results List when you use the Critical Checks filter in the Spotlight Filters section of the Review toolstrip.

Dark orange Division by zero check:

void func(int arg) {
    int loc_var = 0;
    loc_var = 1/arg;  
}

void main(void) {
    int num = 1;
    func(num + 10);
    func(num - 1);
}

The / operator appears dark orange because in the multiple calls to func, the second call results in a division-by-zero error.

Dark orange question mark
Green

Operation is proven not to cause a particular error on all execution paths.

Green Overflow check:

z = x + y;

For all values of x and y that the verification considers, the + operation does not overflow.

Green check mark

Note

For most checks, the software terminates an execution path following the first run-time error on the path. Therefore, if it proves a definite error (red) or absence of error (green) on an operation, the proof is valid only for the execution paths that have not yet been terminated at that point in the code. See Code Prover Analysis Following Red and Orange Checks.

Other Results

Besides checks for run-time errors, Polyspace Code Prover also displays other results about your code.

ResultPurposeIcon
Coding rule violationsIndicates violation of predefined or custom coding rules.Inverted purple triangle icon
Code metricsIndicates code complexity metrics.Blue star icon
Global variablesIndicates global variable declaration.Blue X with orange question mark icon for shared potentially unprotected variables and Blue X with gray X icon for non-shared unused variables

Source Code Colors

Polyspace uses the following color scheme for displaying code on the Source Code pane.

  • Lines with checks:

    For every check on the Results List pane, Polyspace assigns the check color to the corresponding section of code.

    • For lines containing macros, if the macro is collapsed, then Polyspace colors the entire line with the color of the most severe check on the line. The severity decreases in this order: red, gray, orange, green.

      This unreachable for loop contains a macro MAX_SIZE. The entire line is colored gray.

      If there is no check in a line containing a macro, Polyspace underlines the line in black when the macro is collapsed.

    • For all other lines, Polyspace colors only the keyword or identifier associated with the check.

      This assignment has three checks: i and used_global are initialized but the array tab can be accessed outside its bounds. The [ operator is colored orange to indicate the issue.

  • Lines with coding rule violations:

    For every coding rule violation on the Results List pane, Polyspace assigns to the corresponding keyword or identifier:

    • A (inverted triangle) symbol if the coding rule is a predefined rule. The predefined rules available are MISRA C™, MISRA™ AC AGC, MISRA C++, or JSF® C++.

      This if statement and || operation violates MISRA rules.

    • A symbol if the coding rule is a custom rule.

      This function name violates a custom naming convention.

  • Lines with tooltips:

    If a tooltip is available for a keyword or identifier on the Source Code pane, Polyspace:

    • Uses solid underlining for the keyword or identifier if it is associated with a check.

      This line has both checks and tooltips on input, % and used_global.

    • Uses dashed underlining for the keyword or identifier if it is not associated with a check.

      This line has tooltips on for and <, but no checks on them.

    • Uses dashed red underlining on function calls or loop commands to indicate that the function body or loop body contains a potential run-time error. The tooltip shows the line in the function or loop body that causes the error.

      This call to function_with_red leads to a run-time error.

  • Function definitions:

    When a function is defined, Polyspace colors the function name in blue.

  • Lines deactivated due to conditional compilation:

    Polyspace assigns a light gray color to code that is preprocessed out due to conditional compilation. Such code occurs, for instance, in #ifdef statements where the macro for a branch is not defined. This code does not affect the verification (or actual run-time behavior).

Global Variable Colors

The Global Variables Usage pane displays global variables and local static variables. For each global variable, the pane lists all functions and tasks performing read/write access on the variables, along with their attributes, such as values, read/write accesses and shared usage.

Open the Global Variables Usage pane by using the Global Variables icon icon in your Results Details pane, or by going to View > Global Variables Usage. Additionally, you can open the Global Variables Usage pane by selecting a global variable in the Source Code pane, right-clicking, and selecting Show Global Variable usage.

The color scheme is as follows:

  • Variable colors:

    • Black: global variable.

    • Orange: global variable, shared between tasks with no protection against concurrent access.

    • Green: global variable, shared between tasks and protected against concurrent access.

    • Gray: global variable, declared but not used in reachable code.

    See Global Variables.

  • Operation colors: If a task performs certain operations on a global variable, but the operations are in unreachable code, the tasks are colored gray.

For more information, see Global Variables Usage in Polyspace Platform User Interface.

See Also

Topics