モジュールまたはライブラリの検証 (`-main-generator`)

main を含まないモジュールまたはライブラリがソースファイルである場合に関数 main を生成

説明

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

関数 main がソースファイル中に見つからない場合は Polyspace^® で生成するように指定します。

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

Polyspace ユーザーインターフェイス (デスクトップ製品のみ): プロジェクト構成で [Code Prover 検証] ノードを選択してから、このオプションを選択します。
Polyspace Platform ユーザーインターフェイス (デスクトップ製品のみ): プロジェクト構成の [静的解析] タブで [実行時エラー] ノードを選択してから、このオプションを選択します。
コマンドラインとオプションファイル: オプション -main-generator を使用します。コマンドライン情報を参照してください。

モデル生成コードに対する同様のオプションについては、モデル生成コードの検証 (-main-generator) を参照してください。

モジュールまたはライブラリを検証している場合は、このオプションを使用します。Code Prover 解析には、関数 main が必要です。モジュールまたはライブラリを検証するときに、コードに main が存在しない場合があります。

このオプションを使用すると、関数 main が存在しない場合、Code Prover によって生成されます。main 関数が存在する場合、解析では既存の main が使用されます。

オン (既定の設定)

関数 main がソースファイル中に見つからない場合、Polyspace はこれを生成します。生成された main は以下を行います。

[初期化する変数] (-main-generator-writes-variables) で指定された変数を初期化します。
他の関数を呼び出す前に、[初期化関数] (-functions-called-before-main) で指定された関数を呼び出します。
[呼び出す関数] (-main-generator-calls) で指定された関数を可能性があるすべての順序で呼び出します。
(C++ のみ) [クラス] (-class-analyzer) および [指定クラス内で呼び出す関数] (-class-analyzer-calls) で指定されたクラスメソッドを呼び出します。

上記の関数と変数のオプションが設定されていない場合、生成された main は以下を行います。

キーワード const および static で宣言された変数を除くグローバル変数をすべて初期化します。
ソースファイルのどこでも呼び出されていないすべての関数を可能性があるすべての順序で呼び出します。Polyspace は、グローバル変数が 2 つの連続する関数呼び出しの間に記述されていると見なします。したがって、呼び出される各関数で、グローバル変数は最初から型で許容される全範囲の値を有しています。

オフ

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

関数 main がソースファイルに存在する場合、このオプションが有効か無効かに関係なく、検証ではその関数 main が使用されます。
このオプションは、関数 main がソースファイルに存在しない場合にのみ関連します。
オプション [アプリケーション全体の検証] (コマンドラインでの既定の設定) を使用する場合、コードに関数 main が含まれていなければなりません。そうでない場合、次のエラーが表示されます。
Error: required main procedure not found
コードに関数 main が含まれていない場合、このオプションを使用して関数 main を生成します。
マルチタスキングオプションを指定すると、検証では main 生成の指定が無視されます。代わりに、検証では空の関数 main が組み込まれます。
マルチタスキングオプションについての詳細は、Polyspace マルチタスキング解析の手動設定を参照してください。

パラメーター: -main-generator

既定値: オフ

例 (Code Prover): polyspace-code-prover -sources file_name -main-generator

例 (Code Prover Server): polyspace-code-prover-server -sources file_name -main-generator