Variable Ranges in Source Code Tooltips After Code Prover Analysis

Polyspace^® Code Prover™ analyzes C/C++ code for run-time errors and reports the analysis results as checks on operations. The checks are colored green, red, or orange based on whether they pass, fail or remain inconclusive. In addition to the checks, the analysis also reports ranges on variables in tooltips throughout the source code. These range tooltips can support investigation of the reported run-time checks and also facilitate a deeper understanding of the code when used with other navigation tools in the Polyspace user interface or Polyspace Access™ web interface.

For instance, this tooltip on the variable beta indicates that the variable is a local variable, has data type float (on a target where float has 32 bits) and has a value in the range [0.1 .. 0.5]. The range combines values of beta from all possible execution paths that pass through that code operation.

Source Code panel showing tooltip for the beta variable.

Why Code Prover Reports Ranges on Variables

Code Prover analyzes each operation in the source code for all possible execution paths through the operation (subject to verification assumptions). When the analysis reports a range on an instance of a variable or an operation, the range combines values from all execution paths that lead to the variable or operation.

Consider the following example. When Code Prover analyzes the function func, the analysis reports variable ranges on almost all variables in the function. The code comments on each line show the variable ranges reported in a Code Prover analysis. Note that the ranges shown are the ones that occur after the operations on the line.

int func(unsigned int count) { // count is in [0 .. UINT_MAX]
    int var;
    if(count <= 5)
        var = count; //var is in [0..5]
    else
        var = 100;
    return var; //var is 100 or in [0..5]
}

For instance, you can see variable ranges in tooltips:

In the beginning of the function.
Suppose that func is not called elsewhere in the code. Based on the data type unsigned int, Code Prover assumes that count can have values in the range [0 .. 2³² - 1] or [0 .. UINT_MAX].
In each branch of a conditional statement.
An execution path can enter the if branch of the if-else statement only if count is less than or equal to 5. Therefore, inside the if block, count can have values only in the range [0 .. 5]. The variable var, which gets its value from the constrained count, also has the same constraint.
At the end, when the function returns.
In the return statement, var can have either the value [0 .. 5] from the if branch or the value 100 from the else branch. The tooltip on var in the return statement merges these two ranges and shows the range, 100 or [0 .. 5].

Using the tooltips on variable ranges, you can track the data flow in your code and understand how a variable acquires a value that could lead to a run-time error.

Why Variable Ranges Can Sometimes Be Narrower Than Expected

Sometimes, the range reported on a variable can be narrower than what you expect. A narrower-than-expected range can mean that two seemingly unrelated variables might be related from a previous operation.

Consider this example. The code comments on each line show the variable ranges reported in a Code Prover analysis at the end of the operations on the line.

void func(int arg) {

    int first, second, diff;
    first = arg;
    assert( first >= 0 && first <= 256*400); // first is in [0 .. 102400]
    second = (first << 4);  // second is in [0 .. 1638400]
    diff = (first * 16) -  (second + 256);  // diff is only -256
}

At first glance, the tooltip on diff in the last line might be surprising. The variable first is in the range [0..102400] and the variable second is in the range [0 ..1638400], but the difference diff has only one value, -256.

The reason for the single value of diff is that the previous operation:

second = (first << 4);

relates first and second in such a way that

first *
          16

is always equal to second, irrespective of the values of first and second. Therefore, they cancel each other on all execution paths, leading to a single value of diff.

If you see narrower-than-expected ranges in your code, look for previous operations that might relate two of the variables involved in the current operation. You can also enter the pragma Inspection_Point before an operation and then analyze the code to identify a relation between two of the variables in an operation. See Find Relations Between Variables in Code.