В этом учебном пособии показано, как определить, связаны ли переменные произвольной операции в коде ранее.
Например, рассмотрим эту операцию:
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).
Выполните анализ этого кода и откройте результаты. Установите серый флажок Недоступный код.
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. На панели «Источник» щелкните правой кнопкой мыши 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.
Совет
Игнорировать подробности уравнения, показанные во всплывающей подсказке. Используйте подсказку для подтверждения связи определенных переменных. Затем выполните поиск экземпляров переменной, чтобы найти, как они связаны.
Вы можете использовать прагматику Inspection_Point для определения связи между переменными в любой точке кода. Можно ввести любое количество переменных в #pragma заявление:
#pragma Inspection_Point var1 var2 ... varn
Попробуйте этот метод на других примерах. Например, выберите Справка > Примеры > 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.