--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on June 2014 ---
Thanks for the hints and the link. The blog is very impressive and was surprising to me, but I must admit that I did not yet delve too much into floating point analysis. Weakening the post-conditions leaves an ambiguity: if x == 3.5 for example, both 3 and 4 satisfy the predicate. I nevertheless modified my definition of lround, and also added another axiom that claims the existence of a function value: /*@ axiomatic Rounding { @ logic integer lround(real x); @ axiom exists_value: @ \forall real x; \exists integer n; lround(x) == n; @ axiom rounded_value: @ \forall real x ; -0.5 <= (x - lround(x)) <= 0.5; @ } @*/ I have also tried one of the implementation examples of the blog, and added some trivial assertions: // file: round.c #include "round.h" int roundit(float x) { //@ assert lround(3.0) == 3; //@ assert lround(3.1) == 3; //@ assert lround(3.5) == 4; //@ assert lround(3.9) == 4; if (x >= 0x1.0p23) return x; return (int)(x+0.49999997f); } I still cannot prove the post condition, but even the assertions are not proved, which surprises me, and I have no explanation for it. Frank