I observe that some of the test cases (for make check) do not all explicitly include all needed header files. I wonder if this is deliberate or just done as a convenience. It does not seem to be a good coding practice.
If it is deliberate (as a mechanism for creating fault conditions) it probably should be explicitly stated. In particular some of the invocations of void klee_make_symbolic(void *addr, size_t nbytes, const char *name); are missing the final argument. In C++ overloading should take care of things, the problem is that klee_make_symbolic is coded in C and without the signature, the compiler will not place the correct number of arguments on the stack. Perhaps this is deliberate, done as a mechanism for creating a fault conditions. There really is no way for anyone (other than the author if the test) to actually know the actual intent for certain. Comments Dave Lightstone
