-main-generator)Создать main функция, если исходными файлами являются модули или библиотеки, не содержащие main
Этот параметр влияет только на анализ программы проверки кода.
Укажите, что Polyspace ® должен генерировать main если он не находит его в исходных файлах.
Пользовательский интерфейс (только для настольных ПК): в конфигурации проекта этот параметр находится в узле Проверка проверочного кода (Code Prover Verification).
файл командной строки и параметров: Использовать параметр -main-generator. См. раздел Сведения о командной строке.
Аналогичный параметр для сгенерированного модели кода см. в разделе Verify model generated code (-main-generator).
Эта опция используется при проверке модуля или библиотеки. Для анализа программы проверки кода требуется main функция. При проверке модуля или библиотеки код может не иметь main.
При использовании этой опции средство проверки кода создает main функция, если она не существует. Если main существует, анализ использует существующий main.
Вкл (по умолчанию)Polyspace генерирует main если он не находит его в исходных файлах. Произведенный main:
Инициализирует переменные, указанные Variables to initialize (-main-generator-writes-variables).
Перед вызовом других функций вызывает функции, указанные в Initialization functions (-functions-called-before-main).
Во всех возможных заказах вызывает функции, указанные в Functions to call (-main-generator-calls).
(Только C++) Вызывает методы класса, указанные Class (-class-analyzer) и Functions to call within the specified classes (-class-analyzer-calls).
Если выше не указаны функции и опции переменных, генерируется main:
Инициализирует все глобальные переменные, кроме объявленных ключевыми словами const и static.
Во всех возможных заказах вызывает все функции, которые не вызываются нигде в исходных файлах. Polyspace считает, что глобальные переменные могут быть записаны между двумя последовательными вызовами функций. Поэтому в каждой вызываемой функции глобальные переменные изначально имеют полный диапазон значений, допускаемых их типом.
ПрочьПолиспейс останавливается, если main отсутствует в исходных файлах.
Если main функция присутствует в исходных файлах, проверка использует, что main независимо от того, включена или отключена эта опция.
Опция релевантна только в том случае, если main отсутствует в исходных файлах.
При использовании опции Verify whole application (по умолчанию в командной строке), код должен содержать main функция. В противном случае появится ошибка:
Error: required main procedure not found
Если код не содержит main , используйте эту опцию для создания main функция.
Если указать параметры многозадачности, проверка игнорирует ваши спецификации для main генерация. Вместо этого проверка вводит пустой main функция.
Дополнительные сведения о параметрах многозадачности см. в разделе Настройка анализа многозадачности в многозадачном пространстве вручную.
Параметр: -main-generator |
| По умолчанию: Откл. |
Пример (проверка кода):
polyspace-code-prover -sources |
Пример (сервер проверки кода):
polyspace-code-prover-server -sources |