C++ コード検証用のコンテキストを設定する

この例は、C++ コード検証にコンテキストを設定する方法を示します。既定のオプションを使用し、main 関数を設定しない場合、Polyspace^® Code Prover™ はすべての検証条件に対してコードのロバスト性をチェックします。次にソフトウェアの例を示します。

さらに、関数を定義せずに宣言してコード内で呼び出している場合、Polyspace が関数のスタブとして機能します。前提条件の詳細は、Code Prover 解析の前提条件を参照してください。

[構成] ペインで解析オプションを使用し、既定の動作を変更し、コードに関するより多くのコンテキストを設定することができます。コンテキスト依存検証を実施することで、証明されたコードが多くなり、そのためオレンジチェックが少なくなる可能性があります。

以下のオプションを使用します。Polyspace デスクトップ製品のユーザーインターフェイスでは、オプションは [Code Prover 検証] ノードの下に表示されます。

オプション	目的
`初期化する変数 (-main-generator-writes-variables)`	コード内で明示的に初期化されていない場合でも、Polyspace が初期化済みとみなすべきグローバル変数を指定します。
`制約の設定 (-data-range-specifications)`	グローバル変数の範囲を指定します。

クラスメソッドを呼び出すには以下のオプションを使用します。Polyspace デスクトップ製品のユーザーインターフェイスでは、オプションは [Code Prover 検証] ノードの下に表示されます。

オプション	目的
`クラス (-class-analyzer)`	生成された `main` が呼び出すべきメソッドのクラスを指定します。
`指定クラス内で呼び出す関数 (-class-analyzer-calls)`	生成された `main` が呼び出すべきメソッドを指定します。
`クラスの内容のみを解析 (-class-only)`	生成された `main` がクラスメソッドのみを呼び出すべきであることを指定します。
`メンバー初期化チェックをスキップ (-no-constructors-init-check)`	各クラスコンストラクターがすべてのクラスメンバーを初期化するかどうかを `main` でチェックしないように指定します。

以下のオプションを使用し、クラスメソッドでない関数を呼び出します。Polyspace デスクトップ製品のユーザーインターフェイスでは、オプションは [Code Prover 検証] ノードの下に表示されます。

オプション	目的
`初期化関数 (-functions-called-before-main)`	生成された `main` が最初に呼び出すべき関数を指定します。
`呼び出す関数 (-main-generator-calls)`	生成された `main` が後から呼び出すべき関数を指定します。

参考