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

ソースファイルが不完全で 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 で生成されます。