Overall, KLEE should be a pretty good symbolic execution engine for academic research. For being used in practice, it could be limited by following aspects:
[1] The memory model used by the LLVM IR interpreter in KLEE is memory-consuming and time-consuming. For each execution path, KLEE maintains a private "address space". The address space maintains a "stack" for local variables and a "heap" for global variables and dynamically allocated variables. However, each variable (local or global) is wrapped in a MemoryObject object (MemoryObject maintain metadata related to this variable, such as the starting address, size, and allocation information). The size of memory used for each variable would be the size of the original variable plus the size of MemoryObject object. When an variable is to be accessed, KLEE firstly search the "address space" to locate the corresponding MemoryObject. KLEE would check the MemoryObject and see if the access is legitimate. If so, the access will be completed and state of the MemoryObject will be updated. Such memory access is obviously slower than RAM. Such a design can easily support the propagation of symbolic values. However, this model could be simplified via learning from taint analysis (labeling the symbolic status of variables).
[2] KLEE lacks models for system environments. The only system component modeled in KLEE is a simple file system. Others, such as sockets or multi-threading, are not supported. When a program invoke system calls to these non-modeled components, KLEE either (1) terminate the execution and raises an alert or (2) redirect the call to the underlying OS (Problems: symbolic values need to be concretized and some paths would be missed; system calls from different execution paths would interfere with each other). I suppose this is the reason for "it knowing nothing threads" as mentioned above.
[3] KLEE cannot directly work on binaries. KLEE requires LLVM IR of a to-be-tested program. While other Symbolic Execution tools, such as S2E and VINE from the BitBlaze project can work on binaries. An interesting thing is the S2E project relies on KLEE as its symbolic execution engine.
Regarding the above answer, I personally have different opinions. First, it's true that KLEE cannot perfectly work with large-scope programs, but which symbolic execution tool can? Path explosion is more a theoretical open problem instead of an engineering problem. Second, as I mentioned, KLEE might run slowly due to its memory model. However, KLEE does not slow down the execution for nothing. It conservatively checks memory corruptions (such as buffer overflow) and will log a set of useful information for each executed path (such as constraints on the inputs to follow a path). In addition, I did not know other symbolic execution tools that can run super fast. Third, "floating point, longjmp/setjmp, threads, asm; memory objects of variable size" are just engineering works. For example, the author of KLEE actually did something to enable KLEE to support floating point (http://srg.doc.ic.ac.uk/files/papers/kleefp-eurosys-11.pdf). Third, KLEE does not necessarily require instrumentation over the program to label symbolic variables. As mentioned above, symbolic values can be feed into the program via command lines. In fact, users can also specify files to be symbolic. If required, users can simply instrument the library functions to make inputs symbolic (once for all).
