При запуске Polyspace ® для сгенерированного кода программа автоматически считывает из сгенерированного кода следующую информацию:
initialize() функции
terminate() функции
step() функции
Список переменных параметров
Список входных переменных
При запуске программы Code Prover программа использует эту информацию для создания main функция, которая:
Инициализация параметров с помощью параметра «Полиспейс» 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 для выполнения последующего анализа.
Для кода C++, генерируемого с помощью Embedded Coder ®, initialize(), step(), и terminate() функции и связанные переменные либо являются членами класса, либо имеют глобальную область действия.