--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on August 2013 ---
Hello Pierre, On 9 Aug 2013, at 12:02, frama-c-discuss-request at lists.gforge.inria.fr wrote: > int x = 0; > > /*@ requires y >= 0; > @ ensures \result > x; > @*/ > int f(int y) { return y +1; } in my opinion the function cannot be verified because the operation y+1 might overflow in which case the result can become negative. frama-c -cpp-command 'gcc -C -E -I.' -pp-annot -no-unicode -wp -wp-rte -wp-out f.wp f.c [kernel] preprocessing with "gcc -C -E -I. -dD f.c" [wp] Running WP plugin... [wp] Collecting axiomatic usage [rte] annotating function f [wp] 2 goals scheduled [wp] [Alt-Ergo] Goal typed_f_assert_rte_signed_overflow : Unknown [wp] [Alt-Ergo] Goal typed_f_post : Unknown Regards Jens