Exponenta Banner

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

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

  • initialize() функции

  • terminate() функции

  • step() функции

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

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

Если при запуске Программу автоматического доказательства Кода, программное обеспечение использует эту информацию, чтобы сгенерировать 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).

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()шаг, и terminate() функции и сопоставленные переменные являются или членами класса или имеют глобальную область видимости.

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

Поддержка