http://klee.llvm.org/是一个程序分析工具，它通过符号执行和约束求解来工作，找到可能导致程序崩溃的输入，并将其作为测试用例输出。这是一项非常令人印象深刻的工程，迄今为止已经产生了一些好的结果，包括在Unix实用程序的开源实现集合中发现了许多错误，这些实用程序被认为是有史以来测试最彻底的软件之一。
我的问题是:not做什么?
当然，任何这样的工具都有固有的限制，即它不能读懂用户的想法并猜测输出应该是什么。但撇开原则上不可能不说，大多数项目似乎还没有使用Klee;当前版本的限制是什么，它还不能处理哪些类型的错误和工作负载?
看完http://llvm.org/pubs/2008-12-OSDI-KLEE.html
它不能检查大程序的所有可能路径。它甚至在sort实用程序上也失败了。的问题是一个停止问题(不确定问题)，而KLEE是一个启发式的，因此它只能在有限的时间内检查一些路径。
它不能快速工作，根据论文，在COREUTILS中生成141000行代码的测试需要89小时(其中使用libc代码)。而最大的单个程序也只有~10000行。
它不知道浮点数，longjmp/setjmp, threads, asm;可变大小的内存对象
Update:/from llvm blog/http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html
5。LLVM"Klee"子项目使用符号分析在一段代码中"尝试每一条可能的路径"来找到代码中的bug，并生成一个测试用例。
这是一个很棒的小项目，主要是由于不适合在大规模应用程序上运行而受到限制。
Update2: KLEE要求修改程序。http://t1.minormatter.com/ddunbar/klee-doxygen overview.html
。符号内存是通过插入对KLEE(即klee_make_symbolic)的特殊调用来定义的。在执行过程中，KLEE跟踪符号内存的所有使用。
总的来说，KLEE应该是一个非常好的用于学术研究的符号执行引擎。在实际应用中，它可能受到以下几个方面的限制:
[1]在KLEE中LLVM IR解释器使用的内存模型非常消耗内存且耗时。对于每个执行路径，KLEE维护一个私有的"地址空间"。地址空间为局部变量维护一个"堆栈"，为全局变量和动态分配的变量维护一个"堆"。但是，每个变量(本地或全局)都包装在MemoryObject对象中(MemoryObject维护与该变量相关的元数据，例如起始地址、大小和分配信息)。每个变量使用的内存大小将是原始变量的大小加上MemoryObject对象的大小。当要访问一个变量时，KLEE首先搜索"地址空间"以找到相应的MemoryObject。KLEE将检查MemoryObject并查看访问是否合法。如果是，访问将完成，MemoryObject的状态将被更新。这样的内存访问显然比RAM慢。这样的设计可以很容易地支持符号价值的传播。然而，这个模型可以通过学习污点分析(标记变量的符号状态)来简化。
[2] KLEE缺乏系统环境的模型。在KLEE中建模的唯一系统组件是一个简单的文件系统。其他的，如套接字或多线程，则不受支持。当程序调用对这些非建模组件的系统调用时，KLEE要么(1)终止执行并引发警报，要么(2)将调用重定向到底层操作系统(问题:符号值需要具体化，并且会错过一些路径;来自不同执行路径的系统调用会相互干扰)。我想这就是上面提到的"一无所知线程"的原因。
[3] KLEE不能直接在二进制文件上工作。KLEE需要待测试程序的LLVM IR。而其他符号执行工具，如BitBlaze项目的S2E和VINE，可以在二进制文件上工作。有趣的是，S2E项目依赖于KLEE作为它的符号执行引擎。
对于以上答案，我个人有不同的看法。首先，KLEE确实不能完美地处理大范围程序，但是哪个符号执行工具可以呢?路径爆炸与其说是一个工程问题，不如说是一个理论开放问题。其次，正如我提到的，KLEE可能由于其内存模型而运行缓慢。然而，KLEE不会无缘无故地降低执行速度。它会保守地检查内存损坏(如缓冲区溢出)，并为每个执行的路径记录一组有用的信息(如路径输入的约束)。另外，我也不知道有其他的符号执行工具可以运行得非常快。第三，"浮点数，longjmp/setjmp，线程，asm;"可变大小的内存对象"只是工程工程。例如，KLEE的作者实际上做了一些事情使KLEE能够支持浮点数(http://srg.doc.ic.ac.uk/files/papers/kleefp-eurosys-11.pdf)。第三，KLEE并不一定需要程序上的工具来标记符号变量。如上所述，符号值可以通过命令行输入到程序中。实际上，用户也可以将文件指定为符号文件。如果需要，用户可以简单地配置库函数以使输入具有符号性(一劳永逸)。
我对Klee很失望，因为它没有任何内置的数据结构支持。Klee自己也不明白链表是什么。你不能用它来验证任何图形算法的实现。此外，它不能帮助捕获整数溢出错误，这是安全补丁的最重要来源。