0

私は Z3 を初めて使用し、ここと Google で質問への回答を検索しました。私は成功しませんでした。

これは問題を引き起こすコードです:

void test(string str) {
    if (str [0] == 'g') {
        cout << "\"The first letter g" case"<< endl;
        if (str [1] == 'a') cout << "Second letter is 'a'";
        else cout << "Second letter is not 'a'";
    } else {
        cout << "The non-g case" << endl;
        if (str [1] == 'b') cout << "Second letter is 'b'";
        else cout << "Second letter is not 'b'";
    }
}

コードが最後まで実行されるように、入力データを自動的に生成する必要があります。z3でそれを行うことはまったく可能ですか? その場合、z3 C/C++API を使用してこれを行うにはどうすればよいですか?

4

2 に答える 2

1

Z3はテスト ケース ジェネレーターやファザーではなく、定理証明器です。ただし、Z3 はファザーとテストケース ジェネレーターの実装に使用されます。それらの 1 つは、.NET のホワイト ボックス ユニット テストであるPexです。Z3 は、x86 バイナリ用のホワイト ボックス ファザーであるSageでも使用されます。残念ながら、私は Z3 ベースの C++ 用のテスト ケース ジェネレーターを知りません。

于 2012-10-30T17:25:07.423 に答える
0

あなたの質問に直接答えるわけではありませんが、SAT/SMT ソルバーは以前にこのような「エクスプロイト」ベクトルを生成するために使用され、かなりの成功を収めています。たとえば、Brumley の AEG システムをチェックしてください: http://security.ece.cmu.edu/aeg/index.htmlなど。

于 2012-10-31T02:36:53.287 に答える