[wp] Updates WP tests related to new default machdep

src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle

@@ -11,22 +11,22 @@ Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assertion 'a01' (file tests/wp_plugin/overflow2.c, line 20):
+Goal Assertion 'a01' (file tests/wp_plugin/overflow2.c, line 27):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assertion 'a02' (file tests/wp_plugin/overflow2.c, line 21):
+Goal Assertion 'a02' (file tests/wp_plugin/overflow2.c, line 28):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assertion 'a03' (file tests/wp_plugin/overflow2.c, line 22):
+Goal Assertion 'a03' (file tests/wp_plugin/overflow2.c, line 29):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assertion 'a04' (file tests/wp_plugin/overflow2.c, line 23):
+Goal Assertion 'a04' (file tests/wp_plugin/overflow2.c, line 30):
 Assume {
   Type: is_sint16(distance_0) /\ is_uint32(p1_off_0).
   (* Pre-condition *)
@@ -36,7 +36,7 @@ Prove: (p1_off_0 + to_uint16(distance_0)) <= 65545.
 
 ------------------------------------------------------------
 
-Goal Assertion 'a05' (file tests/wp_plugin/overflow2.c, line 24):
+Goal Assertion 'a05' (file tests/wp_plugin/overflow2.c, line 31):
 Let x = p1_off_0 + to_uint16(distance_0).
 Assume {
   Type: is_sint16(distance_0) /\ is_uint32(p1_off_0).
@@ -49,7 +49,7 @@ Prove: x = to_uint32(x).
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/overflow2.c, line 14) in 'pointers_and_companions':
+Goal Assigns (file tests/wp_plugin/overflow2.c, line 21) in 'pointers_and_companions':
 Prove: true.
 
 ------------------------------------------------------------
@@ -62,55 +62,45 @@ Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assertion 'a06' (file tests/wp_plugin/overflow2.c, line 39):
-Let x = p1_off_alt_0 + to_uint16(distance_0).
-Assume {
-  Type: is_sint16(distance_0) /\ is_uint64(p1_off_alt_0).
-  (* Pre-condition *)
-  Have: p1_off_alt_0 <= 10.
-}
-Prove: to_uint64(x) = to_uint32(x).
+Goal Assertion 'a06' (file tests/wp_plugin/overflow2.c, line 46):
+Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assertion 'a07' (file tests/wp_plugin/overflow2.c, line 40):
+Goal Assertion 'a07' (file tests/wp_plugin/overflow2.c, line 47):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assertion 'a08' (file tests/wp_plugin/overflow2.c, line 41):
+Goal Assertion 'a08' (file tests/wp_plugin/overflow2.c, line 48):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Assertion 'a09' (file tests/wp_plugin/overflow2.c, line 42):
-Let x = p1_off_alt_0 + to_uint16(distance_0).
+Goal Assertion 'a09' (file tests/wp_plugin/overflow2.c, line 49):
 Assume {
-  Type: is_sint16(distance_0) /\ is_uint64(p1_off_alt_0).
+  Type: is_sint16(distance_0) /\ is_uint32(p1_off_alt_0).
   (* Pre-condition *)
   Have: p1_off_alt_0 <= 10.
-  Have: to_uint64(x) = to_uint32(x).
 }
-Prove: x <= 65545.
+Prove: (p1_off_alt_0 + to_uint16(distance_0)) <= 65545.
 
 ------------------------------------------------------------
 
-Goal Assertion 'a10' (file tests/wp_plugin/overflow2.c, line 43):
+Goal Assertion 'a10' (file tests/wp_plugin/overflow2.c, line 50):
 Let x = p1_off_alt_0 + to_uint16(distance_0).
-Let x_1 = to_uint32(x).
 Assume {
-  Type: is_sint16(distance_0) /\ is_uint64(p1_off_alt_0).
+  Type: is_sint16(distance_0) /\ is_uint32(p1_off_alt_0).
   (* Pre-condition *)
   Have: p1_off_alt_0 <= 10.
-  Have: to_uint64(x) = x_1.
   (* Assertion 'a09' *)
   Have: x <= 65545.
 }
-Prove: x = x_1.
+Prove: x = to_uint32(x).
 
 ------------------------------------------------------------
 
-Goal Assigns (file tests/wp_plugin/overflow2.c, line 33) in 'pointers_and_companions_ulong':
+Goal Assigns (file tests/wp_plugin/overflow2.c, line 40) in 'pointers_and_companions_ulong':
 Prove: true.
 
 ------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/overflow2.c

+/* run.config
+   OPT: -machdep x86_32
+*/
+/* run.config_qualif
+   OPT: -machdep x86_32
+*/
+
 /* run with: frama-c-gui -wp -wp-rte strange_work_again.c */
 // uproven: a04, a05, a09, a10
 // note that when the type of distance is ushort, all is proven

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

@@ -7,31 +7,7 @@
 ------------------------------------------------------------
 
 Goal Post-condition (file tests/wp_typed/user_string.i, line 23) in 'strlen':
-Let x = ss_0.offset.
-Let x_1 = s.offset.
-Let x_2 = x - x_1.
-Let x_3 = s.base.
-Assume {
-  (* Heap *)
-  Type: (region(x_3) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Pre-condition *)
-  Have: P_Length_of_str_is(Malloc_0, Mchar_0, s, i).
-  (* Pre-condition *)
-  Have: P_Length_of_str_is(Malloc_0, Mchar_0, s, i_1).
-  (* Invariant 'ZERO' *)
-  Have: forall i_2 : Z. ((0 <= i_2) -> (((i_2 + x_1) < x) ->
-      (Mchar_0[shift_sint8(s, i_2)] != 0))).
-  (* Invariant 'RANGE' *)
-  Have: addr_le(s, ss_0) /\
-      addr_le(ss_0, shift_sint8(s, L_Length(Mchar_0, s))).
-  (* Invariant 'BASE' *)
-  Have: ss_0.base = x_3.
-  (* Else *)
-  Have: Mchar_0[ss_0] = 0.
-  (* Assertion 'END' *)
-  Have: P_Length_of_str_is(Malloc_0, Mchar_0, s, x_2).
-}
-Prove: P_Length_of_str_is(Malloc_0, Mchar_0, s, to_sint32(x_2)).
+Prove: true.
 
 ------------------------------------------------------------
 

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

@@ -7,31 +7,7 @@
 ------------------------------------------------------------
 
 Goal Post-condition (file tests/wp_typed/user_string.i, line 23) in 'strlen':
-Let x = ss_0.offset.
-Let x_1 = s.offset.
-Let x_2 = x - x_1.
-Let x_3 = s.base.
-Assume {
-  (* Heap *)
-  Type: (region(x_3) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
-  (* Pre-condition *)
-  Have: P_Length_of_str_is(Malloc_0, Mchar_0, s, i).
-  (* Pre-condition *)
-  Have: P_Length_of_str_is(Malloc_0, Mchar_0, s, i_1).
-  (* Invariant 'ZERO' *)
-  Have: forall i_2 : Z. ((0 <= i_2) -> (((i_2 + x_1) < x) ->
-      (Mchar_0[shift_sint8(s, i_2)] != 0))).
-  (* Invariant 'RANGE' *)
-  Have: addr_le(s, ss_0) /\
-      addr_le(ss_0, shift_sint8(s, L_Length(Mchar_0, s))).
-  (* Invariant 'BASE' *)
-  Have: ss_0.base = x_3.
-  (* Else *)
-  Have: Mchar_0[ss_0] = 0.
-  (* Assertion 'END' *)
-  Have: P_Length_of_str_is(Malloc_0, Mchar_0, s, x_2).
-}
-Prove: P_Length_of_str_is(Malloc_0, Mchar_0, s, to_sint32(x_2)).
+Prove: true.
 
 ------------------------------------------------------------
 

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

@@ -22,7 +22,7 @@
    assigns \nothing;
    ensures \exists integer i; Length_of_str_is(s,i) && \result == i;
  @*/
-int strlen(const char *s) {
+long long strlen(const char *s) {
   const char *ss = s;
   /*@
       loop invariant BASE: \base_addr(s) == \base_addr(ss) ;