KLEE是如何计算分支机构数目的？

Question

我正在使用Klee2.9，并试图从stat文件Klee获取分支信息。我输入了一个if- fed语句程序，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 (“指令”、“全分支”、“部分分支”、“NumBranches”、“UserTime”、“NumState”、“MallocUsage”、“NumQueries”、“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执行程序时，它不会将您的函数与外部函数区分开来。

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

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