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.

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 Color	Purpose	Example
Red	Highlights operations that are proven to cause a particular error on all execution paths`*`. Polyspace Code Prover verification determines errors with reference to the 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 Verification Assumptions and Check Behavior.	Red Overflow on: z = x+y; The operation `+` overflows for every value of `x` and `y` that the verification considers at that point.
Gray	Highlights unreachable code.	Gray Unreachable code check: if(x>0) {} else {} The `else` branch is unreachable for all values of `x` that the verification considers at that point.
Orange	Highlights operations that can cause an error on certain execution paths. For more information, see Orange Checks in Polyspace Code Prover.	Orange Overflow on: z = x+y; The analysis could not 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 at that point. You can use the tooltips on the variables `x` and `y` in the operation to see the range of values that the verification considers.
Green	Highlights operations that are proven to not cause a particular error on all execution paths`*`.	Green Overflow on: z = x+y; The operation `+` does not overflow for all values of `x` and `y` that the verification considers at that point.

* 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.

Result	Purpose	Icon
Coding rule violations	Indicates violation of predefined or custom coding rules.	for predefined rules and for custom rules.
Code metrics	Indicates code complexity metrics.	for metrics that do not exceed a limit you specified and for metrics that exceed a limit.
Global variables	Indicates global variable declaration.	for shared potentially unprotected variables and for non-shared unused variables

Source Code Colors

Polyspace uses the following color scheme for displaying code on the Source 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 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 runtime behavior).

Global Variable Colors

The Variable Access pane shows the global variables in your code along with the read and write operations on the variables.

For instance, used_global is a global variable that is accessed four times: once during initialization, once in the function function_with_red, and twice in the function function_with_grey.

The color scheme is as follows:

Variable colors:
- Orange: Shared, unprotected global variable (only applicable to multitasking code)
- Green: Shared, protected global variable (only applicable to multitasking code)
- Black: Unshared, used global variable
- Gray: Unshared, unused global variable
See Global Variables.
Operation colors: If an operation occurs in unreachable code, it is grey, otherwise black.
In the preceding example, one operation in the function function_with_grey is unreachable but the other is reachable.

For more information, see Variable Access in Polyspace Desktop User Interface.