[wp] do not use stmt-contract

src/plugins/wp/tests/wp_typed/oracle/unit_tset.0.res.oracle

@@ -6,17 +6,20 @@
   Function complex
 ------------------------------------------------------------
 
-Goal Instance of 'Pre-condition (file tests/wp_typed/unit_tset.i, line 6) in 'job'' in 'complex' at call 'job' (file tests/wp_typed/unit_tset.i, line 20)
-:
+Goal Assigns (file tests/wp_typed/unit_tset.i, line 14) in 'complex':
+Call Effect at line 18
 Prove: true.
 
 ------------------------------------------------------------
-------------------------------------------------------------
-  Function complex with behavior default_for_stmt_2
+
+Goal Assigns (file tests/wp_typed/unit_tset.i, line 14) in 'complex':
+Call Effect at line 18
+Prove: true.
+
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_typed/unit_tset.i, line 19) at call 'job' (file tests/wp_typed/unit_tset.i, line 20):
-Call Effect at line 20
+Goal Instance of 'Pre-condition (file tests/wp_typed/unit_tset.i, line 2) in 'job'' in 'complex' at call 'job' (file tests/wp_typed/unit_tset.i, line 18)
+:
 Prove: true.
 
 ------------------------------------------------------------

src/plugins/wp/tests/wp_typed/oracle/unit_tset.1.res.oracle

@@ -6,17 +6,20 @@
   Function complex
 ------------------------------------------------------------
 
-Goal Instance of 'Pre-condition (file tests/wp_typed/unit_tset.i, line 6) in 'job'' in 'complex' at call 'job' (file tests/wp_typed/unit_tset.i, line 20)
-:
+Goal Assigns (file tests/wp_typed/unit_tset.i, line 14) in 'complex':
+Call Effect at line 18
 Prove: true.
 
 ------------------------------------------------------------
-------------------------------------------------------------
-  Function complex with behavior default_for_stmt_2
+
+Goal Assigns (file tests/wp_typed/unit_tset.i, line 14) in 'complex':
+Call Effect at line 18
+Prove: true.
+
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_typed/unit_tset.i, line 19) at call 'job' (file tests/wp_typed/unit_tset.i, line 20):
-Call Effect at line 20
+Goal Instance of 'Pre-condition (file tests/wp_typed/unit_tset.i, line 2) in 'job'' in 'complex' at call 'job' (file tests/wp_typed/unit_tset.i, line 18)
+:
 Prove: true.
 
 ------------------------------------------------------------

src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle

@@ -2,12 +2,13 @@
 [kernel] Parsing tests/wp_typed/unit_tset.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
-[wp] [Qed] Goal typed_complex_assigns : Valid
+[wp] 3 goals scheduled
+[wp] [Qed] Goal typed_complex_assigns_exit : Valid
+[wp] [Qed] Goal typed_complex_assigns_normal : Valid
 [wp] [Qed] Goal typed_complex_call_job_requires : Valid
-[wp] Proved goals:    2 / 2
-  Qed:             2
+[wp] Proved goals:    3 / 3
+  Qed:             3
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  complex                   2        -        2       100%
+  complex                   3        -        3       100%
 ------------------------------------------------------------

src/plugins/wp/tests/wp_typed/unit_tset.i

-/* run.config_qualif
-   OPT:
-*/
-
-/*@ 
-  requires \valid( p + (0..n-1) ); 
+/*@
+  requires \valid( p + (0..n-1) );
   assigns p[0..n-1];
  */
 void job(int *p,int n);
 
-typedef struct S {
+struct S {
   int size ;
   int value[50] ;
-} ;
+} s ;
 
-/*@ requires s.size < 50; */
-void complex(struct S s)
+/*@
+  requires s.size < 50;
+  assigns s.value[1..s.size];
+*/
+void complex(void)
 {
-  /*@ assigns s.value[1..s.size]; */
   job( & s.value[1] , s.size );
 }