Выполните один или несколько из этих шагов, пока вы не определите фиксацию для проверки User assertion. Существует несколько способов зафиксировать эту проверку. Для описания проверки и примеров кода, смотрите User assertion.
Иногда, специально для оранжевой проверки, можно решить, что проверка не представляет действительную ошибку, но предположение Polyspace®, которое не верно для кода. Если можно использовать аналитическую опцию, чтобы ослабить предположение, повторно выполнить верификацию с помощью той опции. В противном случае можно добавить комментарий и выравнивание в результате или коде.
Для общего рабочего процесса, который применяется ко всем проверкам, смотрите, Интерпретируют Результаты Polyspace Code Prover.
Как использовать эту проверку: Обычно вы используете операторы assert во время отладки, чтобы проверять, удовлетворено ли условие в текущей точке в вашем коде. Например, если вы ожидаете, что переменная var будет иметь значения в области значений [1,10] в определенный момент в вашем коде, вы помещаете следующий оператор в той точке:
assert(var >=1 && var <= 10);
Поэтому можно рассудительно вставить операторы assert, которые тестируют на требования из кода.
Красный результат для проверки User assertion показывает, что требование определенно не удовлетворяется.
Оранжевый результат для проверки User assertion показывает, что требование возможно не удовлетворяется.
Проследите поток данных для каждой переменной, вовлеченной в оператор assert.
В следующем примере проследите поток данных для myArray.
int* getArray(int numberOfElements) {
.
.
arrayPtr = (int*) malloc(numberOfElements);
.
.
return arrayPtr;
}
void func() {
int* myArray = getArray(10);
assert(myArray!=NULL);
.
.
}getArray, возвращаемое значение malloc не проверяется на NULL.Возможная фиксация: Если вы ожидаете определенное требование, смотрите, есть ли у вас тесты, которые осуществляют требование. В этом примере, если вы ожидаете, getArray, чтобы возвратить non-NULL значение, в getArray, тестирует возвращаемое значение malloc для NULL.
Чтобы проследить поток данных, выберите проверку и отметьте информацию о панели Result Details.
Если панель Result Details показывает последовательность инструкций, которые приводят к проверке, выбирают каждую инструкцию.
Если панель Result Details показывает номер строки вероятной причины для проверки, щелкните правой кнопкой по панели Source. Выберите Go To Line. Введите номер строки.
В противном случае, для каждой переменной, вовлеченной в условие, найдите предыдущие экземпляры и проследите до первопричины проверки. Для получения дополнительной информации об общих первопричинах смотрите Шаг 3: Ищите Частые причины Проверки.
В зависимости от переменной используйте следующие ярлыки навигации, чтобы найти предыдущие экземпляры. Можно выполнить следующие шаги в пользовательском интерфейсе Polyspace только.
| Переменная | Как найти предыдущие экземпляры переменной |
|---|---|
Локальная переменная | Используйте один из следующих методов:
|
Глобальная переменная Щелкните правой кнопкой по переменной. Если опция, Show In Variable Access View появляется, переменная, является глобальной переменной. |
|
Функциональное возвращаемое значение
ret=func(); |
|
Можно также определить, связаны ли переменные в какой-либо операции от некоторой предыдущей операции. Смотрите Находят Отношения Между Переменными в Коде.
Если проверка является оранжевой и происходит в функции, смотрите, вызвана ли функция многократно. Определите, перестало ли утверждение работать только на определенных вызовах. Для тех вызовов перейдите к телу вызывающей стороны и смотрите, есть ли у вас тесты, которые осуществляют ваше требование утверждения.
Чтобы видеть вызывающие стороны функции, выберите имя функции на панели Source. Все вызывающие стороны появляются на панели Call Hierarchy. Выберите имя вызывающей стороны, чтобы перейти к нему в вашем источнике.
Чтобы определить, вызывает ли подмножество вызовов оранжевую проверку, используйте опцию Sensitivity context (-context-sensitivity). Для примера смотрите, Идентифицируют Вызов функции с Ошибкой времени выполнения.
Если у вас есть тесты, которые осуществляют требование утверждения, видят если:
Оператор контроля в рамках тестов.
Вы изменяете тестовые переменные между тестом и утверждением.
Например, тест, if(index < SIZE) осуществляет тот index, является меньше, чем SIZE. Однако утверждение assert(index < SIZE) может перестать работать если:
Это происходит вне блока if.
Перед утверждением вы изменяете index в блоке if.
Возможная фиксация: Рассмотрите тщательно, необходимо ли удовлетворить требования утверждения. Если необходимо удовлетворить те требования, тесты места, которые осуществляют требование. После тестов постарайтесь не изменять тестовые переменные.
Смотрите, можно ли проследить оранжевую проверку до предположения Polyspace, которое происходит ранее в коде. Если предположение не сохраняется в вашем случае, добавьте комментарий или выравнивание в вашем результате или коде. Смотрите Результаты Polyspace Адреса Через Исправления ошибок или Комментарии.
Например, после вызова функции, вы утверждаете отношение между двумя переменными. Затем:
В зависимости от глубины вызова функции и сложности вашего кода, Polyspace может иногда аппроксимировать переменные диапазоны. Из-за приближения программное обеспечение не может установить, если отношение содержит и производит оранжевую проверку User assertion.
Запустите динамические тесты на оранжевой проверке, чтобы определить, перестало ли утверждение работать.
Для примера смотрите Тест Оранжевые Проверки на Ошибки времени выполнения.
Попытайтесь уменьшать свою сложность кода и повторно выполнить верификацию. В противном случае добавьте комментарий и выравнивание в вашем результате или коде, описывающем, почему вы не изменили свой код.
Для получения дополнительной информации смотрите Аналитические Предположения Программы автоматического доказательства Кода.
Прежде, чем выровнять по ширине оранжевую проверку, рассмотрите тщательно, можно ли улучшить проект кодирования.
