使用KLEE进行dynamic symbolic execution时，如何生成指定分支的测试用例？

方法一：在代码中添加klee_assume约束 #

这是最直接且稳定的方式，通过约束符号变量的取值范围，让KLEE只探索目标分支对应的路径。针对你的代码，修改如下：

#include <klee/klee.h>

int main() {
    int a = 0;
    klee_make_symbolic(&a, sizeof(a), "a");
    // 强制约束a等于0，直接排除其他分支的可能性
    klee_assume(a == 0);
    
    if (a == 0) 
        // 目标分支
        return 0;
    else if (a > 0)
        return 1;
    else
        return 2;
}

编译并运行KLEE后，只会生成满足a == 0的测试用例，其他分支会被直接跳过，不会生成对应的测试文件。

方法二：使用KLEE命令行选项过滤（兼容性有限） #

部分KLEE版本支持通过--constraint选项在命令行直接传入约束条件，比如：

klee --constraint "a == 0" your_program.bc

不过该选项的兼容性可能因KLEE版本而异，不如代码中添加klee_assume的方式通用。

如果只是想在生成全部用例后提取指定分支的用例，可以用klee-stats工具查看每个测试用例对应的路径，再从klee-last目录中复制对应的.ktest文件，但这种方式仍会先生成全部用例，不符合你不想生成全部的需求，因此优先推荐第一种方法。

内容的提问来源于stack exchange，提问作者bam