-main-generator-writes-variables)Задайте глобальные переменные, которые вы хотите сгенерировать main инициализировать
Эта опция влияет только на анализ Code Prover.
Эта опция недоступна для кода, сгенерированного из MATLAB® код или Simulink® модели.
Задайте глобальные переменные, которые вы хотите сгенерировать main для инициализации. Polyspace® считает, что эти переменные имеют любое значение, разрешенное их типом.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция находится на узле Code Prover Verification. Смотрите Зависимости для других опций, которые вы также должны включить.
Командная строка и файл опций: Используйте опцию -main-generator-writes-variables. См. «Информация о командной строке».
Если вы проверяете модуль или библиотеку, Code Prover генерирует main функция, если она не существует. Если a main существует, в анализе используются существующие main.
Анализ Code Prover модуля без main функция делает некоторые допущения по умолчанию относительно инициализации глобальных переменных. Анализ принимает, что глобальные переменные, которые явно не инициализированы, могут иметь полную область значений значений, разрешенных их типами данных при каждом входе в незакрытую функцию. Например, в примере ниже, который не имеет main function, переменная glob принято, что имеют все возможные int значения в foo и bar (несмотря на модификацию в foo). Предположение является консервативным, так как контекст вызова foo и bar, в том числе какая функция будет вызвана ранее, не известно.
int glob;
int foo() {
int locFoo = glob;
glob++;
return locFoo;
}
int bar() {
int locBar = glob;
return locBar;
}main инициализирует такие глобальные переменные к полномасштабным значениям перед вызовом каждой незакрытой в противном случае функции. Используйте эту опцию, чтобы изменить это предположение по умолчанию и реализовать другую стратегию инициализации для глобальных переменных.По умолчанию:
Код С - public
Код С++ - uninit
uninitТолько для C++
Сгенерированный main инициализирует только глобальные переменные, которые вы не инициализировали во время объявления.
none Сгенерированный main не инициализирует глобальные переменные.
Глобальные переменные инициализируются согласно стандарту C/C +. Для образца, int или char переменные инициализируются в 0, float переменные - 0,0 и так далее.
public Сгенерированный main инициализирует все глобальные переменные, кроме объявленных с ключевыми словами static и const.
all Сгенерированный main инициализирует все глобальные переменные, кроме объявленных с ключевым словом const.
custom Сгенерированный main инициализирует только заданные вами глобальные переменные. Щелкните
, чтобы добавить поле. Введите глобальное имя переменной.
Использовать эту опцию можно только в том случае, если задано значение true:
Ваш код не содержит main функция.
Опция отключена, если вы включите опцию Ignore default initialization of global variables (-no-def-init-glob). Глобальные переменные рассматриваются как неинициализированные, пока вы явно не инициализируете их в коде.
Эта опция влияет только на глобальные переменные, определенные в проекте. Если глобальная переменная объявлена как externанализ считает, что переменная может иметь любое значение, разрешенное ее типом данных, независимо от значения этой опции.
Параметр: -main-generator-writes-variables |
Значение: uninit | none | public | all | custom |
По умолчанию: (C) public | (C++) uninit |
Пример (Code Prover): Polyspace Code Prover -sources |
Пример (Код Prover Server):
Полипространство -code-prover-server -sources file_name |
Verify module or library (-main-generator)