アプリケーション全体の検証

ソース ファイルが不完全で main 関数が含まれていない場合に検証を停止

説明

このオプションは Code Prover 解析のみに影響します。

このオプションは、MATLAB® コードまたは Simulink® モデルから生成されたコードでは使用できません。

main 関数がソース ファイル中にない場合は Polyspace® 検証を停止するように指定します。

[コンパイラ] (-compiler) に Visual C++® 設定を選択する場合は、main と見なす関数を指定できます。メイン エントリ ポイント (-main) を参照してください。

オプションの設定

以下のいずれかの方法を使用してオプションを設定します。

  • Polyspace ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成で [Code Prover 検証] ノードを選択してから、このオプションを選択します。

  • Polyspace Platform ユーザー インターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] ノードを選択してから、このオプションを選択します。

  • コマンド ラインとオプション ファイル: 対応するコマンド ライン オプションはありません。コマンド ライン情報を参照してください。

設定

オン

main 関数がソース ファイル中に見つからない場合、Polyspace 検証は停止します。

オフ (既定の設定)

main 関数がソース ファイル中にない場合でも Polyspace により検証を続行します。main がない場合は、main 関数を備えたファイル __polyspace_main.c が生成されます。

ヒント

このオプションを使用する場合、コードに main 関数が含まれていなければなりません。そうでない場合、次のエラーが表示されます。

Error: required main procedure not found

コードに main 関数が含まれていない場合、オプション [モジュールまたはライブラリの検証] (-main-generator) を使用して main 関数を生成します。

コマンド ライン情報

コマンド ラインの場合は、ユーザー インターフェイスと既定の設定が異なり、main 関数がソース ファイル中に見つからないと検証が停止します。オプション -main-generator を指定すると、main がソース ファイル中に見つからない場合に Polyspace で生成されます。

参考

|

トピック