Exponenta Banner

Как работает Polyspace сгенерированного кода

Когда вы запускаете Polyspace® на сгенерированном коде программное обеспечение автоматически считывает из сгенерированного кода следующую информацию:

  • initialize() функции

  • terminate() функции

  • step() функции

  • Список переменных параметра

  • Список переменных входов

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

  1. Инициализирует параметры с помощью опции Polyspace Parameters (-variables-written-before-loop).

  2. Вызывает функции инициализации с помощью опции Initialization functions (-functions-called-before-loop).

  3. Инициализирует входы с помощью опции Inputs (-variables-written-in-loop).

  4. Вызывает step функция, использующая опцию Step functions (-functions-called-in-loop).

  5. Вызывает terminate функция, использующая опцию Termination functions (-functions-called-after-loop).

The 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

Code Prover использует эту сгенерированную main функция для выполнения последующего анализа.

Для кода С++, который генерируется с помощью Embedded Coder®, а initialize(), step(), и terminate() функции и связанные переменные являются членами класса или имеют глобальные возможности.

Документация Polyspace Code Prover

Поддержка