From a9ca0bfbba02d20dace57c89901b540817246615 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 16 Feb 2021 15:08:43 +0100
Subject: [PATCH] [wp] fixed duplicated returns
---
.../wp/tests/wp_typed/oracle/array_initialized.0.res.oracle | 6 +++---
.../wp/tests/wp_typed/oracle/array_initialized.1.res.oracle | 6 +++---
src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle | 2 +-
src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle | 2 +-
4 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
index 478d90b93f1..8df4685c280 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.0.res.oracle
@@ -270,7 +270,7 @@ Prove: valid_rw(Malloc_0, p[i], 1).
Goal Post-condition (file tests/wp_typed/array_initialized.c, line 288) in 'simpl':
Let x = Mint_0[shift_sint32(t, 0)].
Assume {
- Type: is_sint32(x).
+ Type: is_sint32(simpl_0) /\ is_sint32(x).
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
@@ -279,8 +279,8 @@ Assume {
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 49) ->
(Mint_0[shift_sint32(t, i_1)] = x))).
If 0 <= x
- Then { (* Return *) Have: simpl_0 = 1. }
- Else { (* Return *) Have: simpl_0 = 0. }
+ Then { Have: simpl_0 = 1. }
+ Else { Have: simpl_0 = 0. }
}
Prove: (0 <= Mint_0[shift_sint32(t, i)]) <-> (simpl_0 = 1).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
index 91c35e494c2..4391ebbd55c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/array_initialized.1.res.oracle
@@ -273,7 +273,7 @@ Prove: valid_rw(Malloc_0, Mptr_0[shift_PTR(a, i)], 1).
Goal Post-condition (file tests/wp_typed/array_initialized.c, line 288) in 'simpl':
Let x = Mint_0[shift_sint32(t, 0)].
Assume {
- Type: is_sint32(x).
+ Type: is_sint32(simpl_0) /\ is_sint32(x).
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
@@ -282,8 +282,8 @@ Assume {
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 <= 49) ->
(Mint_0[shift_sint32(t, i_1)] = x))).
If 0 <= x
- Then { (* Return *) Have: simpl_0 = 1. }
- Else { (* Return *) Have: simpl_0 = 0. }
+ Then { Have: simpl_0 = 1. }
+ Else { Have: simpl_0 = 0. }
}
Prove: (0 <= Mint_0[shift_sint32(t, i)]) <-> (simpl_0 = 1).
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle
index 3df342a583b..48d804d0c82 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_rec.0.res.oracle
@@ -26,7 +26,7 @@ Goal Post-condition (file tests/wp_typed/user_rec.i, line 9) in 'F1':
Assume {
Type: is_sint32(F1_0) /\ is_sint32(i) /\ is_sint32(n).
If n <= 1
- Then { (* Return *) Have: F1_0 = 1. }
+ Then { Have: F1_0 = 1. }
Else {
(* Invariant *)
Have: L_fact(i - 1) = F1_0.
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle
index 14d0ebde9e9..7ee8668e53c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_rec.1.res.oracle
@@ -26,7 +26,7 @@ Goal Post-condition (file tests/wp_typed/user_rec.i, line 9) in 'F1':
Assume {
Type: is_sint32(F1_0) /\ is_sint32(i) /\ is_sint32(n).
If n <= 1
- Then { (* Return *) Have: F1_0 = 1. }
+ Then { Have: F1_0 = 1. }
Else {
(* Invariant *)
Have: L_fact(i - 1) = F1_0.
--
GitLab