Рассмотрите и зафиксируйте пользовательские проверки утверждения

Выполните один или несколько из этих шагов, пока вы не определите фиксацию для проверки User assertion. Существует несколько способов зафиксировать эту проверку. Для описания проверки и примеров кода, смотрите User assertion.

Иногда, специально для оранжевой проверки, можно решить, что проверка не представляет действительную ошибку, но предположение Polyspace®, которое не верно для кода. Если можно использовать аналитическую опцию, чтобы ослабить предположение, повторно выполнить верификацию с помощью той опции. В противном случае можно добавить комментарий и выравнивание в результате или коде.

Для общего рабочего процесса, который применяется ко всем проверкам, смотрите, Интерпретируют Результаты Polyspace Code Prover.

Как использовать эту проверку: Обычно вы используете assert операторы во время отладки, чтобы проверять, удовлетворяют ли условию в текущей точке в вашем коде. Например, если вы ожидаете переменную var иметь значения в области значений [1,10] в определенный момент в вашем коде вы помещаете следующий оператор в той точке:

assert(var >=1 && var <= 10);
Polyspace статически определяет, удовлетворяют ли условию.

Поэтому можно рассудительно вставить assert операторы, которые тестируют на требования из вашего кода.

  • Красный результат для проверки User assertion показывает, что требование определенно не удовлетворяется.

  • Оранжевый результат для проверки User assertion показывает, что требование возможно не удовлетворяется.

Шаг 1: определите первопричину проверки

Проследите поток данных для каждой переменной, вовлеченной в 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 только.

    ПеременнаяКак найти предыдущие экземпляры переменной

    Локальная переменная

    Используйте один из следующих методов:

    • Ищите переменную.

      1. Щелкните правой кнопкой по переменной. Выберите Search For All References.

        Все экземпляры переменной появляются на панели Search с текущим подсвеченным экземпляром.

      2. На панели Search выберите предыдущие экземпляры.

    • Просмотрите исходный код.

      1. Дважды кликните переменную на панели Source.

        Все экземпляры переменной подсвечены.

      2. Прокрутите, чтобы найти предыдущие экземпляры.

    Глобальная переменная

    Щелкните правой кнопкой по переменной. Если опция, Show In Variable Access View появляется, переменная, является глобальной переменной.

    1. Выберите опцию Show In Variable Access View.

      На панели Variable Access показывают текущий экземпляр переменной.

    2. На этой панели выберите предыдущие экземпляры переменной.

      Операции записи на переменной обозначаются с и операции чтения с.

    Функциональное возвращаемое значение

    ret=func();

    1. Найдите функциональное определение.

      Щелкните правой кнопкой по func на панели Source. Выберите Go To Definition, если опция существует. Если определение не доступно для Polyspace, выбирание опции берет вас к объявлению функции.

    2. В определении func, идентифицируйте каждый return оператор. Переменная, которую возвращает функция, является вашей новой переменной, чтобы проследить.

    Можно также определить, связаны ли переменные в какой-либо операции от некоторой предыдущей операции. Смотрите Находят Отношения Между Переменными в Коде.

Шаг 2: ищите частые причины проверки

  1. Если проверка является оранжевой и происходит в функции, смотрите, вызвана ли функция многократно. Определите, перестало ли утверждение работать только на определенных вызовах. Для тех вызовов перейдите к телу вызывающей стороны и смотрите, есть ли у вас тесты, которые осуществляют ваше требование утверждения.

  2. Если у вас есть тесты, которые осуществляют требование утверждения, видят если:

    • Оператор контроля в рамках тестов.

    • Вы изменяете тестовые переменные между тестом и утверждением.

    Например, тест if(index < SIZE) осуществляет тот index меньше SIZE. Однако утверждение assert(index < SIZE) может перестать работать если:

    • Это происходит вне if блок.

    • Перед утверждением вы изменяете index в if блок.

    Возможная фиксация: Рассмотрите тщательно, необходимо ли удовлетворить требования утверждения. Если необходимо удовлетворить те требования, тесты места, которые осуществляют требование. После тестов постарайтесь не изменять тестовые переменные.

Шаг 3: проследите проверку до предположения Polyspace

Смотрите, можно ли проследить оранжевую проверку до предположения Polyspace, которое происходит ранее в коде. Если предположение не сохраняется в вашем случае, добавьте комментарий или выравнивание в вашем результате или коде. Смотрите Результаты Polyspace Адреса Через Исправления ошибок или Выравнивания.

Например, после вызова функции, вы утверждаете отношение между двумя переменными. То:

  1. В зависимости от глубины вызова функции и сложности вашего кода, Polyspace может иногда аппроксимировать переменные диапазоны. Из-за приближения программное обеспечение не может установить, если отношение содержит и производит оранжевую проверку User assertion.

  2. Запустите динамические тесты на оранжевой проверке, чтобы определить, перестало ли утверждение работать.

    Для примера смотрите Тест Оранжевые Проверки на Ошибки времени выполнения.

  3. Попытайтесь уменьшать свою сложность кода и повторно выполнить верификацию. В противном случае добавьте комментарий и выравнивание в вашем результате или коде, описывающем, почему вы не изменили свой код.

Для получения дополнительной информации смотрите Аналитические Предположения Программы автоматического доказательства Кода.

Примечание

Прежде, чем выровнять по ширине оранжевую проверку, рассмотрите тщательно, можно ли улучшить проект кодирования.