[wp] removed stmt-contract

src/plugins/wp/tests/wp_bts/nupw-bcl-bts1120.i

 /* run.config_qualif
-   OPT: -wp -wp-par 1 -wp-fct "g,unreachable_smt_with_contract"
+   OPT: -wp-fct "g"
 */
 
 /*@ axiomatic ax {
   @ predicate ExitF(integer x);
   @ predicate ExitP(integer x);
-  @ predicate Exit1(integer x);
-
   @ predicate PostF(integer x);
-  @ predicate PostP(integer x);
-  @ predicate Post1(integer x);
-
-  @ predicate P(integer x);
 
-  @ predicate PreF(integer x);
-  @ predicate Pre(integer x);
-  @ predicate Pre1(integer x);
 } */
 
 //@ assigns \nothing; ensures PostF(x); exits ExitF(x) ;
@@ -30,37 +21,3 @@ void g (int max) {
      tmp ++;
   }
 }
-
-//@ requires ok: x > 0 ; assigns \nothing;
-extern int f_with_precond (int x);
-
-// corrected.
-//@ requires PostP(max); ensures ok: PostP(max);
-void unreachable_smt_with_contract (int max) {
-  int tmp = f_with_precond(1);
-  goto L;
-  //@ requires ok: Pre1(max); assigns ok: tmp; ensures ok: Post1(max); exits ok: Exit1(max);
-  tmp = f_with_precond(-2);
-  //@ assert ok: P(tmp); 
-  tmp=3;
-  L:;
-}
-
-//@ assigns \nothing; exits never: \false;
-int f_no_exit(int) ;
-
-// corrected in stronger the PO (e1 is forgotten and is not provable *)
-//@ exits e:ExitP(0);
-int cfg_domination_problem (int max) {
-  int tmp=1;
-  if (max) {
-    tmp=f_no_exit(tmp);
-    goto L;
-  }
-  //@ assigns tmp; exits e1:ExitP(max);
-  {
-    tmp=f(max);
- L: tmp=3;
-  }
-  return tmp;
-}

src/plugins/wp/tests/wp_bts/oracle/nupw-bcl-bts1120.res.oracle

 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/nupw-bcl-bts1120.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] tests/wp_bts/nupw-bcl-bts1120.i:54: Warning: 
-  [cfg] Forget exits clause of node <blkIn-stmt:26>
-[wp] tests/wp_bts/nupw-bcl-bts1120.i:54: Warning: 
-  [cfg] Forget exits clause of node <blkIn-stmt:26>
-[wp] [CFG] Goal unreachable_smt_with_contract_assigns : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_exits_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_ensures_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_requires_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_assert_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_call_f_with_precond_requires_ok : Valid (Unreachable)
 [wp] Warning: Missing RTE guards
-------------------------------------------------------------
-  Function cfg_domination_problem
-------------------------------------------------------------
-
-Goal Exit-condition 'e' in 'cfg_domination_problem':
-Assume { (* Exit 'f' *) Have: P_ExitF(0). }
-Prove: P_ExitP(0).
-
-------------------------------------------------------------
-------------------------------------------------------------
-  Function cfg_domination_problem with behavior default_for_stmt_26
-------------------------------------------------------------
-
-Goal Assigns (file tests/wp_bts/nupw-bcl-bts1120.i, line 60) at block:
-Prove: true.
-
-------------------------------------------------------------
 ------------------------------------------------------------
   Function g
 ------------------------------------------------------------
@@ -54,27 +27,13 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'g' (2/3):
-Call Result at line 27
+Call Result at line 18
 Prove: true.
 
 ------------------------------------------------------------
 
 Goal Assigns nothing in 'g' (3/3):
-Effect at line 29
-Prove: true.
-
-------------------------------------------------------------
-------------------------------------------------------------
-  Function unreachable_smt_with_contract
-------------------------------------------------------------
-
-Goal Post-condition 'ok' in 'unreachable_smt_with_contract':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Instance of 'Pre-condition 'ok' in 'f_with_precond'' in 'unreachable_smt_with_contract' at initialization of 'tmp' (file tests/wp_bts/nupw-bcl-bts1120.i, line 40)
-:
+Effect at line 20
 Prove: true.
 
 ------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle

 # frama-c -wp [...]
 [kernel] Parsing tests/wp_bts/nupw-bcl-bts1120.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] [CFG] Goal unreachable_smt_with_contract_assigns : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_exits_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_ensures_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_requires_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_assert_ok : Valid (Unreachable)
-[wp] [CFG] Goal unreachable_smt_with_contract_call_f_with_precond_requires_ok : Valid (Unreachable)
 [wp] Warning: Missing RTE guards
-[wp] 8 goals scheduled
+[wp] 6 goals scheduled
 [wp] [Qed] Goal typed_g_exits_ok : Valid
 [wp] [Qed] Goal typed_g_loop_assigns : Valid
 [wp] [Qed] Goal typed_g_assigns_exit : Valid
 [wp] [Qed] Goal typed_g_assigns_normal_part1 : Valid
 [wp] [Qed] Goal typed_g_assigns_normal_part2 : Valid
 [wp] [Qed] Goal typed_g_assigns_normal_part3 : Valid
-[wp] [Qed] Goal typed_unreachable_smt_with_contract_ensures_ok_2 : Valid
-[wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_2_requires_ok : Valid
-[wp] Proved goals:   14 / 14
-  Qed:             8
+[wp] Proved goals:    6 / 6
+  Qed:             6
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   g                         6        -        6       100%
-  unreachable_smt_with_contract   2   -       2       100%
 ------------------------------------------------------------