Hi guys,

It seems that there are still some problems with floating point, I came across 
the following assertion failures while running the dd coreutil with the 
parameters used for the OSDI paper:

klee: 
/home/ubuntu/cloud9/klee-liviu/include/klee/Internal/Support/FloatEvaluation.h:242:
 uint64_t klee::floats::UnsignedIntToFP(uint64_t, unsigned int): Assertion `0 
&& "invalid floating point width"' failed.
klee: /home/ubuntu/cloud9/klee-liviu/include/klee/Expr.h:324: uint64_t 
klee::ConstantExpr::getZExtValue(unsigned int) const: Assertion `getWidth() <= 
bits && "Value may be out of range!"' failed.

It would be great if you could look into this!

Thanks,
Liviu

Reply via email to