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.
Code Prover может иногда показывать красные чеки в коде, который должен быть недоступен и серым. При распространении диапазонов переменных Code Prover иногда делает приближения. Делая эти приближения, Code Prover может считать недоступную ветвь достижимой. Если в этой недоступной ветви появляется ошибка, она окрашена в красный цвет.
Рассмотрим оператора:
if (test_var == 5) {
// Code Section
}test_var не имеет значения 5, if ветвь недоступна. Если Code Prover делает приближение, из-за чего test_var получает значение 5, ветвь теперь достижима и может показывать проверки других цветов.Используйте этот рисунок, чтобы понять эффект приближений. Из-за приближений проверяемый цвет, который выше, может заменить цвета ниже. Проверка, которая должна быть красной или зеленой (что указывает на определенную ошибку или определенное отсутствие ошибки), может стать оранжевой, потому что переменная получает дополнительные значения, которые не могут возникнуть во время исполнения. Проверка, которая должна быть серой, может показать красные, зеленые и оранжевые проверки, потому что Code Prover рассматривает недоступную ветвь как достижимую.
