http://klee.llvm.org/是一个程序分析工具，它通过符号执行和约束求解来工作，找到可能导致程序崩溃的输入，并将它们作为测试用例输出。这是一个非常令人印象深刻的工程，迄今为止已经产生了一些良好的结果，包括在 Unix 实用程序的开源实现集合中发现了许多错误，这些实用程序被认为是有史以来编写的一些经过最彻底测试的软件。
我的问题是：它不做什么？
当然，任何此类工具都有其固有的局限性，即它无法读取用户的想法并猜测输出应该是什么。但撇开原则上不可能的事不谈，大多数项目似乎还没有使用 Klee。当前版本的限制是什么，它还不能处理什么样的错误和工作负载？
正如我在阅读http://llvm.org/pubs/2008-12-OSDI-KLEE.html后所说的那样
它无法检查大程序的所有可能路径。sort它甚至在实用程序上也失败了。这个问题是一个停止问题（Undecidable problem），KLEE是一个启发式的，所以它只能在有限的时间内检查一些路径。
它不能快速工作，根据论文，它需要 89 小时才能为 CORUTILS 中的 141000 行代码生成测试（其中使用了 libc 代码）。最大的单个程序只有约 10000 行。
它对浮点、longjmp/setjmp、线程、asm一无所知；可变大小的内存对象。
更新：/来自 llvm 博客/ http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html
5. LLVM“Klee”子项目使用符号分析通过一段代码“尝试所有可能的路径”来查找代码中的错误并生成一个测试用例。这是一个很棒的小项目，主要受限于在大型应用程序上运行不实用。
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；可变大小的内存对象”只是工程。例如，http://srg.doc.ic.ac.uk/files/papers/kleefp-eurosys-11.pdf）。第三，KLEE 不一定需要对程序进行检测来标记符号变量。如上所述，符号值可以通过命令行输入到程序中。事实上，用户也可以将文件指定为符号。如果需要，用户可以简单地检测库函数以使输入符号化（一劳永逸）。