0

私は Klee 2.9 を使用しており、stat ファイルの klee generators からブランチ情報を取得しようとしています。私は 1 つの if-else ステートメント プログラムを入力し、klee は NumBranches を 8 と報告しました。

テスト中のコードを以下に示します。

#include <stdio.h>
#include <stdbool.h>

int main(){
    int a;
    int b;
    klee_make_symbolic(&a,sizeof(a),"a");
    klee_make_symbolic(&b,sizeof(b),"b");
    if (a / b == 1) {
        printf("a==b\n");
    }
    else {
        printf("a!=b\n");   
    }
    return 0;
}

以下に示すファイル出力 run.stats ('Instructions','FullBranches','PartialBranches','NumBranches','UserTime','NumStates','MallocUsage','NumQueries','NumQueryConstructs','NumObjects' ,'WallTime','CoveredInstructions','UncoveredInstructions','QueryTime','SolverTime','CexCacheTime','ForkTime','ResolveTime',)

(0,0,0, 8 ,5.609000e-03,0,528704,0,0,0,4.196167e-05,0,78,0.000000e+00,0.000000e+00,0.000000e+00,0.000000e +00,0.000000e+00)

(32,2,0, 8,9.722000e -03,0,654176,3,56,0,3.826760e-01,27,51,3.799300e-01,3.802470e-01,3.801040e-01,6.900000e -05,0.000000e+00)

8がどのように由来するのか誰か説明できますか?

4

1 に答える 1

0

2 つの理由が考えられます。

「klee_make_symbolic」と「printf」には条件文が含まれています。KLEE がプログラムを実行するとき、関数は外部関数と区別されません。

"--libc=ulibc" で KLEE を実行すると、main 関数は "__ulibc_main" に置き換えられます。「__ulibc_main」は、最初にいくつかの初期化作業を行い、次に元の「main」関数を呼び出します。初期化には、いくつかの条件文が含まれる場合があります。

KLEE のバージョンと使用したコマンドを確認する必要があります。

于 2015-09-30T15:54:26.303 に答える