From b4a832901a0c4b5ada73a001f90b1bba45ee72bb Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 10 Dec 2020 16:51:57 +0100
Subject: [PATCH] [wp] Updates WP tests related to new default machdep
---
.../wp_plugin/oracle/overflow2.res.oracle | 44 +++++++------------
src/plugins/wp/tests/wp_plugin/overflow2.c | 7 +++
.../wp_typed/oracle/user_string.0.res.oracle | 26 +----------
.../wp_typed/oracle/user_string.1.res.oracle | 26 +----------
src/plugins/wp/tests/wp_typed/user_string.i | 2 +-
5 files changed, 27 insertions(+), 78 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
index bbd22a05eec..b0e1722d9dc 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/overflow2.res.oracle
+++ b/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.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/overflow2.c b/src/plugins/wp/tests/wp_plugin/overflow2.c
index f2a27e3b194..da847d4d356 100644
--- a/src/plugins/wp/tests/wp_plugin/overflow2.c
+++ b/src/plugins/wp/tests/wp_plugin/overflow2.c
@@ -1,3 +1,10 @@
+/* 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
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle
index 2da8a610645..f6ac9a650ae 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_string.0.res.oracle
+++ b/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.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle
index ed81e6ce070..b0256f00b0c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_string.1.res.oracle
+++ b/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.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/user_string.i b/src/plugins/wp/tests/wp_typed/user_string.i
index ccadee77578..228942a2a37 100644
--- a/src/plugins/wp/tests/wp_typed/user_string.i
+++ b/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) ;
--
GitLab