Критические проверки оранжевого цвета

Программа определяет подмножество оранжевых проверок, которые, скорее всего, являются ошибками времени выполнения. Если вы выбираете Critical checks из выпадающего списка в левой части панели инструментов Results List, можно просмотреть этот подмножество.

Эти оранжевые проверки связаны с путем и ограниченными входными значениями. Здесь входные значения относятся к значениям, внешним по отношению к приложению. Примеры включают:

Входные параметры функций, вызываемые сгенерированным основным. Для получения дополнительной информации о функциях, вызываемых сгенерированным основным узлом, смотрите Functions to call (-main-generator-calls).
Глобальные и летучие переменные.
Данные, возвращенные упорной функцией. Данные могут быть значением, возвращаемым функцией или параметром функции, измененным через указатель.

Путь

В следующем примере показана связанная с путем оранжевая проверка, которая может быть идентифицирована как потенциальная ошибка времени выполнения.

Примите во внимание следующий код.

void path(int x) { 
   int result; 
   result = 1 / (x - 10); 
   // Orange division by zero
 } 

void main() { 
    path(1);
    path(10);
 }

Программа определяет оранжевую проверку ZDV как потенциальную ошибку. Панель Result Details указывает на потенциальную ошибку:

...
Warning: scalar division by zero may occur
...

Это Division by zero проверить result=1/(x-10) оранжевый, потому что:

path(1) не вызывает деления на нулевую ошибку.
path(10) приводит к делению на нулевую ошибку.

Polyspace^® указывает определенное деление на нулевую ошибку через Non-terminating call ошибку на path(10). Если вы выбираете красный чек path(10)панель Result Details содержит следующую информацию:

NTC .... Reason for the NTC: {path.x=10)

Ограниченные входные значения

Большинство входных значений могут быть ограничены спецификациями области значений данных (DRS). В следующем примере показана оранжевая проверка, связанная с ограниченными входными значениями, которые могут быть идентифицированы как потенциальная ошибка времени выполнения.

int tab[10]; 
extern int val; 
// You specify that val is in [5..10]
 
void assignElement(int index) { 
   int result; 
   result = tab[index];  
   // Orange Out of bounds array index
 } 
void main(void) {
   assignElement(val); 
}

Если вы задаете PERMANENT данных областей значений от 5 до 10 для переменной valВерификация генерирует оранжевую Out of bounds array index проверку tab[index]. Панель Result Details содержит сведения о потенциальной ошибке:

Warning: array index may be outside bounds: [0..9]
This check may be an issue related to bounded input values
Verifying DRS on extern variable val may remove this orange. 
  array size: 10 
  array index value: [5 .. 10]

Неограниченные входные значения

В следующем примере показана оранжевая проверка, связанная с неограниченными входными значениями, которые могут быть идентифицированы как потенциальная ошибка времени выполнения:

int tab[10]; 
extern int val; 
 
void assignElement(int index) { 
   int result; 
   result = tab[index];  
   // Orange Out of bounds array index
 } 
void main(void) {
   assignElement(val); 
}

Эта верификация генерирует оранжевый Out of bounds array index чек на tab[index]. Панель Result Details содержит сведения о потенциальной ошибке:

Warning: array index may be outside bounds: [0..9]
This check may be an issue related to unbounded input values
If appropriate, applying DRS to extern variable val may remove this orange. 
 array size: 10 
 array index value: [-2³¹ .. 2³¹-1]

Документация