[wp] removed stmt-contract

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

@@ -53,34 +53,6 @@ void by_array_in_code(int *p, int *q, int **qq) {
   p1[p2[0]]=*(p3+p4[*(p5+1)]);
 }
 //-------------------------------------------------------
-void by_value_in_code_annotation(int v, int *p, int*q) {
-  //@ assert tab[v-1]==0 && \initialized (&x6);
-  /*@ requires (x1?x2:x3)== 0;
-    @ assigns x4;
-    @*/
-  /*@ loop invariant x5<0;
-    @ loop variant q-p;
-    @*/
-  while (1)
-    //@ assert 0 == \let term=1+\at(x7,Pre) ; 1+term;
-    //@ assert \let pred=(x8==0) ; pred && x9==0;
-    ;
-}
-
-//@ behavior no_exit: exits \false;
-void by_reference_in_code_annotation(int*p) {
-  //@ for no_exit: assert \valid (p);
-  //@ ensures \separated (p1,p2) && \freeable (p3) || \allocable (p5) <==> \initialized (p6);
-  ;
-  //@ loop invariant *p4<0;
-  while (1);
-}
-
-void by_addr_in_code_annotation(void) {
-  //@ requires (&x0 != &s0.c) && &tab[5];
-  return;
-}
-
 void by_array_in_code_annotation(int *p, int *q, int **qq) {
   //@ assert *(ptr+1)==0 && *(p+1)==q[0] && p1[p2[0]]==*(p3+p4[*(p5+1)]);
   ;

src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle

 # frama-c -wp [...]
 [kernel] Parsing tests/wp_usage/code_spec.i (no preprocessing)
 [wp] Running WP plugin...
-[kernel] tests/wp_usage/code_spec.i:154: Warning: 
+[kernel] tests/wp_usage/code_spec.i:126: Warning: 
   No code nor implicit assigns clause for function by_addr_in_spec, generating default assigns from the prototype
-[kernel] tests/wp_usage/code_spec.i:154: Warning: 
+[kernel] tests/wp_usage/code_spec.i:126: Warning: 
   No code nor implicit assigns clause for function by_array_in_spec, generating default assigns from the prototype
 .................................................
 ... Ref Usage
@@ -16,10 +16,6 @@ Function by_value_in_code:
 Function by_reference_in_code: { *p1 *p *qq }
 Function by_addr_in_code: { &x0 &s0 &tab &v1 &s2 &s3 }
 Function by_array_in_code: { p1[] p2[] p3[] p4[] p5[] ptr[] p[] q[] }
-Function by_value_in_code_annotation:
-{ x1 x2 x3 x4 x5 x6 x7 x8 x9 tab v p q }
-Function by_reference_in_code_annotation: { *p1 *p2 *p3 *p4 *p5 *p6 *p }
-Function by_addr_in_code_annotation: { &x0 &s0 &tab }
 Function by_array_in_code_annotation:
 { p1[] p2[] p3[] p4[] p5[] ptr[] p[] q[] }
 Function by_value_in_spec: { x0 x1 p0 p1 p2 }
@@ -39,7 +35,5 @@ Function calling_spec:
 Function cup:
 { val *ref &addr array[] &addr_value val_ref array_ref[] value_array }
 .................................................
-[wp] [CFG] Goal by_addr_in_code_annotation_requires : Valid (Unreachable)
-[wp] [CFG] Goal by_reference_in_code_annotation_no_exit_exits : Valid (Unreachable)
 [wp] Warning: Missing RTE guards
 [wp] No proof obligations