--- layout: fc_discuss_archives title: Message 48 from Frama-C-discuss on May 2009 ---
/*@ ensures \result >= 0.0; */ double sqr(double x) { return x * x; } 1/ A lot of work has been done on floating-point operations since the last release. That is to say, support for floating-point operations will be much less partial in the next release than in Lithium, both for Jessie and for the Value Analysis. 2/ With the value analysis you need to indicate that the property must be analyzed by case by adding an assertion x<=0 || x>=0, which does not incur any additional proof obligation since it can be verified to hold easily. The same trick may help automatic theorem provers, if you somehow arrange for this disjunction to be in the hypotheses, they may have the idea to study what that means for x*x separately. 3/ With both Jessie or the Value Analysis you will get a proof obligation. You will probably want to use the "strict" model in which infinites and NaN are treated as unwanted errors when they occur. In this case the proof obligation is that x*x should not overflow. Even with the Full model in Jessie your post-condition does not hold because NaN is not >=0 (the result can be NaN when the sqr function is applied to NaN). Pascal