Hi, KLEE is failing two test cases unexpectedly for me (running make check), and I am unable to run the unit tests because the makefile cannot locate the STP library. Before digging further, I wanted to be sure that I'm not making an obvious mistake, and, if not, ask for advice on where to look next.
Make check first complains that the grep for StaticDestructor.cpp finds no matches. A look at StaticDestructor.cpp.tmp1.log shows that the null dereference in the destructor is detected (``KLEE: ERROR: memory error: out of bound pointer''), however the expected pattern (``:16: memory error'') never occurs. I'm guessing that this is just a bug in the test suite. It next fails the test case on WriteCov.c; the coverage files are empty (zero bytes). That seems strange to me. Even stranger, make unittests gives me a linker error almost immediately, saying that it is unable to find -lstp. In KLEE's Release/lib directory there are many files matching libstp_*.a, but I can't discover anything nearer the mark. So I probably went wrong in the build process somewhere. As a sanity check, my results for the first tutorial are exactly those given on KLEE's site, up to differences due to the architecture change (such as instruction counts). If it is useful to know: I am running OpenSUSE 11.0 on an x86_64 processor. I built and tested klee for x86_64 by executing the following commands. The patch files mentioned are directly lifted from http://keeda.stanford.edu/pipermail/klee-dev/2009-October/000136.html. bash> export BASE=`pwd` bash> wget 'http://llvm.org/releases/2.6/llvm-gcc-4.2-2.6-x86_64-linux.tar.gz' bash> wget 'http://llvm.org/releases/2.6/llvm-2.6.tar.gz' bash> wget 'http://t1.minormatter.com/~ddunbar/klee-uclibc-0.01.tgz' bash> svn co http://llvm.org/svn/llvm-project/klee/trunk klee bash> tar xfz llvm-gcc-4.2-2.6-x86_64-linux.tar.gz bash> tar xfz llvm-2.6.tar.gz bash> tar xfz klee-uclibc-0.01.tgz bash> mv llvm-gcc-4.2-2.6-x86_64-linux llvm-gcc bash> mv llvm-2.6 llvm bash> export PATH=$BASE/llvm-gcc/bin:$BASE/llvm/Release/bin:$PATH bash> cd llvm bash> ./configure --enable-optimized bash> make bash> cd ../klee-uclibc bash> ./configure --with-llvm=$BASE/llvm bash> patch .config $BASE/config.patch bash> patch ./libc/stdlib/stdlib.c $BASE/stdlib.c.patch bash> patch ./libc/sysdeps/linux/i386/bits/kernel_types.h $BASE/i386_kernel_types.h.patch bash> patch ./libc/sysdeps/linux/x86_64/bits/kernel_types.h $BASE/x86_64_kernel_types.h.patch bash> make bash> cd ../klee bash> ./configure --with-llvm=$BASE/llvm --with-uclibc=$BASE/klee-uclibc --enable-posix-runtime bash> make ENABLE_OPTIMIZED=1 bash> export PATH=$BASE/klee/Release/bin:$PATH bash> export CPATH=$BASE/klee/include:$CPATH bash> export LIBRARY_PATH=$BASE/klee/Release/lib:$BASE/llvm/projects/sample/Release/lib:$BASE/llvm/Release/lib:$BASE/klee-uclibc/lib:$BASE/llvm-gcc/lib:$LIBRARY_PATH bash> make check bash> make unittests bash> cd examples/islower bash> cat islower.c bash> llvm-gcc --emit-llvm -c -g islower.c bash> klee islower.o bash> ktest-tool klee-last/test000001.ktest bash> ktest-tool klee-last/test000002.ktest bash> ktest-tool klee-last/test000003.ktest Thank you, Brady J. Garvin
