Re: [klee-dev] KLEE unable to load a symbol

2016-05-27 Thread Marko Dimjašević
Hi Andrea, On Fri, 2016-05-27 at 18:47 +0100, Andrea Mattavelli wrote: > just to be sure that everything works as expected, have you tried to > run it (with your infrastructure) on Coreutils? Since we know that KLEE > works on those programs, it might be a good cross-checking experiment. It's

Re: [klee-dev] KLEE unable to load a symbol

2016-05-27 Thread Andrea Mattavelli
Hi Marko, just to be sure that everything works as expected, have you tried to run it (with your infrastructure) on Coreutils? Since we know that KLEE works on those programs, it might be a good cross-checking experiment. Best, Andrea > On 27 May 2016, at 18:44, Marko Dimjašević

Re: [klee-dev] KLEE unable to load a symbol

2016-05-27 Thread Marko Dimjašević
On Thu, 2016-05-26 at 15:30 -0600, Marko Dimjašević wrote: > For example, these files from the apt package have the same issue: > So I'd say the problem is quite common. I ran KLEE without making anything symbolic on over 30 Debian source packages and this really is a common problem. Pretty much

[klee-dev] Floating-Point Symbolic Execution

2016-05-27 Thread Andrew Santosa
Dear All, In KLEE, it seems symbolic floating point variables are simply converted to int and grounded to 0. I am wonderingwhat is the current state of floating point symbolic execution support in KLEE? I know there has been some workon KLEE-FP in the past, but does it actually check path