-main-generator-writes-variables)Задайте глобальные переменные, что вы хотите сгенерированный main инициализировать
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Эта опция не доступна для кода, сгенерированного из кода MATLAB® или моделей Simulink®.
Задайте глобальные переменные, что вы хотите сгенерированный main инициализировать. Polyspace® полагает, что эти переменные имеют любое значение, позволенное их типом.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Code Prover Verification. Смотрите Зависимости для других опций, которые необходимо также включить.
Командная строка и файл опций: Используйте опцию -main-generator-writes-variables. Смотрите информацию о командной строке.
Если вы проверяете модуль или библиотеку, Программа автоматического доказательства Кода генерирует main функционируйте, если вы не существуете. Если main существует, анализ использует существующий main.
Анализ Программы автоматического доказательства Кода модуля без main функция делает некоторые предположения по умолчанию об инициализации глобальной переменной. Анализ принимает, что глобальные переменные, которые явным образом не инициализируются, могут иметь полный спектр значений, позволенных их типами данных после каждой записи в невостребованную функцию. Например, в примере ниже, который не имеет main функция, переменная 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
uninitC++ только
Сгенерированный main только инициализирует глобальные переменные, которые вы не инициализировали во время объявления.
none Сгенерированный main не инициализирует глобальные переменные.
Глобальные переменные инициализируются согласно C/C + стандарт. Например, int или char переменные инициализируются к 0, float переменные к 0,0, и так далее.
public Сгенерированный main инициализирует все глобальные переменные кроме объявленных с ключевыми словами static и const.
all Сгенерированный main инициализирует все глобальные переменные кроме объявленных с ключевым словом const.
custom Сгенерированный main только инициализирует глобальные переменные, которые вы задаете. Щелкните
, чтобы добавить поле. Введите имя глобальной переменной.
Можно использовать эту опцию, только если следующее верно:
Ваш код не содержит 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 |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |
Verify module or library (-main-generator)