Поиск отношений между переменными в коде

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

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

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.

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