Выполните один или несколько из следующих шагов до тех пор, пока вы не определите исправление для проверки User assertion. Существует несколько способов исправить эту проверку. Для получения описания примеров проверки и кода смотрите User assertion.
Иногда, особенно для оранжевого чека, можно определить, что чек представляет не реальную ошибку, а Polyspace® предположение, что не соответствует действительности для вашего кода. Если для ослабления допущения можно использовать опцию анализа, повторите верификацию с помощью этой опции. В противном случае можно добавить комментарий и обоснование в результат или код.
Общий рабочий процесс, который применяется ко всем проверкам, см. в разделе Интерпретация результатов Prover кода в пользовательском интерфейсе рабочего стола Polyspace.
Как использовать эту проверку: Обычно вы используете 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 для возврата не- NULL значение, в getArray, проверьте возврат значение malloc для NULL.
Чтобы проследить поток данных, выберите проверку и отметьте информацию на панели Result Details.
Если на панели Result Details отображается последовательность команд, ведущих к проверке, выберите каждую инструкцию.
Если на панели Result Details отображается номер линии вероятной причины проверки, щелкните правой кнопкой мыши на панели Source. Выберите Go To Line. Введите номер линии.
В противном случае для каждой переменной, вовлеченной в условие, найдите предыдущие образцы и вернитесь к первопричине проверки. Для получения дополнительной информации об общих первопричинах смотрите Шаг 3: Проверьте общие причины проверки.
В зависимости от переменной используйте следующие навигационные ярлыки для поиска предыдущих образцов. Можно выполнить следующие шаги только в пользовательском интерфейсе Polyspace.
| Переменная | Как найти предыдущие образцы переменной |
|---|---|
Локальная переменная | Используйте один из следующих методов:
|
Глобальная переменная Щелкните правой кнопкой мыши переменную. Если появляется Show In Variable Access View опция, переменная является глобальной переменной. |
|
Функция возврата значение
ret=func(); |
|
Можно также определить, связаны ли переменные в любой операции с какой-либо предыдущей операцией. См. Раздел «Поиск отношений между переменными в коде».
Если проверка оранжевая и происходит в функции, смотрите, вызывается ли функция несколько раз. Определите, не удается ли выполнить проверку типа «assertion» только при определенных вызовах. Для этих вызовов перейдите к телу вызывающего абонента и проверьте, есть ли у вас тесты, которые обеспечивают соблюдение вашего требования к проверке.
Чтобы увидеть вызывающих абонентов функции, выберите имя функции на панели Source. Все вызывающие абоненты отображаются на панели Call Hierarchy. Выберите имя вызывающего абонента для перехода к нему в источнике.
Чтобы определить, является ли подмножество вызовов причиной проверки оранжевого цвета, используйте опцию Sensitivity context (-context-sensitivity). Для получения руководства Идентификация вызова функции с ошибкой времени выполнения.
Если у вас есть тесты, которые приводят в исполнение требование об утверждении, смотрите, если:
Оценка оператора находится в возможностях тестов.
Вы изменяете переменные теста между тестом и утверждением.
Например, тестовое if(index < SIZE) принудительно применяет это index меньше SIZE. Однако утверждение assert(index < SIZE) может ошибиться, если:
Это происходит вне if блок.
Перед утверждением вы изменяете index в if блок.
Возможное исправление: Тщательно подумайте, должны ли вы соответствовать вашим требованиям. Если вы должны соответствовать этим требованиям, разместите тесты, которые соблюдают ваши требования. После тестов избегайте изменения тестовых переменных.
Посмотрите, можно ли проследить оранжевую проверку до допущения Polyspace, которое происходит ранее в коде. Если предположение не имеет значения true в вашем случае, добавьте комментарий или обоснование в свой результат или код. Смотрите Адрес Результаты Polyspace через исправления ошибок или обоснования.
Например, после вызова функции вы утверждаете отношение между двумя переменными. Затем:
В зависимости от глубины вызова функции и сложности вашего кода, Polyspace может иногда аппроксимировать диапазоны переменных областей значений. Из-за приближения программное обеспечение не может установить, удерживает ли отношение и производит ли оно оранжевую проверку User assertion.
Запустите динамические тесты на оранжевой проверке, чтобы определить, не удается ли выполнить проверку типа «assertion».
Для получения руководства «Тестирование Orange Checks на ошибки времени выполнения».
Попытайтесь уменьшить сложность кода и повторить верификацию. В противном случае добавьте комментарий и обоснование в свой результат или код, описывающий, почему вы не изменили свой код.
Для получения дополнительной информации смотрите Допущения анализа Code Prover.
Примечание
Прежде чем обосновывать оранжевую проверку, внимательно рассмотрим, сможете ли вы улучшить свои проекты кодирования.
