Функции, чтобы вызвать (-main-generator-calls)

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

Описание

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

Задайте функции, которые вы хотите, чтобы сгенерированный main вызвал. main вызывает эти функции после тех, вы задаете через опцию Initialization functions (-functions-called-before-main).

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

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

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

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

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

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

Настройки

Значение по умолчанию: unused

none

Сгенерированный main не вызывает функции.

unused

Сгенерированный main вызывает только те функции, которые не называются в исходном коде. Это не вызывает встроенные функции.

all

Сгенерированный main вызывает все функции кроме встроенных единиц.

custom

Сгенерированный main вызывает функции, которые вы задаете.

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

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

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

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

Зависимости

Эта опция доступна, только если вы выбираете Verify module or library (-main-generator).

Советы

  • Выберите unused, когда вы будете использовать Code Prover Verification> Verify files independently.

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

  • Чтобы проверить многозадачное приложение без основного, выберите none.

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

  • Чтобы задать инстанцирования шаблонов в качестве аргументов, запустите анализ однажды с аргументом all опции. Ищите имя шаблона в анализе, регистрируют и используют имя шаблона, как это появляется в аналитическом журнале для аргумента опции.

    Например, чтобы задать это инстанцирование функции шаблона в качестве аргумента опции:

    template <class T>
    T GetMax (T a, T b) {
      T result;
      result = (a>b)? a : b;
      return (result);
    } 
    template int GetMax<int>(int, int); // explicit instantiation
    
    Запустите анализ с опцией -main-generator-calls all. Ищите getMax в аналитическом журнале. Вы видите функциональный формат:
    T1 getMax<int>(T1, T1)
    Чтобы вызвать только это инстанцирование шаблона, удалите пробел между аргументами и используйте опцию:
    -main-generator-calls custom="T1 getMax<int>(T1,T1)"

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

Параметр: -main-generator-calls
Значение: none | unused | all | custom=function1[,function2[,...]]
Значение по умолчанию: unused
Пример (программа автоматического доказательства кода): polyspace-code-prover -sources file_name -main-generator -main-generator-calls all
Пример (сервер программы автоматического доказательства кода): polyspace-code-prover-server -sources file_name -main-generator -main-generator-calls all