Critical Orange Checks in Polyspace Code Prover

Code Prover exhaustively checks your code for certain types of run-time errors. If a check is inconclusive, the result is displayed in orange (with a question mark). With each orange check, the analysis provides additional information that can help determine whether the check represents a possible run-time error or the result of an overapproximation or a broad assumption.

List of critical orange checks in Code Prover.

If a check is more likely to be a run-time error, it is considered as a critical orange check. Note that red and gray checks fall under the purview of critical checks by definition, since a red check indicates a definite run-time error and a gray check indicates code that is definitely unreachable (under the current verification assumptions). There is typically no question of determining likelihood when reviewing errors denoted with red and gray checks. With orange checks, critical checks help to focus review on results that are more likely to be run-time errors.

How to See Only Critical Checks

You can reduce the list of Code Prover results to only red, gray and critical orange checks.

Polyspace Desktop User Interface

In the user interface of the Polyspace^® desktop products, you can directly focus the list of results to critical checks only. On the Results List pane, from the All results dropdown, select Critical checks.

Dropdown showing critical checks

Selecting Critical checks retains only red, gray and critical orange checks on the Results List pane.

Polyspace Access Web Interface and Polyspace Platform User Interface

In the Polyspace Access™ web interface and the Polyspace Platform user interface, you can use separate filters for red, gray and critical orange checks:

Display only red, gray and orange checks using the color-based filters.
Display only critical orange checks using the text-based filters. In the Show only text filter, enter Origin: Path related issue to see path-related orange checks and Origin: Bounded inputs to see orange checks related to bounded inputs.

Which Orange Checks Are Considered Critical

The notion of critical checks allows you to prioritize your review of orange checks. You can choose to review the critical orange checks before other orange checks, or review only the critical orange checks. See also Managing Orange Checks in Polyspace Code Prover.

The critical orange checks are related to path and bounded input values. Here, input values refer to values that are external to the application. Examples include:

Inputs to functions called by generated main. For more information on functions called by generated main, see Functions to call (-main-generator-calls).
Global and volatile variables.
Data returned by a stubbed function. The data can be the value returned by the function or a function parameter modified through a pointer.

Note that there might be orange checks where the software cannot determine whether the check is path-related or input-related. Therefore, a safer approach might be to review critical checks before others but not confine the review to critical checks only.

Path

Checks that are path-related fall under the purview of critical orange checks. On the Results List pane, for these checks, the Information column contains the entry, Origin: Path related issue. These checks are critical because the software has identified distinct execution paths where a run-time error is likely to occur. The execution paths are distinct and separable from other paths that end up at the line with the check because they pass through different instructions in your code (another possibility would have been passing through the same instructions but for different inputs).

The following example shows a path-related orange check.

void path(int x) { 
   int result; 
   result = 1 / (x - 10); 
   // Orange division by zero
 } 

void main() { 
    path(1);
    path(10);
 }

The software identifies the orange Division by zero check as a potential error. The Result Details pane indicates the potential error:

...
Warning: scalar division by zero may occur
...

This Division by zero check on result=1/(x-10) is orange because:

path(1) does not cause a division by zero error.
path(10) causes a division by zero error.

Note that the orange check in this case represents a definite run-time error. Therefore, besides the path-related orange check, the analysis also indicates the error through a red Non-terminating call error on path(10).

Bounded Input Values

Checks that are related to bounded inputs fall under the purview of critical orange checks. On the Results List pane, for these checks, the Information column contains the entry, Origin: Bounded inputs. These checks are critical because the software has identified that a run-time error might occur for some program input that is externally bounded. Because the input values are explicitly bounded, the software did not need to make an assumption about the input. Therefore, the input values and the consequent run-time errors are likely to occur in practice.

Most input values can be bounded by external constraints (also known as Data Range Specifications or DRS). See also Inputs and Stubbing.

The following example shows an orange check related to bounded input values.

int tab[10]; 
extern int val; 
// You specify that val is in [5..10]
 
void assignElement(int index) { 
   int result; 
   result = tab[index];  
   // Orange Out of bounds array index
 } 
void main(void) {
   assignElement(val); 
}

If you specify a PERMANENT data range of 5 to 10 on the variable val, verification generates an orange Out of bounds array index check on tab[index]. The Result Details pane provides information about the potential error and states that the check might be related to bounded input values:

Warning: array index may be outside bounds: [0..9]
This check may be an issue related to bounded input values
Verifying DRS on extern variable val may remove this orange. 
  array size: 10 
  array index value: [5 .. 10]

Unbounded Input Values

Checks that are related to unbounded inputs do not fall under the purview of critical orange checks. On the Results List pane, for these checks, the Information column contains the entry, Origin: Possibly impacted by inputs. These checks are not considered critical because the software has identified that a run-time error might occur for some program input that is not bounded. Because the input values are not bounded, the software assumes a broad range of input values based on the input data types. The input values and the consequent run-time errors might not occur in practice.

The following example shows an orange check related to unbounded input values that might be identified as a potential run-time error:

int tab[10]; 
extern int val; 
 
void assignElement(int index) { 
   int result; 
   result = tab[index];  
   // Orange Out of bounds array index
 } 
void main(void) {
   assignElement(val); 
}

The verification generates an orange Out of bounds array index check on tab[index]. The Result Details pane provides information about the potential error and states that the check might be related to unbounded input values:

Warning: array index may be outside bounds: [0..9]
This check may be an issue related to unbounded input values
If appropriate, applying DRS to extern variable val may remove this orange. 
 array size: 10 
 array index value: [-2³¹ .. 2³¹-1]