Identify Root Causes of Code Prover Red or Orange Checks

Issue

After verification, Polyspace^® Code Prover™ highlights operations in your code with specific colors depending on whether the operation can cause a run-time error. See Code Prover Result and Source Code Colors.

It is not immediately clear why the verification highlights a specific operation in red (definite run-time error) or orange (potential run-time error). Even if you understand the cause of an error, it is not immediately clear where to fix it.

Possible Cause: Relation to Prior Code Operations

Often a run-time error in a specific operation is related to prior operations in your code.

For instance, an operation overflows because of a large operand value but the operand acquires that value in previous operations.

Solution

To investigate how a prior operation triggers a run-time error in the current operation, do the following:

View the message associated with the verification result on the current operation.
The message appears in the Result Details pane or in tooltips on the operation in the Source pane. The message shows you how to investigate the result further.
For instance, the message below shows that the right operand can be zero. To determine how the operand variable acquires the value zero, you have to browse through previous operations that write to the variable.
Browse prior operations in your code that are related to the current operation.
The Polyspace user interface provides features for easy navigation between specific points in your code. For instance, you can navigate from a function name to the function definition.

Identify a suitable place in your code where you can implement the fix.

For specific information on how to review each check type, see Reviewing Code Prover Run-Time Checks.

Possible Cause: Software Assumptions

If you do not provide your complete application or the external information required for verification, the software has to make certain assumptions about the missing code or external information.

For instance, if you do not provide a main function, the software generates a main that calls only the uncalled functions. If func1 calls func2, the generated main does not call func2 again. The verification checks for run-time errors in func2 only from the call context in func1.

The assumptions are such that they apply to most applications. However, in a few cases, the default assumptions might not describe your run-time environment accurately. If the assumptions are not what you expect, the verification results can be unexpected.

Solution

See if you can trace your verification result to a software assumption. For a partial list of assumptions, see Code Prover Analysis Assumptions. An additional list of assumptions is provided in codeprover_limitations.pdf in polyspaceroot\polyspace\verifier\code_prover_desktop.

Often, you can change the default assumptions using certain options.

Target and Compiler: See if you must set an option to emulate your compiler behavior.
For instance, if you want quotients of division operations to be rounded down instead of rounded up, use the option Division round down (-div-round-down).
Inputs and Stubbing: See if you have to externally constrain some variables.
For instance, if you want to constrain a global variable within a specific range, use the option Constraint setup (-data-range-specifications).
Multitasking: See if you forgot to specify some tasks or protection mechanisms.
For instance, if you want to specify that a function represents a nonpreemptable interrupt, use the option Interrupts (-interrupts).
Code Prover Verification: If you are verifying a module without a main, see if the generated main initializes your global variables and calls your functions in the right order.
For instance, if you want the generated main to call all your functions, use the option Functions to call (-main-generator-calls) with argument all.
Verification Assumptions: See if the global verification assumptions are appropriate for your run-time environment.
For instance, if you want the verification to consider that unknown pointers can be NULL-valued, use the option Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe).
Check Behavior: See if the run-time check specifications are appropriate for your run-time environment.
For instance, if you want the Illegally dereferenced pointer check to allow pointer arithmetic across fields of a structure, use the option Enable pointer arithmetic across fields (-allow-ptr-arith-on-struct).

If you still cannot understand your result, contact MathWorks^® Technical Support for help with interpreting your result. If you cannot share your actual verification results, provide only certain essential information about your result. See Contact Technical Support About Issues with Running Polyspace.