http://klee.llvm.org/ is a program analysis tool that works by symbolic execution and constraint solving, finding possible inputs that will cause a program to crash, and outputting these as test cases. It's an extremely impressive piece of engineering that has produced some good results so far, including finding a number of bugs in a collection of open-source implementations of Unix utilities that had been considered among some of the most thoroughly tested software ever written.
My question is: what does it not do?
Of course, any such tool has the inherent limit that it can't read the user's mind and guess what the output was supposed to be. But leaving aside the in principle impossible, most projects don't yet seem to be using Klee; what are the limitations of the current version, what sort of bugs and workloads can it as yet not handle?