Test Orange Checks for Run-Time Errors

Note

The Automatic Orange Tester will be removed in a future release.

This example shows how to run dynamic tests on orange checks. An orange check means that Polyspace^® static verification detects a possible error but cannot prove it. Orange checks can occur because of:

Run-time errors.
Approximations that Polyspace made during static verification.

For more information, see Orange Checks in Code Prover.

By running tests, you can determine which orange checks represent run-time errors. Provided that you have emulated the run-time environment accurately, if a dynamic test fails, the orange check represents a run-time error. For this example, save the following code in a file test_orange.c:

volatile int r;
#include <stdio.h>

int input() {
 int k;
 k = r%21 - 10;
 // k  has value in [-10,10]
 return k;
}


void main() {
int x=input();
printf("%.2f",1.0/x); 
}

Run Tests for Full Range of Input

Note

The Automatic Orange Tester is not supported on Mac.

Create a Polyspace project. Add test_orange.c to your project.
In the project configuration, under Advanced Settings, select Automatic Orange Tester.
After verification, Polyspace generates additional source code that tests each orange check for run-time errors. The software compiles this instrumented code. When you run the automatic orange tester later, the software tests the resulting binary code.
Run a verification and open the results.
An orange Division by zero error appears on the operation 1.0/x.
Select Tools > Automatic Orange Tester.
In the Automatic Orange Tester window, click Start.
The Automatic Orange Tester runs tests on your code. If the tests take too long, use the Stop All button to stop the tests. Reduce Number of tests before running again.
After the tests are completed, under AOT Results, view the number of Tests that detected run-time errors.
The orange Division by zero check represents a run-time error, so you see test case failures.
On the Results tab, click the row describing the check.
A Test Case Detail window shows:
- The operation on which the tests were run.
- The test cases that failed with the reason for the failure.

Run Tests for Specified Range of Input

The Automatic Orange Tester window lists variables that cause orange checks. Because Polyspace does not have sufficient information about these variables, it makes assumptions about their range. If you know the variable range, you can specify it before running dynamic tests on orange checks. For pointer variables, you can specify the amount of memory written through the pointer. For instance, if the pointer points to an array, you can specify whether the first element of the array or the entire array is written through the pointer.

In the Automatic Orange Tester window, on the row describing r, click Advanced.
In the Edit Values window, under Variable Values, select Range of values.
Specify a minimum value of 1 and maximum of 9 for r. The Automatic Orange Tester saves the range as a .tgf file in the Polyspace-Instrumented folder in your results folder.
Click Start to restart tests on the orange Division by zero check for r in [1,9].
A division by zero cannot occur for r in [1,9], so there are no test failures. Although a test failure indicates a run-time error for specified inputs, because of the finite number of tests performed, the absence of test failures does not mean absence of a run-time error.
To prove that your range converts the orange check into a green check, you must provide the range during another static verification.
1. In the Automatic Orange Tester window, select File > Export Constraints.
2. Save your ranges as a text file.
3. Before running the next verification, on the Configuration pane, under Inputs & Stubbing, provide the text file for Constraint setup.
4. Run a verification and open your results.
  Instead of orange, there is a green Division by zero check on the operation 1.0/x.

Documentation