Code Prover Result and Source Code Colors
This topic explains the various colors used in displaying the results of a Polyspace® Code Prover™ analysis.
Polyspace displays the different verification results with specific icons and colors on the Results List and Result Details pane.
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.
Highlights operations that are proven to cause a particular error on
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;
Highlights unreachable code.
Gray Unreachable code check:
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
The most common reason is that the operation overflows only for some
Highlights operations that are proven to not cause a particular error on
Green Overflow on:
z = x+y;
* 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.
Besides checks for run-time errors, Polyspace Code Prover also displays other results about your code.
|Coding rule violations
|Indicates violation of predefined or custom coding rules.
|for predefined rules and for custom rules.
|Indicates code complexity metrics.
|for metrics that do not exceed a limit you specified and for metrics that exceed a limit.
|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.
forloop 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:
used_globalare initialized but the array
tabcan 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++.
||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
Uses dashed underlining for the keyword or identifier if it is not associated with a check.
This line has tooltips on
<, 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_redleads to a run-time error.
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
#ifdefstatements 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.
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
The color scheme is as follows:
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_greyis unreachable but the other is reachable.
For more information, see Variable Access in Polyspace Desktop User Interface.