--- layout: fc_discuss_archives title: Message 17 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



> 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)

I couldn't reproduce this with Frama-C Boron 20100401 (one of the
binary packages from http://frama-c.com including Why 2.26).

Here is the complete C file I used:

/*@ requires 0 < x <= 1000000000;
  ensures ((\result + 0.0) / 2 > x);
*/
int function1(int x) {
 return (2*x + 1);
}