--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on August 2010 ---
Pascal Cuoq schrieb: > ACSL uses promotion rules similar to that of C, but with integer and > real at the far end. And of course rationals are only real numbers > that happen to be the result of some division of integers. > > For some reason the syntax ((real)\result) is rejected. The error > message is "cannot cast to logic type" which is true but seems like a > bad excuse. Anyway, if you don't mind a slightly convoluted > expression, the following takes advantage of the implicit promotion > from integer to real to express what you mean: > > ensures (\result + 0.0) / 2 > x; > > I think? The Why file contains the corresponding goal: > > gt_real(div_real(add_real(real_of_int(integer_of_int32(result)), 0.0), > 2.0), > real_of_int(integer_of_int32(x)))) > > Regards, > > Pascal > > _______________________________________________ > 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 > The syntax ((real)\result) indeed gives the error "cannot cast to logic type" you mentioned. However when I tried (\result + 0.0), I get the following: "Fatal error: exception Assert_failure("cil/src/logic/logic_typing.ml", 763, 59) What am I doing wrong there?