0

我正在使用 Klee 2.9，并尝试从 stat 文件 klee 生成器获取分支信息。我输入了一个 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

两个可能的原因：

“klee_make_symbolic”和“printf”包含条件语句。当 KLEE 执行程序时，它不会将您的函数与外部函数区分开来。

如果您使用“--libc=uclibc”运行 KLEE，则主函数将替换为“__uclibc_main”。“__uclibc_main”先做一些初始化工作，然后调用原来的“main”函数。初始化可能包含一些条件语句。

您需要检查 KLEE 的版本和您使用的命令。

于 2015-09-30T15:54:26.303 回答