[wp] removed stmt-contract

src/plugins/wp/tests/wp_bts/issue_453.i

-typedef unsigned T;
-T incr_value;
-
-//@ axiomatic A { predicate Incr(T x, T r) = r == x + incr_value; }
-
-/*@ assigns \nothing;
-  @ ensures Incr(x, \result);
-  @ */
-T incr(T x);
-
-// Was KO before the fix of #453
-void f1(T i) {
-  /*@ loop assigns i;
-    @*/
-  while (i<10) {
-    /*@ assigns i ;
-       ensures Sincr: Incr(\old(i), i);
-      */
-    i = incr(i);
-  }
-}
-
-// Was OK before the fix of #453
-void f2(T i) {
-  /*@ loop assigns i;
-    @*/
-  while (i<10) {
-    //@ ghost A: ;
-    /*@ assigns i ;
-       ensures Sincr: Incr(\old(i), i);
-      */
-    i = incr(i);
-    //@ ghost B: ;
-  }
-}

src/plugins/wp/tests/wp_bts/oracle/issue_453.res.oracle

-# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_453.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-------------------------------------------------------------
-  Function f1
-------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_bts/issue_453.i, line 13):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
-  Function f1 with behavior default_for_stmt_7
-------------------------------------------------------------
-
-Goal Post-condition 'Sincr' at call 'incr' (file tests/wp_bts/issue_453.i, line 19):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_bts/issue_453.i, line 16) at call 'incr' (file tests/wp_bts/issue_453.i, line 19):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
-  Function f2
-------------------------------------------------------------
-
-Goal Loop assigns (file tests/wp_bts/issue_453.i, line 25):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
-  Function f2 with behavior default_for_stmt_17
-------------------------------------------------------------
-
-Goal Post-condition 'Sincr' at call 'incr' (file tests/wp_bts/issue_453.i, line 32):
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_bts/issue_453.i, line 29) at call 'incr' (file tests/wp_bts/issue_453.i, line 32):
-Prove: true.
-
-------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle

-# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_453.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] 6 goals scheduled
-[wp] [Qed] Goal typed_f1_loop_assigns : Valid
-[wp] [Qed] Goal typed_f1_ensures_Sincr : Valid
-[wp] [Qed] Goal typed_f1_assigns : Valid
-[wp] [Qed] Goal typed_f2_loop_assigns : Valid
-[wp] [Qed] Goal typed_f2_ensures_Sincr : Valid
-[wp] [Qed] Goal typed_f2_assigns : Valid
-[wp] Proved goals:    6 / 6
-  Qed:             6
-------------------------------------------------------------
- Functions                 WP     Alt-Ergo  Total   Success
-  f1                        3        -        3       100%
-  f2                        3        -        3       100%
-------------------------------------------------------------