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

Документация Polyspace Code Prover
Поддержка