Exponenta Banner

Disable checks for non-initialization (-disable-initialization-checks)

Отключите проверки для неинициализированных переменных и указателей

Описание

Эта опция влияет только на анализ Code Prover.

Задайте, что Polyspace® Code Prover™ не должны проверять отсутствие инициализации в коде.

Задать опцию

Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция находится на узле Check Behavior.

Командная строка и файл опций: Используйте опцию -disable-initialization-checks. См. «Информация о командной строке».

Зачем использовать эту опцию

Используйте эту опцию, если вы не хотите обнаруживать образцы неинициализированных переменных.

Настройки

На

Polyspace Code Prover не выполняет следующие проверки:

Polyspace принимает, что при объявлении:

  • Переменные имеют полный диапазон значений, разрешенных их типом.

  • Указатели можно NULL-значен или указывает на блок памяти с неизвестным смещением.

Off (по умолчанию)

Polyspace Code Prover проверяет отсутствие инициализации в вашем коде. Программа отображает красный цвет, проверяет, образец ли переменная не инициализирован, и оранжевый цвет проверяет, инициализирована ли переменная только на некоторых путях выполнения.

Совет

  • Если вы выбираете эту опцию, программное обеспечение не сообщает о большинстве нарушений MISRA C®: 2004 правила 9,1 и MISRA C:2012 Rule 9.1.

  • Если вы выберете эту опцию, количество и тип оранжевых чеков в вашем коде может измениться.

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

    Проверки на неинициализацию включеныПроверки на отсутствие инициализации отключены
    void func(int flag) {
    int var1,var2;
    if( flag==0) {
        var1=var2;
    }
    else {
        var1=0;
    }
    var2=var1 + 1;
}

    В этом примере программное обеспечение создает:

    • Красная Non-initialized local variable проверка var2 в if ветвь. Процесс верификации продолжается, как будто только else ветвь if оператор существует.

    • Зеленый Non-initialized local variable чек на var1 в последнем операторе. var1 имеет присвоенное значение 0.

    • Зеленый Overflow чек на + операция.

    void func(int flag) {
    int var1,var2;
    if( flag==0) {
        var1=var2;
    }
    else {
        var1=0;
    }
    var2=var1 + 1;
}

    В этом примере программное обеспечение:

    • Не производит проверки Non-initialized local variable. При инициализации программное обеспечение принимает, что var2 имеет полную область значений int значения. Следуя if оператор, поскольку программное обеспечение рассматривает оба if ветви, это принимает, что var1 также имеет полную область значений int значения.

    • Устанавливает оранжевый Overflow на + операция. Для образца, если var1 имеет максимальное int значение, добавление 1 к нему может вызвать переполнение.

Информация о командной строке

Параметр: -disable-initialization-checks
По умолчанию: Off
Пример (Code Prover): Polyspace Code Prover -sources file_name -disable-initialization-checks
Пример (Код Prover Server): Полипространство -code-prover-server -sources file_name -disable-initialization-checks

См. также

Темы

Документация Polyspace Code Prover

Поддержка