メインコンテンツ

main 関数のない C アプリケーションの検証

Polyspace® 検証には、コードが main 関数を有することが必要です。次のいずれかを行います。

  • コードに main 関数を設定します。

  • Polyspace が main を生成すべきことを指定します。

main 関数の生成

検証の前に、次のオプションのうちの 1 つを指定します。Polyspace デスクトップ製品のユーザー インターフェイスでは、オプションは [Code Prover 検証] ノードの下に表示されます。

オプション説明
アプリケーション全体の検証

ソフトウェアによって main が検出されないと検証が停止します。

モジュールまたはライブラリの検証 (-main-generator)

検証の前に、Polyspace はコードに main 関数が含まれているかどうかをチェックします。

main 関数が存在する場合、ソフトウェアはその main を使用します。それ以外の場合は、ソフトウェアは以下のように指定されるオプションを使用して main を生成します。

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; 
}

 例 1: main で特定の関数を呼び出してから別の関数を呼び出す

 例 2: main で特定の関数を 10 回呼び出してから別の関数を呼び出す

参考

トピック