モジュールまたはライブラリの検証 (-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 |
例 (Code Prover Server): polyspace-code-prover-server -sources |
参考
アプリケーション全体の検証 | 初期化する変数 (-main-generator-writes-variables) | 初期化関数 (-functions-called-before-main) | 呼び出す関数 (-main-generator-calls) | クラス (-class-analyzer) | 指定クラス内で呼び出す関数 (-class-analyzer-calls)
トピック
- Polyspace 解析オプションの指定
- main 関数のない C アプリケーションの検証 (Polyspace Code Prover)
- C++ クラスの検証 (Polyspace Code Prover)