生成されたコードの Polyspace 解析の動作

Simulink^® モデルからコードを生成する場合、生成されたコードには次のコンポーネントを含めることができます。

シミュレーションの開始前に実行する関数 initialize()。
シミュレーションの終了後に実行する関数 terminate()。
シミュレーションを実行するためにループ内で実行する関数 step()。

さらに、生成されるコードには、上記の呼び出しを含むプレースホルダー main() 関数が含まれる場合もあります。プレースホルダー main() は、展開の目的に合わせて編集することもできます。Embedded Coder^® によって生成される main についての詳細は、Main Program (Embedded Coder)を参照してください。

生成されたコードに対して Polyspace^® を実行すると、Polyspace によってコードから次の情報が収集されます。

関数 initialize()
関数 terminate()
関数 step()
パラメーター変数のリスト
入力変数のリスト

Code Prover を実行する場合、解析を容易にするために、この情報を使用して個別の main() 関数が生成されます。生成されたプレースホルダー main() が存在するかどうかに関係なく、Polyspace は独自の main() 関数を使用して次のタスクを実行します。

Polyspace オプション [パラメーター] (-variables-written-before-loop) を使用してパラメーターを初期化します。
オプション [初期化関数] (-functions-called-before-loop) を使用して初期化関数を呼び出します。
オプション [入力] (-variables-written-in-loop) を使用して入力を初期化します。
オプション [ステップ関数] (-functions-called-in-loop) を使用して、ループ内で関数 step を呼び出します。既定では、関数 step がループ内で任意の回数呼び出される可能性があると Polyspace が仮定します。Code Prover 解析の精度を上げるためにループ内の反復回数を指定するには、オプション -main-generator-bounded-loop (Polyspace Code Prover) を使用します。
オプション [終了関数] (-functions-called-after-loop) を使用して関数 terminate を呼び出します。

以下は、Polyspace によって生成される main 関数の構造の一例です。

init parameters    \\ -variables-written-before-loop
init_fct()	         \\ -functions-called-before-loop
  while(random){        \\ start main loop with one or more iterations
  init inputs      \\ -variables-written-in-loop
  step_fct()       \\ -functions-called-in-loop
}
terminate_fct()    \\ -functions-called-after-loop

Embedded Coder で生成された C++ コードでは、関数 initialize()、関数 step()、関数 terminate()、および関連する変数は、クラスメンバーであるか、グローバルスコープを持つかします。