--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on August 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c-discuss Digest, Vol 63, Issue 2



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