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