Find Relations Between Variables in Code

This tutorial shows how to determine if the variables in an arbitrary operation in your code are previously related.

For instance, consider this operation:

return(var1 - var2);

In your IDE, you can place breakpoints to stop execution and determine the values of var1 and var2 for a specific run.
In Polyspace^®, after you analyze your code, the tooltips on var1 and var2 show their range of values for all runs that the verification considers.

However, the range information is not enough to determine if the variables are related. You must perform additional steps to determine the relation.

Insert Pragma to Determine Variable Relation

In this example, consider the operation highlighted. You cannot tell from a quick glance if wheel_speed and wheel_speed_old are related. However, this information is crucial to understand a possible bug in subsequent operations.

#define MAX_SPEED 120
#define TEST_TIME 10000

int wheel_speed;
int wheel_speed_old;

int out;

int update_speed(int new_speed) {
    if(new_speed < MAX_SPEED)
	return new_speed;
    else
	return MAX_SPEED;
}

void increase_speed(void)
{
 
  int temp, index=1;

  while(index<TEST_TIME) {
    temp = wheel_speed - wheel_speed_old;
     
    if(index > 1) {
       if (temp < 0)
         out = 1;
       else
         out = 0;
    }
    
    wheel_speed_old = update_speed(wheel_speed);
    index++;
  }

}

To understand why you need the relation between wheel_speed and wheel_speed_old and how to find the relation:

Constrain the range of the variable wheel_speed to an initial value of 0..100 for the Polyspace analysis. Use the analysis option Constraint setup (-data-range-specifications).
Run analysis on this code and open the results. Select the gray Unreachable code check.
```
if (temp < 0)
         out = 1;
```
The check indicates that the variable temp is nonnegative. temp comes from the previous operation:
```
temp = wheel_speed - wheel_speed_old;
```
See the range of wheel_speed and wheel_speed_old. Place your cursor on these variables. You see these ranges:
- wheel_speed: 0..100
- wheel_speed_old: Full range of an int variable.
It is not clear from these ranges why wheel_speed - wheel_speed_old is always nonnegative. You have to find out if the variables are somehow related.
Insert a pragma before the line where you want the variable relation. Add the following line just before if(temp < 0):
```
#pragma Inspection_Point wheel_speed wheel_speed_old
```
Rerun the analysis and open the results. Place your cursor on wheel_speed_old in the line that you added.
The tooltip confirms that wheel_speed and wheel_speed_old are related:
```
wheel_speed_old <= wheel_speed
```
To find how the two variables got related, search for all instances of wheel_speed_old. On the Source pane, right-click wheel_speed_old and select Search For All References.
Browse through the instances. In this case, you see that the line which relates wheel_speed and wheel_speed_old is:
```
  wheel_speed_old = update_speed(wheel_speed);
```
This line ensures that after the first run of the while loop, wheel_speed_old is less than or equal to wheel_speed_old. The branch if(index > 1) is entered from the second run onwards. In this branch, the relation between wheel_speed and wheel_speed_old is reflected through the gray Unreachable code check.

Tip

Ignore the details of the relation shown in the tooltip. Use the tooltip to confirm if certain variables are related. Then, search for instances of the variable to find how they are related.

Further Exploration

You can use the pragma Inspection_Point to determine the relation between variables at any point in the code. You can enter as many variables as you want in the #pragma statement:

#pragma Inspection_Point var1 var2 ... varn

Try this technique on other examples. For instance, select Help > Examples > Code_Prover_Example.psprj. Group the results by file. In the file single_file_analysis.c, you see this code:

    if (output_v7 >= 0) {

      #pragma Inspection_Point output_v7 s8_ret
      saved_values[output_v7] = s8_ret;
      return s8_ret;
    }

If you place your cursor on s8_ret in the last two statements, you find that the ranges of s8_ret are different. Find out what changed between the two statements.

Hint: The tooltip in the #pragma statement indicates that the variable s8_ret is related to the variable output_v7. Note the orange check that reduces the range of output_v7.

Find Relations Between Variables in Code

Insert Pragma to Determine Variable Relation

Further Exploration

See Also

Topics