Exponenta Banner

Verify initialization section of code only (-init-only-mode)

Проверяйте один только код инициализации на ошибки времени выполнения и другие проблемы

Описание

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

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

Чтобы указать на конец кода инициализации, вы вводите линию

#pragma polyspace_end_of_init
в main функция (только однажды). Код инициализации запускается с начала main и продолжается до этой прагмы.

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

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

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

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

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

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

Например, в этом примере:

#include <limits.h>

int aVar;
const int aConst = INT_MAX;
int anotherVar;

int main() {
      aVar = aConst + 1;
#pragma polyspace_end_of_init
      anotherVar = aVar - 1;
      return 0;
}
переполнение в линии aVar = aConst+1 должен быть зафиксирован сначала перед значением aVar используется в последующем коде.

Настройки

На

Polyspace проверяет код с начала main и продолжает до прагмы polyspace_end_of_init.

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

Polyspace проверяет законченное приложение, начинающееся с main функция.

Зависимости

Можно использовать эту опцию и определять раздел кода как код инициализации только если:

  • Ваша программа содержит main функционируйте и вы используете опцию Verify whole application (неявно установите по умолчанию в командной строке).

  • Вы устанавливаете Source code language (-lang) toc.

Обратите внимание на то, что прагма должна появиться только однажды в main функция. Прагма может появиться прежде или после объявлений переменной, но должна появиться после определений типа (typedefS.

Вы не можете использовать эту опцию со следующими опциями:

Советы

  • Используйте эту опцию наряду с опцией Check that global variables are initialized after warm reboot (-check-globals-init) полностью проверять код инициализации прежде, чем проверять остающуюся программу. Если вы используете обе опции, верификация проверяет на следующее:

    • Определенные или возможные ошибки времени выполнения в коде инициализации.

    • Ли весь non-const глобальные переменные инициализируются вдоль всех путей к выполнению через код инициализации.

  • Многозадачные опции отключены, если вы проверяете код инициализации только потому, что инициализация глобальных переменных, как ожидают, произойдет, прежде чем задачи (потоки) начнутся. В результате тела задачи не проверяются.

    См. также Многозадачность.

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

    Например, в этом примере, pragma появляется в if блок. Красная неинициализированная переменная проверка появляется на линии int a = var потому что путь, содержащий инициализацию, останавливается в местоположении прагмы. На единственном другом остающемся пути, который обходит if блокируйтесь, переменная var не инициализируется.

    int var;

int func();

int main() {
    int err = func();
    if(err) {
        var = 0;
 #pragma polyspace_end_of_init
    }
    int a = var;   
    return 0;
}
    Чтобы избежать этих ситуаций, попытайтесь поместить прагму вне блока. Смотрите другие предложения для размещения прагмы в ссылке для Check that global variables are initialized after warm reboot (-check-globals-init).

  • Чтобы определить инициализацию структуры, регулярный анализ Программы автоматического доказательства Кода только рассматривает поля, которые используются.

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

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

Параметр: -init-only-mode
Значение по умолчанию: 'off'
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники file_name - init-only-mode
Пример (Сервер Программы автоматического доказательства Кода): сервер программы автоматического доказательства полипробела кода - источники file_name - init-only-mode

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

|

Темы

Введенный в R2020a

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