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

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

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

return(var1 - var2);

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

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

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

В этом примере считайте операцию подсвеченной. Вы не можете сказать от быстрого взгляда если 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 и как найти отношение:

Настройте аналитическую настройку Polyspace:
- Установите язык исходного кода на C. Используйте аналитическую опцию Source code language (-lang).
- Ограничьте область значений переменной 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.

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