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

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

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

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

Path

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

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

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]

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