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 <qingyangcx2...@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@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
