main
関数のない C アプリケーションの検証
Polyspace® 検証には、コードが main
関数を有することが必要です。次のいずれかを行います。
コードに
main
関数を設定します。Polyspace が
main
を生成すべきことを指定します。
main
関数の生成
検証の前に、次のオプションのうちの 1 つを指定します。Polyspace デスクトップ製品のユーザー インターフェイスでは、オプションは [Code Prover 検証] ノードの下に表示されます。
オプション | 説明 |
---|---|
アプリケーション全体の検証 | ソフトウェアによって |
モジュールまたはライブラリの検証 (-main-generator) | 検証の前に、Polyspace はコードに
|
main
関数の手動作成
main
の自動生成時に、ソフトウェアにより関数の呼び出し順序またはグローバル変数の動作について特定の仮定が行われます。たとえば、自動で生成される既定の main
では、動作が次のようにモデル化されます。
オプション
[呼び出す関数] (-main-generator-calls)
を使用して指定した関数は、任意の順序で呼び出すことができます。各関数本体の先頭では、グローバル変数はその型に応じて許容されるすべての値を取る可能性がある。
呼び出し順序のより正確なモデルを指定するには、検証用に main
関数を手動で作成できます。この main
関数は、プロジェクトに個別のファイルとして追加できます。場合によっては、正確な呼び出し順序を指定すると、オレンジ チェックの数を減らせます。たとえば、次のコードでは Polyspace は、f
および g
が任意の順序で呼び出される可能性があると仮定します。したがって、g
の前に f
が呼び出される場合に、オレンジのオーバーフローを生成します。g
の後に f
が呼び出されることがわかっている場合、main
関数を作成してこの順序をモデル化できます。
static char x; static int y; void f(void) { y = 300; } void g(void) { x = y; }