Exponenta Banner

Отключите проверки на неинициализацию (-disable-initialization-checks)

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

Описание

Эта опция влияет на анализ Программы автоматического доказательства Кода только.

Укажите, что Polyspace® Code Prover™ не должен проверять на неинициализацию в вашем коде.

Установите опцию

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

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

Почему использование эта опция

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

Настройки

На

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

  • Non-initialized local variable: Локальная переменная не инициализируется прежде чем быть считанным.

  • Non-initialized variable: Переменная кроме локальной переменной не инициализируется прежде чем быть считанным.

  • Non-initialized pointer: Указатель не инициализируется прежде чем быть считанным.

  • Return value not initialized: C функция не делает возвращаемого значения, когда ожидается.

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

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

  • Указатели могут быть NULL - оцененный или указать на блок памяти при неизвестном смещении.

От (значения по умолчанию)

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

Советы

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

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

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

    Проверки на Enabled неинициализациюПроверки на отключенную неинициализацию
    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'
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -disable-initialization-checks
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -disable-initialization-checks

Смотрите также

Темы

Документация Polyspace Code Prover
Поддержка