-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 инициализирует такие глобальные переменные до значений полного диапазона перед вызовом каждой в противном случае функции. Эта опция используется для изменения этого предположения по умолчанию и реализации другой стратегии инициализации для глобальных переменных.По умолчанию:
Код C - public
Код C++ - uninit
uninitТолько C++
Произведенный 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 -sources |
Пример (сервер проверки кода):
polyspace-code-prover-server -sources |