Polyspace ® считает, что все пути выполнения, содержащие ошибку времени выполнения, заканчиваются в месте ошибки. Для заданного пути выполнения Polyspace выделяет первое появление ошибки времени выполнения как проверку красным или оранжевым цветом и исключает этот путь из рассмотрения. Поэтому:
После проверки красным цветом Polyspace не анализирует остающийся код в той же области, что и проверка.
После проверки оранжевого цвета Polyspace анализирует оставшийся код. Но он рассматривает только сокращенное подмножество путей выполнения, которое не содержало ошибки времени выполнения. Следовательно, если зеленая проверка выполняется в операции после оранжевой проверки, это означает, что операция не вызывает ошибки времени выполнения только для этого сокращенного набора путей выполнения.
Возможны исключения из этого поведения. Например:
Для оранжевого переполнения, если указано warn-with-wrap-around или allow для Overflow mode for signed integer (-signed-integer-overflows) или Overflow mode for unsigned integer (-unsigned-integer-overflows), Polyspace переносит результат переполнения и не завершает пути выполнения.
Для субнормального результата с плавающей запятой, если указан warn-all для Subnormal detection mode (-check-subnormal), Polyspace не завершает пути выполнения с субнормальными результатами.
Путь, содержащий ошибку времени выполнения, завершается по следующим причинам:
Состояние программы неизвестно после ошибки. Например, после ошибки «Незаконно» в операции x=*ptr, значение x неизвестно.
Можно просмотреть ошибку как можно раньше в коде, поскольку первая ошибка на пути выполнения отображается в результатах проверки.
Не обязательно просматривать, а затем фиксировать или обосновывать один и тот же результат более одного раза. Например, рассмотрим эти операторы, где вертикальное многоточие представляет код, в котором переменная i не изменяется.
x = arr[i]; . . y = arr[i];
x=arr[i], это означает, что i может находиться за пределами массива. Вы не хотите просматривать еще один оранжевый чек y=arr[i] по той же причине.
Используйте эти два правила для понимания ваших проверок. Следующие примеры показывают, как эти два правила могут привести к проверкам, которые могут вводить в заблуждение при просмотре вне контекста. Ознакомьтесь с приведенными ниже примерами, чтобы ознакомиться с практикой проверки проверок в контексте оставшегося кода.
В следующем примере показано, что происходит после проверки красным цветом:
void red(void)
{
int x;
x = 1 / x ;
x = x + 1;
}Когда проверка Polyspace достигает деления на x, x еще не инициализирована. Поэтому программное обеспечение генерирует красный Non-initialized local variable проверка для x.
Пути выполнения за пределами разделения на x остановлены. Проверки для выписки не создаются x = x + 1;.
В следующем примере показано, как зеленая проверка может быть результатом предыдущей оранжевой проверки. Оранжевая проверка завершает пути выполнения, содержащие ошибку. Зеленая проверка операции после оранжевой проверки означает, что операция не вызывает ошибки времени выполнения только для остальных путей выполнения.
extern int Read_An_Input(void);
void propagate(void)
{
int x;
int y[100];
x = Read_An_Input();
y[x] = 0;
y[x] = 0;
}В этой функции:
x присваивается возвращаемое значение Read_An_Input. После этого назначения программное обеспечение оценивает диапазон x как [-2^31, 2^31-1].
Первое y[x]=0; показывает Out of bounds array index ошибка, потому что x может иметь отрицательные значения.
После первого y[x]=0;, от размера y, оценки программного обеспечения x находиться в диапазоне [0,99].
Второе y[x]=0; показывает зеленый чек, потому что x лежит в диапазоне [0,99].
В следующем примере показано, как серый чек может быть результатом предыдущего оранжевого чека.
Рассмотрим следующий пример:
extern int read_an_input(void);
void main(void)
{
int x;
int y[100];
x = read_an_input();
y[x] = 0;
y[x-1] = (1 / x) + x ;
if (x == 0)
y[x] = 1;
}Линия y[x]=1; недостижим.
Поэтому тест для оценки того, x = 0 всегда имеет значение false.
Возвращаемое значение read_an_input() никогда не равно 0.
Однако read_an_input может возвращать любое значение в полном целочисленном диапазоне, поэтому это неверное объяснение.
Вместо этого рассмотрим путь выполнения, ведущий к серому коду:
Оранжевая проверка индекса массива Out of bounds y[x]=0; означает, что последующие строки имеют дело с x в [0,99].
Оранжевое деление на ноль проверить на деление на x означает, что x не может равняться 0 в последующих строках. Поэтому, следуя этой строке, x находится в [1,99].
Поэтому x никогда не равно 0 в if состояние. Кроме того, доступ к массиву осуществляется через y[x-1] показывает зеленый чек.
В следующем примере показано, как красная ошибка может выявить ошибку, возникшую в предыдущих строках.
%% file1.c %%
void f(int);
int read_an_input(void);
int main() {
int x,old_x;
x = read_an_input();
old_x = x;
if (x<0 || x>10)
return 1;
f(x);
x = 1 / old_x;
// Red Division by Zero
return 0;
}
|
%% file2.c %%
#include <math.h>
void f(int a) {
int tmp;
tmp = sqrt(0-a);
}
|
Красная проверка выполняется на x=1/old_x; в file1.c из-за следующей последовательности шагов во время проверки:
Когда x присвоен old_x в file1.c, проверка предполагает, что x и old_x имеют полный диапазон целого числа, то есть [-2^31 , 2^31-1].
После if предложение в file1.c, x находится в [0,10]. Поскольку x и old_x равны, Полиспейс считает, что old_x находится в [0,10] также.
Когда x передается в f в file1.c, единственно возможное значение, которое x может иметь значение 0. Все остальные значения приводят к особой ситуации во время выполнения в file2.c, то есть tmp = sqrt(0–a);.
Красная ошибка возникает на x=1/old_x; в file1.c потому что программное обеспечение предполагает old_x равно 0.
Средство проверки кода иногда может отображать красные чеки в коде, который должен быть недостижимым и серым. При распространении диапазонов переменных средство проверки кода иногда делает аппроксимации. Делая эти аппроксимации, Code Prover может считать недостижимую ветвь достижимой. Если в этой недостижимой ветви появляется ошибка, она окрашивается в красный цвет.
Рассмотрим утверждение:
if (test_var == 5) {
// Code Section
}test_var не имеет значения 5, if ветвь недоступна. Если средство проверки кода делает аппроксимацию, из-за которой test_var получает значение 5, ветвь теперь доступна и может отображать проверки других цветов.Используйте этот рисунок, чтобы понять эффект аппроксимаций. Из-за аппроксимаций цвет проверки, который выше, может заменить цвета ниже. Проверка, которая должна быть красной или зеленой (указывающая на определенную ошибку или определенное отсутствие ошибки), может стать оранжевой, поскольку переменная получает дополнительные значения, которые не могут возникнуть во время выполнения. В чеке, который должен быть серым, могут отображаться красные, зеленые и оранжевые чеки, поскольку программа Code Prover считает недостижимую ветвь доступной.
