--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on August 2010 ---
> 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); }