[klee-dev] failed external call

Alexandru Ionut Diaconescu alexandruionutdiaconescu at gmail.com
Wed May 1 12:51:54 BST 2013


Hello everyone,

I am trying to use the taint analysis from the following project:
http://cs.famaf.unc.edu.ar/~rcorin/kleecrypto/ . They have a KLEE program
that is doing taint analysis, it is in the examples folder.

I receive the following KLEE error : *failed external call:
klee_set_pc_taint*. In my entire KLEE "root" folder, klee_set_pc_taint
appears only in their .c program:
*#define TEST(x) { printf("testing " #x " \n"); klee_set_pc_taint(0);
test_##x(); }*
by using the linux command grep -r "klee_set_pc_taint" *
So it is defined only there (not appearing in any header file).

My question is : klee_set_pc_taint is
*1.* their own definition, only in the .c file and it is a problem with the
project program
*2.* It should be defined in the *klee/Release+Asserts/lib* folder, where I
had another problem. I was able to install KLEE, but when I was trying to
run the taint analysis example, it failed requiring for *
klee/Release+Asserts/lib/libkleeRuntimeIntrinsic.bca* , which was not in
the folder. So I renamed the libkleeRuntimeIntrinsic.a file to
libkleeRuntimeIntrinsic.bca and the problem was apparently removed. Maybe
this has any link with their own defined klee_set_pc_taint ? I suppose I
set up good the PATH with llvm-gcc, since I had no problems with building.

Thank for your any advice !
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list