Найдите отношения между переменными в коде

Этот пример показывает, как определить, связаны ли переменные в произвольной операции в вашем коде ранее.

Например, рассмотрите эту операцию:

return(var1 - var2);

В вашем IDE можно поместить точки останова, чтобы остановить выполнение и определить значения var1 и var2 для определенного выполнения.
В Polyspace^®, после того, как вы анализируете свой код, подсказки на var1 и var2 показывают свою область значений значений для всех выполнений, что верификация рассматривает.

Однако информации об области значений недостаточно, чтобы определить, связаны ли переменные. Необходимо выполнить дополнительные шаги, чтобы определить отношение.

Вставьте прагму, чтобы определить переменное отношение

В этом примере считайте операцию подсвеченной. Вы не можете сказать от быстрого взгляда, если wheel_speed и wheel_speed_old связаны. Однако эта информация крайне важна, чтобы понять возможную ошибку в последующих операциях.

#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++;
  }

}

Чтобы понять, почему вам нужно отношение между wheel_speed и wheel_speed_old и как найти отношение:

Ограничьте область значений переменной wheel_speed к 0.. 100 для анализа Polyspace. Используйте аналитическую опцию Constraint setup (-data-range-specifications).
Запустите анализ этого кода и откройте результаты. Выберите серую проверку Unreachable code.
```
if (temp < 0)
         out = 1;
```
Проверка указывает, что переменная temp является неотрицательной. temp прибывает из предыдущей операции:
```
temp = wheel_speed - wheel_speed_old;
```
Смотрите область значений wheel_speed и wheel_speed_old. Установите свой курсор на эти переменные. Вы видите эти области значений:
- wheel_speed: 0. 100
- wheel_speed_old: Полный спектр переменной int.
Не ясно из этих областей значений, почему wheel_speed - wheel_speed_old является всегда неотрицательным. Необходимо узнать, связаны ли переменные так или иначе.
Вставьте прагму перед строкой, где вы хотите переменное отношение. Добавьте следующую строку незадолго до if(temp < 0):
```
#pragma Inspection_Point wheel_speed wheel_speed_old
```
Повторно выполните анализ и откройте результаты. Установите свой курсор на wheel_speed_old в строке, которую вы добавили.
Подсказка подтверждает, что wheel_speed и wheel_speed_old связаны:
```
wheel_speed_old <= wheel_speed
```
Чтобы найти, как эти две переменные были связаны, ищите все экземпляры wheel_speed_old. На панели Source щелкните правой кнопкой по wheel_speed_old и выберите Search For All References.
Просмотрите экземпляры. В этом случае вы видите, что строка, которая связывает wheel_speed и wheel_speed_old:
```
  wheel_speed_old = update_speed(wheel_speed);
```
Эта строка гарантирует, что после первого показа цикла while, wheel_speed_old меньше чем или равен wheel_speed_old. Ответвление if(index > 1) вводится от второго выполнения вперед. В этом ответвлении, отношении между wheel_speed и wheel_speed_old отражается посредством серой проверки Unreachable code.

Совет

Проигнорируйте детали отношения, показанного в подсказке. Используйте подсказку, чтобы подтвердить, связаны ли определенные переменные. Затем поиск инстанцируют переменной, чтобы найти, как они связаны.

Дальнейшее исследование

Можно использовать прагму Inspection_Point, чтобы определить отношение между переменными в любой точке в коде. Можно ввести столько переменных, сколько вы хотите в операторе #pragma:

#pragma Inspection_Point var1 var2 ... varn

Попробуйте этот метод на других примерах. Например, выберите Help> Examples> Code_Prover_Example.psprj. Сгруппируйте результаты файлом. В файле single_file_analysis.c вы видите этот код:

    if (output_v7 >= 0) {

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

Если вы устанавливаете свой курсор на s8_ret в последних двух операторах, вы находите, что области значений s8_ret отличаются. Узнайте то, что изменилось между этими двумя операторами.

Подсказка: подсказка в операторе #pragma указывает, что переменная s8_ret связана с переменной output_v7. Отметьте оранжевую проверку, которая уменьшает область значений output_v7.

Документация