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 всегда ложным.
Возвращаемое значение read_an_input() никогда не равно 0.
Однако read_an_input может возвратить любое значение в полной целочисленной области значений, таким образом, это не правильное объяснение.
Вместо этого рассмотрите продвижение пути к выполнению к коду Грея:
Оранжевый Out of bounds array index проверяет средние значения y[x]=0;, что последующие строки имеют дело с x в [0,99].
Оранжевый Division by Zero проверяет деление средними значениями 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 равны, Polyspace полагает, что 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 также.
Программа автоматического доказательства кода может иногда показывать красные регистрации кода, который, как предполагается, является недостижимым и серым. При распространении переменных диапазонов Программа автоматического доказательства Кода иногда делает приближения. В создании этих приближений Программа автоматического доказательства Кода может рассмотреть в противном случае недостижимое ответвление как достижимое. Если ошибка появляется в том недостижимом ответвлении, это окрашено в красный.
Рассмотрите оператор:
if (test_var == 5) {
// Code Section
}test_var не имеет значения 5, ответвление if недостижимо. Если Программа автоматического доказательства Кода делает приближение, из-за которого test_var получает значение 5, ответвление теперь достижимо и может показать проверки других цветов.Используйте эту фигуру, чтобы понять эффект приближений. Из-за приближений цвет проверки, который выше, может заменить цвета ниже. Проверка, которая должна быть красной или зеленой (указание на определенную ошибку или определенное отсутствие ошибки) может стать оранжевой, потому что переменная получает дополнительные значения, которые не могут произойти во время выполнения. Проверка, которая должна быть серой, может показать красные, зеленые и оранжевые проверки, потому что Программа автоматического доказательства Кода рассматривает недостижимое ответвление как достижимое.
