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



It seems it was because of and older version of frama-c or why (I used 
the one from the Ubuntu-repositories). I now compiled to most recent 
version from the website, and it works.
Thanks a lot.


Pascal Cuoq schrieb:
> 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);
> }
>
> _______________________________________________
> 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
>