Cristian,

Thank you.  I'll give it another try.

Thanks!
Brady J. Garvin

>
> Hi Brady, thanks for your email.  I just fixed the unittests problems.
> The other two test failures are due to some issues related to debug
> info, which Daniel should be able to fix soon.
>
> Cristian
>
> On 29/04/10 01:10, bgarvin at cse.unl.edu wrote:
>> 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
>>
>>
>>
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at keeda.stanford.edu
>> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>


Reply via email to