Hi, If you search the "PATCH OF KLEE" http://keeda.stanford.edu/pipermail/klee-dev/attachments/20121007/6b3c595b/attachment-0001.obj for: add("klee_set_taint"
...you will see that it is handled in "klee/lib/Core/SpecialFunctionHandler.cpp". Thanks, Paul On 1 May 2013 12:51, Alexandru Ionut Diaconescu <[email protected]> wrote: > 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 ! > > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
