--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on June 2014 ---
I am trying to introduce the rounding function axiomatically but my definition seems not to be sufficient. Here is my example: // file: round.h /*@ axiomatic Rounding { @ logic integer lround(real x); @ axiom rounded_value: @ \forall real x ; -0.5 <= (x - lround(x)) < 0.5; @ } @*/ /*@ requires 0.0 <= x <= 1000.0; @ ensures \result == lround(x); @*/ int roundit(float x); The implementation is as follows: // file: round.c #include "round.h" int roundit(float x) { return (int)(x+0.5); } When I try to prove this function with the float model (using Alt-Ergo), I get the following error: ------------------------------------------------------------ --- Alt-Ergo (stderr) : ------------------------------------------------------------ File "/tmp/wp067b74.dir/typed_ref_int_float/roundit_assert_3_Alt-Ergo.mlw", line 183, characters 23-47:typing error: real and int cannot be unified What is the reason for it, I have assumed that logic type integer is a subset of logic type real? When I replace the float model by the real model, there is no such error, but Alt-Ergo is not able to prove the post condition. I am probably overlooking something trivial, so thanks for your patience. Frank