C コード検証用のコンテキストを設定する
この例は、C コード検証用のコンテキストを設定する方法を示します。既定のオプションを使用し、main 関数を設定しない場合、Polyspace® Code Prover™ はすべての検証条件に対してコードのロバスト性をチェックします。次にソフトウェアの例を示します。
グローバル変数および呼び出されない関数の入力が全範囲であるとみなします。
呼び出されない関数を任意の順番で呼び出す
mainを生成します。
さらに、関数を定義せずに宣言してコード内で呼び出している場合、Polyspace が関数のスタブとして機能します。前提条件の詳細は、Code Prover 解析の前提条件を参照してください。
[構成] ペインで解析オプションを使用し、既定の動作を変更し、コードに関するより多くのコンテキストを設定することができます。コンテキスト依存検証を実施することで、証明されたコードが多くなり、そのためオレンジ チェックが少なくなる可能性があります。
変数範囲の制御
以下のオプションを使用します。Polyspace デスクトップ製品のユーザー インターフェイスでは、オプションは [Code Prover 検証] ノードの下に表示されます。
| オプション | 目的 |
|---|---|
初期化する変数 (-main-generator-writes-variables) | コード内で明示的に初期化されていない場合でも、Polyspace が初期化済みとみなすべきグローバル変数を指定します。 |
制約の設定 (-data-range-specifications) | グローバル変数の範囲を指定します。 |
関数の呼び出し順序を制御する
以下のオプションを使用します。Polyspace デスクトップ製品のユーザー インターフェイスでは、オプションは [Code Prover 検証] ノードの下に表示されます。
| オプション | 目的 |
|---|---|
初期化関数 (-functions-called-before-main) | 生成された main が最初に呼び出すべき関数を指定します。 |
呼び出す関数 (-main-generator-calls) | 生成された main が後から呼び出すべき関数を指定します。 |
スタブ動作の制御
以下のオプションを使用します。Polyspace デスクトップ製品のユーザー インターフェイスでは、オプションは [入力およびスタブ] ノードの下に表示されます。
| オプション | 目的 |
|---|---|
スタブを生成する関数 (-functions-to-stub) | Polyspace がスタブすべき関数を指定します。 |
