Функции инициализации (-functions-called-before-main)

Задайте функции, которые вы хотите, чтобы сгенерированный main вызвал перед другими функциями

Описание

Эта опция влияет на анализ Программы автоматического доказательства Кода только.

Задайте функции, которые вы хотите, чтобы сгенерированный main вызвал перед другими функциями.

Установите опцию

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция находится на узле Code Prover Verification. Смотрите Зависимости для других опций, которые необходимо также включить.

Командная строка: Используйте опцию -functions-called-before-main. Смотрите информацию о Командной строке.

Почему использование эта опция

Если вы проверяете модуль или библиотеку, Программа автоматического доказательства Кода генерирует функцию main, если вы не существуете. Если main существует, анализ использует существующий main.

Используйте эту опцию наряду с опцией Functions to call (-main-generator-calls), чтобы задать, какие функции сгенерированный main должен вызвать. Если функция не вызвана прямо или косвенно от main, программное обеспечение не анализирует функцию.

Настройки

Никакое значение по умолчанию

Введите имена функций или выберите из списка.

  • Щелкните, чтобы добавить поле и ввести имя функции.

  • Щелкните, чтобы перечислить функции в вашем коде. Выберите функции из списка.

Если функция или метод не перегружаются, задайте имя функции. В противном случае задайте прототипа функции с аргументами. Например, в следующем коде, необходимо задать прототипы func(int) и func(double).

int func(int x) { 
 return(x * 2);
}
double func(double x) { 
 return(x * 2);
}
Для C++, если функция:

  • Метод класса: сгенерированный main вызывает конструктора класса прежде, чем вызвать эту функцию.

  • Не метод класса: сгенерированный main вызывает эту функцию прежде, чем вызвать методы класса.

Если вы используете оператор разрешения области видимости, чтобы задать функцию от конкретного пространства имен, введите полностью определенное имя, например, myClass::init(int). Если функция не имеет параметра, используйте пустую круглую скобку, например, myClass::init().

Зависимости

Эта опция включена, только если вы выбираете Verify module or library под Code Prover Verification, и ваш код не содержит функцию main.

Советы

Несмотря на то, что эти функции вызваны перед другими функциями, они могут быть названы в произвольном порядке. Если вы хотите вызвать свои функции инициализации в определенном порядке, вручную запишите функцию main, чтобы вызвать их.

Информация о командной строке

Параметр: -functions-called-before-main
Значение: function1[,function2[,...]]
Никакое значение по умолчанию
Пример 1 (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -main-generator -functions-called-before-main myfunc
Пример 2 (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -main-generator -functions-called-before-main myClass::init(int)
Пример 1 (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -main-generator -functions-called-before-main myfunc
Пример 2 (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -main-generator -functions-called-before-main myClass::init(int)