[klee-dev] Concretizing internal variables in coreutils experiment

Andrew Santosa asantosa1999 at gmail.com
Tue Jan 16 02:27:10 GMT 2018


Hi Charitha,
You can try to run the configure script of Coreutils in the following way:
CFLAGS=-I<klee_include_dir> LDFLAGS=-L<klee_lib_dir> LIBS=-lkleeRuntest ./configure <configure_options>

where <klee_lib_dir> is where libkleeRuntest.so* live. You may need to set LD_LIBRARY_PATH to <klee_lib_dir> for running the produced executable.
I hope this helps.
Andrew
 

    On Saturday, 13 January 2018, 7:59:35 am GMT+8, Charitha Saumya <cgusthin at purdue.edu> wrote:  
 
 Hi,

I want to use "klee_assume" inside some of the applications (say "echo") 
in coreutils.

For example I modified echo.c with following lines..

#include <klee/klee.h>

..

..

klee_assume(some_var == some_value);

..

..

I get a linker error when trying to compile modified coreutils using wllvm.

undefined reference to `klee_assume'
clang: error: linker command failed with exit code 1 (use -v to see 
invocation)

is there a workaround to solve this problem?

Thanks,
Charitha



_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
  
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list