KLEE如何计算分支数量

Question

我正在使用Klee 2.9，并试图从统计文件Klee generats中获取分支信息。我输入了一个one-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==bn");
    }
    else {
        printf("a!=bn");   
    }
    return 0;
}

以及如下所示的文件输出run.stats，（‘指令’、‘FullBranches’、‘PartialBranches"、‘NumBranches‘、‘UserTime’、‘NumStates’、‘MallocUsage’、‘NumQueries’、’NumQueryConstructs‘、‘NumObjects’、‘AllTime’、’OveredInstructions‘、’UncoveredInstruction‘、’QueryTime‘、‘SolverTime‘、’ExCacheTime‘、'ForkTime‘、'ResolveTime‘）

（0,0,0，8，5.609000e-03,0528704,0,0,4.196167e-05,0,78,0.00000e+00,0.00000e+0,0.000000e+00,0000000e+0,0000000e+00,000000e+000）

（32,2,0，8，9.722000e-03,0654176,3,56,0,3.826760e-01,27,51,3.799300e-01,3.802470e-01,38.801040e-01,6.9000000e-05,0.00000e+00）

有人能解释一下8是怎么来的吗？

Answer 1

两个可能的原因：

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

如果使用"--libc=uclbc"运行KLEE，主函数将替换为"__uclbc_main"。"__uclac_main"首先做一些初始化工作，然后调用原始的"main"函数。初始化可能包含一些条件语句。

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