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