--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on October 2013 ---
Pascal, I am sure you know that the default model in Jessie rules out special values (infinities and NaNs). This means two things: * for any FP operation it must be proved that no overflow occur (or equivalently that the result is not NaN nor infinity) * consequently, we can assumed safely that input FP data of any function is non-special. This is the case of the example given. I strongly believe this is the best model for 99.9% of programs, i.e except in very particular cases, special values should never show up in a program. - Claude PS: just for the braves who want to play with special values, Jessie has a model with special values #pragma JessieFloatModel(full) Le 07/10/2013 01:27, Pascal Cuoq a ?crit : > Do you expect the property to be provable or not? The program below > shows that it does not hold for typical C implementations with IEEE 754 > representations for floating-point types: > > $ cat d.c > #include <stdio.h> > > double a = 0. / 0.; > > int main(){ > double b = a; > printf("%d\n", a == b); > } > $ gcc d.c && ./a.out > 0 > > It would be considered a bug in Jessie if it generates, for the same > program property, a provable obligation for some provers and an > unprovable one for others. I would just like it to be clear whether, > with Jessie's default models regarding aliasing and floating-point, we > are looking for an issue with the Z3 output or with Alt-Ergo, CVC3, and > CVC4's. > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |