[klee-dev] failed external call

2013-05-01 Thread Alexandru Ionut Diaconescu
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*.

Re: [klee-dev] failed external call

2013-05-01 Thread 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

Re: [klee-dev] failed external call

2013-05-01 Thread Alexandru Ionut Diaconescu
I was trying again to use wget and patch but it seems it doesn't work. I will look for the warnings received during installation. Sorry for the beginner questions, I will try to solve it. ___ klee-dev mailing list klee-dev@imperial.ac.uk

Re: [klee-dev] failed external call

2013-05-01 Thread Daniel Liew
I'm not sure your patch is applying cleanly there but the bigger problem is that the configure step can't find the STP header file hence nothing can be built. Take a look at config.log (generated when running configure in the KLEE directory) for hints about what went wrong but it looks like

Re: [klee-dev] failed external call

2013-05-01 Thread Alexandru Ionut Diaconescu
Yes, that's why I was afraid for, the patch breaking the build. thank you a lot for the detailed information ! I will try and hope it works On Wed, May 1, 2013 at 4:05 PM, Daniel Liew daniel.l...@imperial.ac.ukwrote: I'm not sure your patch is applying cleanly there but the bigger problem is

[klee-dev] How to show (get) the negative values returned in klee's .pc files?

2013-05-01 Thread General Email
Hi, I need to understand how to use klee_assume and klee_assert. I tried to implement the following assumptions (in the function listed below) which assumed that if a symbolic variable x satisfies the condition !(0(x+5)) and that if another variable y is set to x+7, I want to check whether y is

Re: [klee-dev] How to show (get) the negative values returned in klee's .pc files?

2013-05-01 Thread General Email
Thanks Daniel, This is very helpful. So, my next question is how does klee generate such a condition based on the following set of commands?! klee_assume(!(0(x+5))); klee_assume(y==x+7); klee_assert(y0); I would appreciate if you provide me with some guidance of how klee_assume and