Оранжевая проверка показывает, что Polyspace ® обнаруживает возможную ошибку во время выполнения, но не может ее доказать. Проверка операции отображается оранжевым цветом, если выполнены оба условия:
| Первое условие | Второе условие | Пример |
|---|---|---|
| Операция выполняется несколько раз на пути выполнения или на нескольких путях выполнения. | Во время статической проверки операция завершается с ошибкой только часть раз или только на части путей. | Операция выполняется в:
|
| Операция включает переменную, которая может принимать несколько значений. | Во время статической проверки операция завершается неуспешно только для части значений. | Операция включает в себя volatile переменная. |
Во время статической проверки Polyspace может учитывать больше путей выполнения, чем путей выполнения во время выполнения. Если операция завершается неуспешно для подмножества путей, Polyspace не может определить, действительно ли это подмножество происходит во время выполнения. Поэтому вместо красного чека он производит оранжевый чек по операции.
Рассмотрим следующий пример:
void main() {
func(1);
func(0);
}
double func(int value) {
return (1.0/value); //Orange check
} |
func вызывается дважды с двумя аргументами. Только один из вызовов приводит к делению на ноль в теле func. Средство проверки кода показывает этот результат как оранжевое деление при нулевой проверке.
Рассмотрим следующий пример:
double func(int value) {
int reducedValue = value%21 - 10; // Result in [-10,10]
return 1.0/reducedValue; //Orange check
} |
Если контекст вызова func неизвестен, Code Prover предполагает, что его аргумент value может принять любое int значение. В результате, reducedValue может принимать любое значение в [-10,10]. Одно из этих значений равно нулю, что приводит к делению на ноль в func. Средство проверки кода показывает этот результат как оранжевое деление при нулевой проверке.
Рассмотрение супернабора действительных путей выполнения является звуковым приближением, поскольку Polyspace не теряет информацию. Если операция содержит ошибку времени выполнения, Polyspace не производит зеленую проверку операции. Если Polyspace не может доказать ошибку времени выполнения из-за аппроксимаций, он производит оранжевую проверку. Поэтому необходимо просмотреть оранжевые чеки.
Примеры аппроксимаций Polyspace включают в себя:
Аппроксимация диапазона переменной в определенной точке пути выполнения. Например, Polyspace может аппроксимировать диапазон {-1} U [0,10] из float переменная по [-1,10].
Аппроксимация перемежения инструкций в многозадачном коде. Например, даже если определенные команды в паре задач не могут прерывать друг друга, проверка Polyspace может не учитывать это.
Чтобы убедиться, что операция не завершается неуспешно во время выполнения, выполните следующие действия.
Определите, действительно ли могут возникнуть пути выполнения, по которым операция завершается неуспешно.
Дополнительные сведения см. в разделе Интерпретация результатов проверки кода в пользовательском интерфейсе Polyspace Desktop.
Если может возникнуть какой-либо из путей выполнения, устраните причину сбоя.
Если пути выполнения не могут возникнуть, введите комментарий в результат Polyspace или исходный код, описывающий, почему они не могут возникнуть. См. раздел Результаты анализа пространства адресов с помощью исправлений ошибок или обоснований.
В ходе последующей проверки можно импортировать эти комментарии в результаты. Затем, если проверка оранжевого цвета сохраняется при последующей проверке, повторная проверка не требуется.
Polyspace выполняет аппроксимации из-за одного из следующих.
Код не содержит полной информации о выполнении во время выполнения. Например, код частично разработан или содержит переменные, значения которых известны только во время выполнения.
Если требуется меньше оранжевых чеков, предоставьте информацию, необходимую Polyspace. Дополнительные сведения см. в разделе Предоставление контекста для проверки.
Ваш код очень сложный. Например, могут быть преобразования нескольких типов или несколько goto заявления.
Если требуется меньше проверок оранжевого цвета, уменьшите сложность кода и следуйте рекомендуемым практикам кодирования. Дополнительные сведения см. в разделе Соблюдение правил кодирования.
Polyspace должен завершить проверку в разумные сроки и использовать разумные вычислительные ресурсы.
Если требуется меньше проверок оранжевого цвета, повысьте точность проверки. Но более высокая точность также увеличивает время проверки. Дополнительные сведения см. в разделе Повышение точности проверки.