From de4f10b8ea0f37a209e9a5f524bf347e98424713 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 16 Feb 2021 14:59:15 +0100
Subject: [PATCH] [wp] pre-condition naming
---
.../wp_typed/oracle/user_bitwise.0.res.oracle | 16 ++++++++--------
.../tests/wp_typed/oracle/user_swap.0.res.oracle | 4 +++-
2 files changed, 11 insertions(+), 9 deletions(-)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
index 4e4f0bbf55a..ba38a185ae0 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
@@ -33,7 +33,7 @@ Assume {
Type: is_uint32(x) /\ is_sint32(n) /\ is_uint32(x_2).
(* Goal *)
When: (0 <= i) /\ (i < n) /\ is_sint32(i).
- (* Pre-condition *)
+ (* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 31).
}
Prove: (land(lor(to_uint32(lsl(x, n)), x_2), lsl(1, i)) != 0) <->
@@ -48,7 +48,7 @@ Assume {
Type: is_uint32(x) /\ is_sint32(n) /\ is_uint32(x_2).
(* Goal *)
When: (0 <= i) /\ (x_1 <= 31) /\ is_sint32(i).
- (* Pre-condition *)
+ (* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 31).
}
Prove: (land(lor(to_uint32(lsl(x, n)), x_2), lsl(1, x_1)) != 0) <->
@@ -66,7 +66,7 @@ Assume {
Type: is_sint32(n) /\ is_uint64(x) /\ is_uint64(x_2).
(* Goal *)
When: (0 <= i) /\ (i < n) /\ is_sint32(i).
- (* Pre-condition *)
+ (* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 63).
}
Prove: (land(lor(to_uint64(lsl(x, n)), x_2), lsl(1, i)) != 0) <->
@@ -81,7 +81,7 @@ Assume {
Type: is_sint32(n) /\ is_uint64(x) /\ is_uint64(x_2).
(* Goal *)
When: (0 <= i) /\ (x_1 <= 63) /\ is_sint32(i).
- (* Pre-condition *)
+ (* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 63).
}
Prove: (land(lor(to_uint64(lsl(x, n)), x_2), lsl(1, x_1)) != 0) <->
@@ -120,7 +120,7 @@ Assume {
Type: is_uint32(x) /\ is_sint32(n) /\ is_uint32(x_1).
(* Goal *)
When: (0 <= i) /\ (i < n) /\ is_sint32(i).
- (* Pre-condition *)
+ (* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 31).
}
Prove: (land(lor(x_1, to_uint32(lsl(x, 32 - n))), lsl(1, 32 + i - n)) != 0) <->
@@ -135,7 +135,7 @@ Assume {
Type: is_uint32(x) /\ is_sint32(n) /\ is_uint32(x_2).
(* Goal *)
When: (0 <= i) /\ (x_1 <= 31) /\ is_sint32(i).
- (* Pre-condition *)
+ (* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 31).
}
Prove: (land(lor(x_2, to_uint32(lsl(x, 32 - n))), lsl(1, i)) != 0) <->
@@ -153,7 +153,7 @@ Assume {
Type: is_sint32(n) /\ is_uint64(x) /\ is_uint64(x_1).
(* Goal *)
When: (0 <= i) /\ (i < n) /\ is_sint32(i).
- (* Pre-condition *)
+ (* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 63).
}
Prove: (land(lor(x_1, to_uint64(lsl(x, 64 - n))), lsl(1, 64 + i - n)) != 0) <->
@@ -168,7 +168,7 @@ Assume {
Type: is_sint32(n) /\ is_uint64(x) /\ is_uint64(x_2).
(* Goal *)
When: (0 <= i) /\ (x_1 <= 63) /\ is_sint32(i).
- (* Pre-condition *)
+ (* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 63).
}
Prove: (land(lor(x_2, to_uint64(lsl(x, 64 - n))), lsl(1, i)) != 0) <->
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle
index ed045c6b782..ae4e2e2a552 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_swap.0.res.oracle
@@ -35,7 +35,9 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ (region(b.base) <= 0) /\ linked(Malloc_0).
(* Pre-condition *)
- Have: valid_rw(Malloc_0, a, 1) /\ valid_rw(Malloc_0, b, 1).
+ Have: valid_rw(Malloc_0, a, 1).
+ (* Pre-condition *)
+ Have: valid_rw(Malloc_0, b, 1).
}
Prove: x_2 = x_1.
--
GitLab