-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);
}Метод класса: сгенерированный main вызывает конструктора класса прежде, чем вызвать эту функцию.
Не метод класса: сгенерированный main вызывает эту функцию прежде, чем вызвать методы класса.
Если вы используете оператор разрешения области видимости, чтобы задать функцию от конкретного пространства имен, введите полностью определенное имя, например, myClass::init(int). Если функция не имеет параметра, используйте пустую круглую скобку, например, myClass::init().
Эта опция включена, только если вы выбираете Verify module or library под Code Prover Verification, и ваш код не содержит функцию main.
Несмотря на то, что эти функции вызваны перед другими функциями, они могут быть названы в произвольном порядке. Если вы хотите вызвать свои функции инициализации в определенном порядке, вручную запишите функцию main, чтобы вызвать их.
Параметр: -functions-called-before-main |
Значение: |
| Никакое значение по умолчанию |
Пример 1 (программа автоматического доказательства кода):
|
Пример 2 (программа автоматического доказательства кода):
|
Пример 1 (сервер программы автоматического доказательства кода):
|
Пример 2 (сервер программы автоматического доказательства кода):
|
Class (-class-analyzer) | Functions to call (-main-generator-calls) | Functions to call within the specified classes (-class-analyzer-calls) | Variables to initialize (-main-generator-writes-variables) | Verify module or library (-main-generator)