Этот пример показывает, как определить, связаны ли переменные в произвольной операции в вашем коде ранее.
Например, рассмотрите эту операцию:
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
.