--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on June 2014 ---
Hello, (Currently) Alt-Ergo does not consider that "int" is a subtype of "real". This is why it says "typing error: real and int cannot be unified ". This should evolve with our new (experimental) input language based on SMT2. A workaround would be to introduce an explicit cast between int and real. - Mohamed. -- Senior R&D Engineer, OCamlPro Research Associate, VALS team, LRI. http://www.iguer.info Le 19/06/2014 09:19, Frank Dordowsky a ?crit : > > 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 > _______________________________________________ > 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