Exponenta Banner

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

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

Описание

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

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

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

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

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

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

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

Настройки

On

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

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

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

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

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

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

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

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

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

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

Советы

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

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

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

    Проверки на 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 - источники file_name - "отключите проверки инициализации"
Пример (Сервер Программы автоматического доказательства Кода): сервер программы автоматического доказательства полипробела кода - источники file_name - "отключите проверки инициализации"

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

Темы

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

Поддержка