Code Prover Analysis Following Red and Orange Checks

Polyspace^® considers that all execution paths that contain a run-time error terminate at the location of the error. For a given execution path, Polyspace highlights the first occurrence of a run-time error as a red or orange check and excludes that path from consideration. Therefore:

Following a red check, Polyspace does not analyze the remaining code in the same scope as the check.
Following an orange check, Polyspace analyzes the remaining code. But it considers only a reduced subset of execution paths that did not contain the run-time error. Therefore, if a green check occurs on an operation after an orange check, it means that the operation does not cause a run-time error only for this reduced set of execution paths.
Exceptions to this behavior can occur. For instance:
- For an orange overflow, if you specify warn-with-wrap-around or allow for Overflow mode for signed integer (-signed-integer-overflows) or Overflow mode for unsigned integer (-unsigned-integer-overflows), Polyspace wraps the result of an overflow and does not terminate the execution paths.
- For a subnormal float result, if you specify warn-all for Subnormal detection mode (-check-subnormal), Polyspace does not terminate the execution paths with subnormal results.
For more information on analysis options, see the documentation for Polyspace Code Prover™ or Polyspace Code Prover Server™.

The path containing a run-time error is terminated for the following reasons:

The state of the program is unknown following the error. For instance, following an Illegally dereferenced pointer error on an operation x=*ptr, the value of x is unknown.
You can review an error as early in your code as possible, because the first error on an execution path is shown in the verification results.
You do not have to review and then fix or justify the same result more than once. For instance, consider these statements, where the vertical ellipsis represents code in which the variable i is not modified.
```
x = arr[i];
.
.
y = arr[i];
```
If an orange Out of bounds array index check appears on x=arr[i], it means that i can be outside the array bounds. You do not want to review another orange check on y=arr[i] arising from the same cause.

Use these two rules to understand your checks. The following examples show how the two rules can result in checks that can be misleading when viewed out of context. Understand the examples below thoroughly to practice reviewing checks in context of the remaining code.

Code Following Red Check

The following example shows what happens after a red check:

void red(void)
{
int x;
x = 1 / x ;
x = x + 1;
}

When Polyspace verification reaches the division by x, x has not yet been initialized. Therefore, the software generates a red Non-initialized local variable check for x.

Execution paths beyond division by x are stopped. No checks are generated for the statement x = x + 1;.

Green Check Following Orange Check

The following example shows how a green check can result from a previous orange check. An orange check terminates execution paths that contain an error. A green check on an operation after an orange check means that the operation does not cause a run-time error only for the remaining execution paths.

extern int Read_An_Input(void);
void propagate(void)
{
	int x;
	int y[100];
	x = Read_An_Input();
	y[x] = 0;
	y[x] = 0;
}

In this function:

x is assigned the return value of Read_An_Input. After this assignment, the software estimates the range of x as [-2^31, 2^31-1].
The first y[x]=0; shows an Out of bounds array index error because x can have negative values.
After the first y[x]=0;, from the size of y, the software estimates x to be in the range [0,99].
The second y[x]=0; shows a green check because x lies in the range [0,99].

Gray Check Following Orange Check

The following example shows how a gray check can result from a previous orange check.

Consider the following example:

extern int read_an_input(void);

void main(void)
{
	int x;
	int y[100];
	x = read_an_input();
	y[x] = 0; 
	y[x-1] = (1 / x) + x ;
	if (x == 0)
		y[x] = 1;
}

From the gray check, you can trace backwards as follows:

The line y[x]=1; is unreachable.
Therefore, the test to assess whether x = 0 is always false.
The return value of read_an_input() is never equal to 0.

However, read_an_input can return any value in the full integer range, so this is not the correct explanation.

Instead, consider the execution path leading to the gray code:

The orange Out of bounds array index check on y[x]=0; means that subsequent lines deal with x in [0,99].
The orange Division by Zero check on the division by x means that x cannot be equal to 0 on the subsequent lines. Therefore, following that line, x is in [1,99].
Therefore, x is never equal to 0 in the if condition. Also, the array access through y[x-1] shows a green check.

Red Check Following Orange Check

The following example shows how a red error can reveal a bug which occurred on previous lines.

%% file1.c %% 

void f(int); 
int read_an_input(void); 

int main()  { 
    int x,old_x; 
    x = read_an_input();
    old_x = x; 
    if (x<0 || x>10) 
      return 1; 
    f(x); 
    x = 1 / old_x; 
    // Red Division by Zero
    return 0;    
}

%% file2.c %% 

#include <math.h> 

void f(int a) { 
    int tmp; 
    tmp = sqrt(0-a); 
}

A red check occurs on x=1/old_x; in file1.c because of the following sequence of steps during verification:

When x is assigned to old_x in file1.c, the verification assumes that x and old_x have the full range of an integer, that is [-2^31 , 2^31-1].
Following the if clause in file1.c, x is in [0,10]. Because x and old_x are equal, Polyspace considers that old_x is in [0,10] as well.
When x is passed to f in file1.c, the only possible value that x can have is 0. All other values lead to a run-time exception in file2.c, that is tmp = sqrt(0–a);.
A red error occurs on x=1/old_x; in file1.c because the software assumes old_x to be 0 as well.

Red Checks in Unreachable Code

Code Prover can sometimes show red checks in code that is supposed to be unreachable and gray. When propagating variable ranges, Code Prover sometimes makes approximations. In making these approximations, Code Prover might consider an otherwise unreachable branch as reachable. If an error appears in that unreachable branch, it is colored red.

Consider the statement:

if (test_var == 5) {
  // Code Section
}

If test_var does not have the value 5, the if branch is unreachable. If Code Prover makes an approximation because of which test_var acquires the value 5, the branch is now reachable and can show checks of other colors.

Use this figure to understand the effect of approximations. Because of approximations, a check color that is higher up can supersede the colors below. A check that should be red or green (indicating a definite error or definite absence of error) can become orange because a variable acquires extra values that cannot occur at run time. A check that should be gray can show red, green and orange checks because Code Prover considers an unreachable branch as reachable.

Documentation