Code Prover 検証

アプリケーションまたはモジュール全体の検証

main 関数をもつ完全なアプリケーションを検証するか、main 関数をもたないモジュールを検証するかを指定するには、Code Prover 検証オプションを使用します。モジュールを検証する場合は、本ソフトウェアによって main 関数が生成されます。生成された main 関数を微調整するには、これらのオプションを使用します。

Polyspace オプション

すべて展開する

アプリケーション全体の検証ソース ファイルが不完全で main 関数が含まれていない場合に検証を停止
グローバル変数の共有と使用のみを表示 (-shared-variables-mode)グローバル変数の共有と使用を完全解析を実行することなく計算
コードの初期化セクションのみの検証 (-init-only-mode)初期化コードのみのランタイム エラーとその他の問題のチェック
モジュールまたはライブラリの検証 (-main-generator)main を含まないモジュールまたはライブラリがソース ファイルである場合に関数 main を生成
初期化する変数 (-main-generator-writes-variables)生成された main により初期化するグローバル変数の指定
初期化関数 (-functions-called-before-main)生成された main により他の関数より先に呼び出す関数の指定
呼び出す関数 (-main-generator-calls)生成された main により初期化関数の後に呼び出す関数の指定
ファイルを個別に検証 (-unit-by-unit)各ソース ファイルを他のソース ファイルと別個に検証するオプション
共通のソース ファイル (-unit-by-unit-common-source)ファイルごとの検証で各ソース ファイルにインクルードするファイルの指定
メイン エントリ ポイント (-main)main の Microsoft Visual C++ 拡張の指定
クラスの内容のみを解析 (-class-only)クラス メソッド以外のコードを解析しない
メンバー初期化チェックをスキップ (-no-constructors-init-check)クラス コンストラクターがクラス メンバーを初期化するかどうかをチェックしない
指定クラス内で呼び出す関数 (-class-analyzer-calls)検証するクラス メソッドの指定
クラス (-class-analyzer)検証するクラスの指定
モデル生成コードの検証 (-main-generator)ソース ファイル中にない場合は main 関数を生成することの指定
パラメーター (-variables-written-before-loop)生成された main によって巡回コード ループの前に必ず初期化される変数の指定
入力 (-variables-written-in-loop)生成された main によって巡回コード ループ中に必ず初期化される変数の指定
初期化関数 (-functions-called-before-loop)生成された main によって巡回コード ループの前に必ず呼び出される関数の指定
ステップ関数 (-functions-called-in-loop)生成された main によって巡回コード ループ中に必ず呼び出される関数の指定
終了関数 (-functions-called-after-loop)生成された main によって巡回コード ループの後に必ず呼び出される関数の指定

トピック