KLEE如何计算分支数

Question

我正在使用 Klee 2.9，并试图从统计文件 klee generats 中获取分支信息。我输入了一个 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是怎么来的？

Answer 1

两个可能的原因：

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

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

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

KLEE如何计算分支数

How does KLEE count number of branches

klee