From a3b60b2768e6d884d25ff7ab56b81e5499d4609d Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 13 Mar 2019 16:42:51 +0100
Subject: [PATCH] [wp/tests] no more need of +cast for a test
---
src/plugins/wp/tests/wp_acsl/logic.i | 4 +-
.../wp/tests/wp_acsl/oracle/logic.res.oracle | 43 +++++++++---------
.../wp_acsl/oracle_qualif/logic.res.oracle | 44 +++++++++----------
3 files changed, 44 insertions(+), 47 deletions(-)
diff --git a/src/plugins/wp/tests/wp_acsl/logic.i b/src/plugins/wp/tests/wp_acsl/logic.i
index 2f8fa186d83..7a54adc27e1 100644
--- a/src/plugins/wp/tests/wp_acsl/logic.i
+++ b/src/plugins/wp/tests/wp_acsl/logic.i
@@ -1,8 +1,8 @@
/* run.config
- OPT: -wp-model Typed+cast
+ OPT: -wp-model Typed
*/
/* run.config_qualif
- OPT: -wp -wp-model Typed+cast -wp-steps 50
+ OPT: -wp -wp-model Typed -wp-steps 50
*/
// Test logic types defined from C types
//--------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
index 96e9d783dee..a3547cdccf7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/logic.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-model 'Typed (Cast)' [...]
+# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/logic.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
@@ -66,19 +66,18 @@ Let a = global(G_tr_31).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = global(G_buint_37).
-Let a_5 = shiftfield_F4_bytes(a_4).
+Let a_4 = shiftfield_F4_bytes(global(G_buint_37)).
Let m = Array1_S1(a_3, 3, Mint_0).
Assume {
- Type: is_uint32(Mint_0[a_4]) /\ IsArray1S1(m).
+ Type: IsArray1S1(m).
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 0)] = 1.
+ Init: Mint_0[shift_uint8(a_4, 0)] = 1.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 1)] = 2.
+ Init: Mint_0[shift_uint8(a_4, 1)] = 2.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 2)] = 4.
+ Init: Mint_0[shift_uint8(a_4, 2)] = 4.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 3)] = 8.
+ Init: Mint_0[shift_uint8(a_4, 3)] = 8.
(* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
@@ -103,19 +102,18 @@ Let a = global(G_tr_31).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = global(G_buint_37).
-Let a_5 = shiftfield_F4_bytes(a_4).
+Let a_4 = shiftfield_F4_bytes(global(G_buint_37)).
Let m = Array1_S1(a_3, 3, Mint_0).
Assume {
- Type: is_uint32(Mint_0[a_4]) /\ IsArray1S1(m).
+ Type: IsArray1S1(m).
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 0)] = 1.
+ Init: Mint_0[shift_uint8(a_4, 0)] = 1.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 1)] = 2.
+ Init: Mint_0[shift_uint8(a_4, 1)] = 2.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 2)] = 4.
+ Init: Mint_0[shift_uint8(a_4, 2)] = 4.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 3)] = 8.
+ Init: Mint_0[shift_uint8(a_4, 3)] = 8.
(* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
@@ -140,19 +138,18 @@ Let a = global(G_tr_31).
Let a_1 = shift___anonstruct_Point_1(a, 2).
Let a_2 = shift___anonstruct_Point_1(a, 1).
Let a_3 = shift___anonstruct_Point_1(a, 0).
-Let a_4 = global(G_buint_37).
-Let a_5 = shiftfield_F4_bytes(a_4).
+Let a_4 = shiftfield_F4_bytes(global(G_buint_37)).
Let m = Array1_S1(a_3, 3, Mint_0).
Assume {
- Type: is_uint32(Mint_0[a_4]) /\ IsArray1S1(m).
+ Type: IsArray1S1(m).
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 0)] = 1.
+ Init: Mint_0[shift_uint8(a_4, 0)] = 1.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 1)] = 2.
+ Init: Mint_0[shift_uint8(a_4, 1)] = 2.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 2)] = 4.
+ Init: Mint_0[shift_uint8(a_4, 2)] = 4.
(* Initializer *)
- Init: Mint_0[shift_uint8(a_5, 3)] = 8.
+ Init: Mint_0[shift_uint8(a_4, 3)] = 8.
(* Initializer *)
Init: Mint_0[shiftfield_F1_x(a_3)] = 10.
(* Initializer *)
@@ -238,7 +235,7 @@ Let a_4 = global(G_buint_37).
Let a_5 = shiftfield_F4_bytes(a_4).
Let a_6 = Load_S4(a_4, Mint_0).
Assume {
- Type: is_uint32(Mint_0[a_4]) /\ IsS4(a_6).
+ Type: IsS4(a_6).
(* Initializer *)
Init: Mint_0[shift_uint8(a_5, 0)] = 1.
(* Initializer *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
index 8f4e0382edf..225cf1c40b8 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-model 'Typed (Cast)' -wp-timeout 90 -wp-steps 50 [...]
+# frama-c -wp -wp-timeout 90 -wp-steps 50 [...]
[kernel] Parsing tests/wp_acsl/logic.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
@@ -35,27 +35,27 @@
[wp] tests/wp_acsl/logic.i:62: Warning:
Logic cast to struct (Tint2) from (int [6]) not implemented yet
[wp] 21 goals scheduled
-[wp] [Qed] Goal typed_cast_h_ensures : Valid
-[wp] [Qed] Goal typed_cast_h_assigns_exit : Valid
-[wp] [Qed] Goal typed_cast_h_assigns_normal : Valid
-[wp] [Qed] Goal typed_cast_main_requires_qed_ok : Valid
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_2 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_3 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_4 : Unsuccess
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_5 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_6 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_7 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_8 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_9 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_10 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_11 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_12 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_13 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_14 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_15 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_16 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_17 : Unsuccess (Stronger)
-[wp] [Alt-Ergo] Goal typed_cast_main_requires_qed_ok_18 : Unsuccess (Stronger)
+[wp] [Qed] Goal typed_h_ensures : Valid
+[wp] [Qed] Goal typed_h_assigns_exit : Valid
+[wp] [Qed] Goal typed_h_assigns_normal : Valid
+[wp] [Qed] Goal typed_main_requires_qed_ok : Valid
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_2 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_3 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_4 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_5 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_6 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_7 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_8 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_9 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_10 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_11 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_12 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_13 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_14 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_15 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_16 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_17 : Unsuccess (Stronger)
+[wp] [Alt-Ergo] Goal typed_main_requires_qed_ok_18 : Unsuccess (Stronger)
[wp] Proved goals: 4 / 21
Qed: 4
Alt-Ergo: 0 (unsuccess: 17)
--
GitLab