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

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

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

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

main 関数の生成

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

オプション	説明
アプリケーション全体の検証	ソフトウェアによって main が検出されないと検証が停止します。
モジュールまたはライブラリの検証 (-main-generator)	検証の前に、Polyspace はコードに main 関数が含まれているかどうかをチェックします。 main 関数が存在する場合、ソフトウェアはその main を使用します。それ以外の場合は、ソフトウェアは以下のように指定されるオプションを使用して main を生成します。 初期化する変数 (-main-generator-writes-variables) 初期化関数 (-functions-called-before-main) 呼び出す関数 (-main-generator-calls)

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 で特定の関数を呼び出してから別の関数を呼び出す

次のプロトタイプをもつ関数 func1 と関数 func2 の 2 つについて検証するとします。

int func1(void *ptr, int x);
void func2(int x, int y);

func1 は必ず func2 より先に呼び出されなければならないという要件があります。

この動作をモデル化する main を手動で定義するには、次の手順に従います。

1. 関数のパラメーター タイプごとに volatile 変数の宣言を含む main を作成します。

2. volatile 終了条件のループを作成します。

   検証では、変数 volatile がその型に許容される任意の値を取る可能性があると仮定されます。ループは任意の実行の後に終了する可能性があるため、この条件で func1 と func2 を任意の回数呼び出すことをモデル化します。

3. このループ内で、func1 を呼び出してから func2 を呼び出します。

以下の main を記述できます。

void main()
{
    volatile int random=0; 
    volatile void * volatile ptr;
    while(random) 
    {
        random = func1(ptr, random);
        func2(random, random); 
    }
}

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

次のプロトタイプをもつ関数 func1 と関数 func2 の 2 つについて検証するとします。

void func1(int);
void func2(void);

func1 と func2 の両方が呼び出されるときは、常に func1 が 10 回呼び出されてから func2 が呼び出されることがわかっています。

この動作をモデル化する main を手動で定義するには、次の手順に従います。

1. 関数のパラメーター タイプごとに volatile 変数の宣言を含む main を作成します。

2. main 関数で、func1 をループで 10 回呼び出してから func2 を呼び出します。

たとえば、main を次のように記述できます。

void main(void) {
    int i=0;
    volatile int random=0;
    
    while (++i <= 10)
        func1(random);

    func2();

}

参考

トピック

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