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

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

Это подразделение нулевой проверкой result=1/(x-10) оранжевый, потому что:

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

Polyspace ® указывает определенное деление на нулевую ошибку посредством ошибки неразрывного вызова на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); 
}

Если для переменной указан диапазон данных PERMENT от 5 до 10 val, проверка генерирует оранжевую проверку индекса массива Out of bounds на 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 на 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]

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