Code Prover исчерпывающе проверяет ваш код на определенные типы ошибок времени выполнения. Если проверка является неокончательной, результат отображен в оранжевом (с вопросительным знаком). С каждой оранжевой проверкой анализ предоставляет дополнительную информацию, которая может помочь определить, представляет ли проверка возможную ошибку времени выполнения или результат сверхприближения или широкого предположения.
Если проверка, более вероятно, будет ошибкой времени выполнения, это рассматривается как критическую оранжевую проверку. Обратите внимание на то, что красные и серые проверки подпадают под область критических проверок по определению, поскольку красная проверка указывает на определенную ошибку времени выполнения, и серая проверка указывает на код, который определенно недостижим (под текущими предположениями верификации). Обычно нет никакого вопроса определения вероятности при рассмотрении ошибок, обозначенных с красными и серыми проверками. С оранжевыми проверками критические проверки помогают фокусировать анализ на результатах, которые, более вероятно, будут ошибками времени выполнения.
Можно уменьшать список результатов Code Prover только к красным, серым и критическим оранжевым проверкам.
В пользовательском интерфейсе Polyspace® десктопные решения, можно непосредственно фокусировать список результатов к критическим проверкам только. На панели Results List, от выпадающего списка All results, выбирают Critical checks.
Выбор Critical checks сохраняет только красные, серые и критические оранжевые проверки на панели Results List.
В Polyspace доступ к веб-интерфейсу можно использовать отдельные фильтры для красных, серых и критических оранжевых проверок:
Отобразите только красные, серые и оранжевые проверки с помощью основанных на цвете фильтров.
Отобразите только критические оранжевые проверки с помощью основанных на тексте фильтров. В текстовом фильтре Show only введите Origin: Path related issue, чтобы видеть связанные с путем оранжевые проверки и Origin: Bounded inputs, чтобы видеть оранжевые проверки, связанные с ограниченными входными параметрами.
Понятие критических проверок позволяет вам приоритизировать свой анализ оранжевых проверок. Можно принять решение рассмотреть критические оранжевые проверки перед другими оранжевыми проверками или рассмотреть только критические оранжевые проверки. См. также Управление Оранжевые Регистрации Polyspace Code Prover.
Критические оранжевые проверки связаны с путем и ограниченными входными значениями. Здесь, входные значения относятся к значениям, которые являются внешними к приложению. Примеры включают:
Входные параметры функций вызваны сгенерированным основным. Для получения дополнительной информации о функциях, вызванных сгенерированным основным, смотрите Functions to call (-main-generator-calls).
Глобальные и энергозависимые переменные.
Данные возвращены заблокированной функцией. Данные могут быть значением, возвращенным функцией или параметром функции, измененным через указатель.
Обратите внимание на то, что могут быть оранжевые проверки, где программное обеспечение не может определить, связана ли с путем проверка или связана с входом. Поэтому более безопасный подход может быть должен рассмотреть критические проверки перед другими, но не ограничить анализ критическими проверками только.
Проверки, которые являются связанным с путем падением под областью критических оранжевых проверок. На панели Results List, для этих проверок, столбец Information содержит запись, Origin: Path related issue. Эти проверки очень важны, потому что программное обеспечение идентифицировало отличные пути к выполнению, где ошибка времени выполнения, вероятно, произойдет. Пути к выполнению отличны и отделимы от других путей, которые заканчиваются в линии с проверкой, потому что они проходят через различные инструкции в вашем коде (другая возможность проходила бы через те же инструкции, но для различных входных параметров).
Следующий пример показывает связанную с путем оранжевую проверку.
void path(int x) {
int result;
result = 1 / (x - 10);
// Orange division by zero
}
void main() {
path(1);
path(10);
}
Программное обеспечение идентифицирует оранжевую проверку Division by zero как потенциальную ошибку. Панель Result Details указывает на потенциальную ошибку:
... Warning: scalar division by zero may occur ...
Этот Division by zero проверяет result=1/(x-10) является оранжевым потому что:
path(1) не вызывает ошибку деления на нуль.
path(10) вызывает ошибку деления на нуль.
Обратите внимание на то, что оранжевая проверка в этом случае представляет определенную ошибку времени выполнения. Поэтому помимо связанной с путем оранжевой проверки, анализ также указывает на ошибку через красную ошибку Non-terminating call на path(10).
Проверки, которые связаны с ограниченными входными параметрами, подпадают под область критических оранжевых проверок. На панели Results List, для этих проверок, столбец Information содержит запись, Origin: Bounded inputs. Эти проверки очень важны, потому что программное обеспечение идентифицировало, что ошибка времени выполнения может произойти для некоторых входных данных программы, которые внешне ограничены. Поскольку входные значения явным образом ограничены, программное обеспечение не должно было делать предположение о входе. Поэтому входные значения и последовательные ошибки времени выполнения, вероятно, произойдут на практике.
Большинство входных значений может быть ограничено внешними ограничениями (также известный как Технические требования Области значений Данных или 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]
Проверки, которые связаны с неограниченными входными параметрами, подпадают под область критических оранжевых проверок. На панели Results List, для этих проверок, столбец Information содержит запись, Origin: Possibly impacted by inputs. Эти проверки не рассматриваются очень важными, потому что программное обеспечение идентифицировало, что ошибка времени выполнения может произойти для некоторых входных данных программы, которые не ограничены. Поскольку входные значения не ограничены, программное обеспечение принимает широкий диапазон входных значений на основе типов входных данных. Входные значения и последовательные ошибки времени выполнения не могут произойти на практике.
Следующий пример показывает оранжевую проверку, связанную с неограниченными входными значениями, которые могут быть идентифицированы как потенциальная ошибка времени выполнения:
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: [-231 .. 231-1]