[klee-dev] use klee-fp support float

[Chengyu Zhang]

Hi，
KLEE can't deal with the float in this version. KLEE will convert float to const when meet float.
Because of the limited of STP solver (can't deal with the float constraints) , the develop group of KLEE is trying to add Z3 solver support in KLEE. But the feature have not completed yet.

Best,
Chengyu

2016年12月30日 +0800 07:01 Cx Qingyang <qingyangcx2015 at gmail.com>，写道：
> Hi,I have successfully build klee-fp,but i don't know how to make it support float.For example,in the get_sign.c,i change the int x to
> float x.Firstly klee-gcc.cde -I ../../include -emit-llvm -c -g get_sign.c,then klee.cde get_sign.o,and i get a warning :silently concretizing expression(ReadLSB w32 0 a) to value 0.
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
HTML attachment scrubbed and removed