[klee-dev] failed external call

[Paul Thomson]

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
<alexandruionutdiaconescu at gmail.com> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>