Когда вы запускаете Polyspace® на сгенерированном коде, программное обеспечение автоматически считывает следующие информации из сгенерированного кода:
Функции initialize()
Функции terminate()
Функции step()
Список переменных параметра
Список входных переменных
Если при запуске Программу автоматического доказательства Кода, программное обеспечение использует эту информацию, чтобы сгенерировать функцию main что:
Инициализирует параметры с помощью опции Polyspace Parameters (-variables-written-before-loop).
Функции инициализации вызовов с помощью опции Initialization functions (-functions-called-before-loop).
Инициализирует входные параметры с помощью опции Inputs (-variables-written-in-loop).
Вызывает функцию step использование опции Step functions (-functions-called-in-loop).
Вызывает функцию terminate использование опции Termination functions (-functions-called-after-loop).
Функция main концептуально выглядит так:
init parameters \\ -variables-written-before-loop
init_fct() \\ -functions-called-before-loop
while(1){ \\ start main loop
init inputs \\ -variables-written-in-loop
step_fct() \\ -functions-called-in-loop
}
terminate_fct() \\ -functions-called-after-loopПрограмма автоматического доказательства кода использует, это сгенерировало функцию main, чтобы выполнить последующий анализ.
Для Кода С++, который сгенерирован с Embedded Coder®, initialize(), step(), и функции terminate() и связанные переменные являются или членами класса или имеют глобальную область видимости.