Re: [klee-dev] math.h functions interpreted as external

2021-01-26 Thread Cristian Cadar 

Hi Juan,

The warnings say that no implementation for these functions is 
available.  You should compile uclibc with support for these functions.


However, note that mainline KLEE does not have support for symbolic 
floating point operations, but there are a couple of (open-source but 
unmaintained) extensions of KLEE which do:

https://srg.doc.ic.ac.uk/publications/17-klee-n-version-fp-ase.html

Best,
Cristian

On 07/01/2021 10:26, juanfrancisco.garcia wrote:

I'm getting this warnings for all math.h functions,

KLEE: WARNING ONCE: calling external: floor(9221120237041090560)
KLEE: WARNING ONCE: calling external: round(0)

math.h is included, and if I change libc to uclibc I also get this 
warnings:


KLEE: WARNING: undefined reference to function: acos
KLEE: WARNING: undefined reference to function: atan2
KLEE: WARNING: undefined reference to function: ceil
KLEE: WARNING: undefined reference to function: cos
KLEE: WARNING: undefined reference to function: floor
KLEE: WARNING: undefined reference to function: round
KLEE: WARNING: undefined reference to function: sin
KLEE: WARNING: undefined reference to function: sqrt


Are math.h functions supported in klee?

I also tried with z3 solver that supports floating point, and it gives 
the same warnings.


Thanks in advance,
Juan Francisco García




___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] terminateStateOnExit never called

2021-01-26 Thread Frank Busse 
Hi,


On Tue, 26 Jan 2021 21:23:29 +0600
"Md. Hasanur Rahman"  wrote:

> When an execution path finishes with normal exit, is it supposed to
> call terminateStateOnExit? It seems it had never been called.

Yes.

If a test case is missing, there could be several reasons. Off the top
of my head:
1. you're using "--only-output-states-covering-new" and the path didn't
   cover new code
2. the path reaches an error that was already reported (you need
   --emit-all-errors)
3. the path hasn't finished yet or KLEE was interrupted
   (--dump-states-on-halt disabled or KLEE killed)

> I want to know this particular test case from KLEE

In case you have a bunch of ktest files you can replay them one by one
and look for the desired output (--replay-ktest-file=path/file.ktest
--only-replay-seeds).


Kind regards,

Frank

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] terminateStateOnExit never called

2021-01-26 Thread Md. Hasanur Rahman 
Hi,

When an execution path finishes with normal exit, is it supposed to call
terminateStateOnExit? It seems it had never been called.

The benchmark I am using is doing exit once (because it is printing
something that this benchmark is supposed to do) and I want to know this
particular test case from KLEE. How can I know this?

- Thanks
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev