[wp] removed stmt-contract

src/plugins/wp/tests/wp_usage/core.i

-/* run.config
-   OPT: -wp-no-core
-   OPT: -wp-core
-*/
-
-/* run.config_qualif
-   DONTRUN:
-*/
-
-int a,b,c,x;
-//@ predicate OBS(integer x,integer y);
-//@ ensures OBS(\old(x),x);
-void f(void)
-{
-  if (a)
-    //@ ensures x == \old(x);
-    a++;
-  if (b) 
-    //@ ensures x == \old(x);
-    b++;
-  x++;
-  if (c)
-    //@ ensures x == \old(x);
-    c++;
-}

src/plugins/wp/tests/wp_usage/oracle/core.0.res.oracle

-# frama-c -wp [...]
-[kernel] Parsing tests/wp_usage/core.i (no preprocessing)
-[kernel] tests/wp_usage/core.i:11: Warning: 
-  parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] tests/wp_usage/core.i:24: Warning: 
-  Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_usage/core.i:20: Warning: 
-  Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_usage/core.i:17: Warning: 
-  Missing assigns clause (assigns 'everything' instead)
-------------------------------------------------------------
-  Function f
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_usage/core.i, line 12) in 'f':
-Assume {
-  Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(x) /\
-      is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3).
-  If a != 0
-  Then { Have: x_3 = x. }
-  Else { Have: x_3 = x. }
-  If b != 0
-  Then { Have: x_3 = x_2. }
-  Else { Have: x_3 = x_2. }
-  If c != 0
-  Then { Have: (1 + x_2) = x_1. }
-  Else { Have: (1 + x_2) = x_1. }
-}
-Prove: P_OBS(x, x_1).
-
-------------------------------------------------------------
-------------------------------------------------------------
-  Function f with behavior default_for_stmt_15
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_usage/core.i, line 23) at instruction (file tests/wp_usage/core.i, line 24):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
-  Function f with behavior default_for_stmt_4
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_usage/core.i, line 16) at instruction (file tests/wp_usage/core.i, line 17):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
-  Function f with behavior default_for_stmt_9
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_usage/core.i, line 19) at instruction (file tests/wp_usage/core.i, line 20):
-Prove: true.
-
-------------------------------------------------------------

src/plugins/wp/tests/wp_usage/oracle/core.1.res.oracle

-# frama-c -wp [...]
-[kernel] Parsing tests/wp_usage/core.i (no preprocessing)
-[kernel] tests/wp_usage/core.i:11: Warning: 
-  parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-[wp] tests/wp_usage/core.i:24: Warning: 
-  Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_usage/core.i:20: Warning: 
-  Missing assigns clause (assigns 'everything' instead)
-[wp] tests/wp_usage/core.i:17: Warning: 
-  Missing assigns clause (assigns 'everything' instead)
-------------------------------------------------------------
-  Function f
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_usage/core.i, line 12) in 'f':
-Let x_1 = 1 + x.
-Assume {
-  Type: is_sint32(a) /\ is_sint32(b) /\ is_sint32(c) /\ is_sint32(x) /\
-      is_sint32(x_1).
-}
-Prove: P_OBS(x, x_1).
-
-------------------------------------------------------------
-------------------------------------------------------------
-  Function f with behavior default_for_stmt_15
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_usage/core.i, line 23) at instruction (file tests/wp_usage/core.i, line 24):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
-  Function f with behavior default_for_stmt_4
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_usage/core.i, line 16) at instruction (file tests/wp_usage/core.i, line 17):
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
-  Function f with behavior default_for_stmt_9
-------------------------------------------------------------
-
-Goal Post-condition (file tests/wp_usage/core.i, line 19) at instruction (file tests/wp_usage/core.i, line 20):
-Prove: true.
-
-------------------------------------------------------------