-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 |