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