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 достигает деления xX еще не был инициализирован. Поэтому программное обеспечение генерирует красный 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.cX находится в [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, ветвь теперь достижима и может показать проверки других цветов.Используйте этот рисунок, чтобы изучить эффект приближений. Из-за приближений цвет проверки, который выше, может заменить цвета ниже. Проверка, которая должна быть красной или зеленой (указание на определенную ошибку или определенное отсутствие ошибки) может стать оранжевой, потому что переменная получает дополнительные значения, которые не могут произойти во время выполнения. Проверка, которая должна быть серой, может показать красные, зеленые и оранжевые проверки, потому что Программа автоматического доказательства Кода рассматривает недостижимую ветвь как достижимую.
