--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on August 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Integer-arithmetics, rational postconditions



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?