From d85fb03f379c75f2bd444e08a15a04ab4b104998 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 5 Jan 2022 14:02:01 +0100
Subject: [PATCH] [wp] Test flash: removed test

---
 .../tests/wp_plugin/oracle/flash.1.res.oracle | 237 +-----------------
 .../tests/wp_plugin/oracle/flash.2.res.oracle |  37 ---
 2 files changed, 5 insertions(+), 269 deletions(-)
 delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle

diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
index 77857dc55d0..f8d847b6ba4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/flash.1.res.oracle
@@ -1,7 +1,6 @@
 # frama-c -wp [...]
 [kernel] Parsing flash.c (with preprocessing)
 [wp] Running WP plugin...
-[wp] flash-ergo.driver:2: Warning: Redefinition of logic INDEX_init
 [wp] Warning: Missing RTE guards
 ------------------------------------------------------------
   Function job
@@ -13,252 +12,26 @@ Prove: true.
 ------------------------------------------------------------
 
 Goal Post-condition 'A_reads' in 'job':
-Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_64).
-Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_65).
-Let a_3 = C_RdAt_int(a_2).
-Let a_4 = C_WrAt_int(a_2).
-Let a_5 = Flash.update(Flash.init, a).
-Let a_6 = Flash.update(a_5, a_2).
-Let a_7 = Flash.update(a_6, a).
-Let x_1 = 1 + RD_time_0.
-Let x_2 = 1 + WR_time_0.
-Let x_3 = OBSERVER_time_0 - 1.
-Let x_4 = RD_time_0 - 1.
-Let a_8 = L_RD_current(x_4).
-Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
-Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_8, a_2)).
-Let x_8 = RD_time_0 - 2.
-Let x_9 = OBSERVER_time_0 - 3.
-Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
-Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
-Assume {
-  Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_5) /\
-      is_sint32(x_8) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
-      is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_6) /\
-      is_sint32(x_10) /\ is_sint32(x_11) /\ is_sint32(x_7) /\
-      is_sint32(x_6 + x_10 + x_11).
-  (* Pre-condition *)
-  Have: L_OBSERVER(x_9) = nil.
-  (* Pre-condition *)
-  Have: L_RD_current(x_8) = Flash.init.
-  (* Pre-condition *)
-  Have: L_WR_current(WR_time_0) = Flash.init.
-  (* Call 'RD' *)
-  Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      (x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
-  (* Call 'RD' *)
-  Have: (a_6 = L_RD_current(RD_time_0)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
-  (* Call 'WR' *)
-  Have: (L_WR_current(x_2) = Flash.update(Flash.init, a_2)) /\
-      (L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
-  (* Call 'RD' *)
-  Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
-      (a_7 = L_RD_current(x_1)).
-}
-Prove: Flash.get(a_7, a) = 2.
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Post-condition 'B_reads' in 'job':
-Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_64).
-Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_65).
-Let a_3 = C_RdAt_int(a_2).
-Let a_4 = C_WrAt_int(a_2).
-Let a_5 = Flash.update(Flash.init, a).
-Let a_6 = Flash.update(a_5, a_2).
-Let a_7 = Flash.update(a_6, a).
-Let x_1 = 1 + RD_time_0.
-Let x_2 = 1 + WR_time_0.
-Let x_3 = OBSERVER_time_0 - 1.
-Let x_4 = RD_time_0 - 1.
-Let a_8 = L_RD_current(x_4).
-Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
-Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_8, a_2)).
-Let x_8 = RD_time_0 - 2.
-Let x_9 = OBSERVER_time_0 - 3.
-Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
-Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
-Assume {
-  Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_5) /\
-      is_sint32(x_8) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x) /\
-      is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_6) /\
-      is_sint32(x_10) /\ is_sint32(x_11) /\ is_sint32(x_7) /\
-      is_sint32(x_6 + x_10 + x_11).
-  (* Pre-condition *)
-  Have: L_OBSERVER(x_9) = nil.
-  (* Pre-condition *)
-  Have: L_RD_current(x_8) = Flash.init.
-  (* Pre-condition *)
-  Have: L_WR_current(WR_time_0) = Flash.init.
-  (* Call 'RD' *)
-  Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      (x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
-  (* Call 'RD' *)
-  Have: (a_6 = L_RD_current(RD_time_0)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
-  (* Call 'WR' *)
-  Have: (L_WR_current(x_2) = Flash.update(Flash.init, a_2)) /\
-      (L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
-  (* Call 'RD' *)
-  Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
-      (a_7 = L_RD_current(x_1)).
-}
-Prove: Flash.get(a_7, a_2) = 1.
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Post-condition 'B_writes' in 'job':
-Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_64).
-Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_65).
-Let a_3 = C_RdAt_int(a_2).
-Let a_4 = C_WrAt_int(a_2).
-Let a_5 = Flash.update(Flash.init, a).
-Let a_6 = Flash.update(a_5, a_2).
-Let x_1 = 1 + WR_time_0.
-Let a_7 = Flash.update(Flash.init, a_2).
-Let x_2 = RD_time_0 - 1.
-Let x_3 = OBSERVER_time_0 - 1.
-Let x_4 = RD_time_0 - 2.
-Let a_8 = L_RD_current(x_4).
-Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
-Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_8, a_2)).
-Let x_8 = RD_time_0 - 3.
-Let x_9 = OBSERVER_time_0 - 3.
-Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
-Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
-Assume {
-  Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
-      is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
-      is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_6) /\ is_sint32(x_10) /\
-      is_sint32(x_11) /\ is_sint32(x_7) /\ is_sint32(x_6 + x_10 + x_11).
-  (* Pre-condition *)
-  Have: L_OBSERVER(x_9) = nil.
-  (* Pre-condition *)
-  Have: L_RD_current(x_8) = Flash.init.
-  (* Pre-condition *)
-  Have: L_WR_current(WR_time_0) = Flash.init.
-  (* Call 'RD' *)
-  Have: (a_8 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      (x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
-  (* Call 'RD' *)
-  Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
-  (* Call 'WR' *)
-  Have: (L_WR_current(x_1) = a_7) /\
-      (L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
-  (* Call 'RD' *)
-  Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
-      (Flash.update(a_6, a) = L_RD_current(RD_time_0)).
-}
-Prove: Flash.get(a_7, a_2) = 1.
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Post-condition 'ReadValues' in 'job':
-Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_64).
-Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_65).
-Let a_3 = C_RdAt_int(a_2).
-Let a_4 = C_WrAt_int(a_2).
-Let a_5 = Flash.update(Flash.init, a).
-Let a_6 = Flash.update(a_5, a_2).
-Let x_1 = 1 + WR_time_0.
-Let x_2 = RD_time_0 - 1.
-Let x_3 = OBSERVER_time_0 - 1.
-Let x_4 = RD_time_0 - 2.
-Let a_7 = L_RD_current(x_4).
-Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
-Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_7, a_2)).
-Let x_8 = RD_time_0 - 3.
-Let x_9 = OBSERVER_time_0 - 3.
-Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
-Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
-Let x_12 = x_6 + x_10 + x_11.
-Assume {
-  Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
-      is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
-      is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_6) /\ is_sint32(x_10) /\
-      is_sint32(x_11) /\ is_sint32(x_7) /\ is_sint32(x_12).
-  (* Pre-condition *)
-  Have: L_OBSERVER(x_9) = nil.
-  (* Pre-condition *)
-  Have: L_RD_current(x_8) = Flash.init.
-  (* Pre-condition *)
-  Have: L_WR_current(WR_time_0) = Flash.init.
-  (* Call 'RD' *)
-  Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      (x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
-  (* Call 'RD' *)
-  Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
-  (* Call 'WR' *)
-  Have: (L_WR_current(x_1) = Flash.update(Flash.init, a_2)) /\
-      (L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
-  (* Call 'RD' *)
-  Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
-      (Flash.update(a_6, a) = L_RD_current(RD_time_0)).
-}
-Prove: x_12 = (L_RD_value(a, 0) + L_RD_value(a, 1) + L_RD_value(a_2, 0)).
+Prove: true.
 
 ------------------------------------------------------------
 
 Goal Post-condition 'WriteValues' in 'job':
-Let x = 1 + OBSERVER_time_0.
-Let a = global(G_a_64).
-Let a_1 = C_RdAt_int(a).
-Let a_2 = global(G_b_65).
-Let a_3 = C_RdAt_int(a_2).
-Let a_4 = C_WrAt_int(a_2).
-Let a_5 = Flash.update(Flash.init, a).
-Let a_6 = Flash.update(a_5, a_2).
-Let x_1 = 1 + WR_time_0.
-Let x_2 = RD_time_0 - 1.
-Let x_3 = OBSERVER_time_0 - 1.
-Let x_4 = RD_time_0 - 2.
-Let a_7 = L_RD_current(x_4).
-Let x_5 = OBSERVER_time_0 - 2.
-Let x_6 = L_RD_value(a, Flash.get(Flash.init, a)).
-Let x_7 = x_6 + L_RD_value(a_2, Flash.get(a_7, a_2)).
-Let x_8 = RD_time_0 - 3.
-Let x_9 = OBSERVER_time_0 - 3.
-Let x_10 = L_RD_value(a_2, Flash.get(a_5, a_2)).
-Let x_11 = L_RD_value(a, Flash.get(a_6, a)).
-Assume {
-  Type: is_sint32(OBSERVER_time_0) /\ is_sint32(RD_time_0) /\
-      is_sint32(WR_time_0) /\ is_sint32(x_9) /\ is_sint32(x_8) /\
-      is_sint32(x_5) /\ is_sint32(x_4) /\ is_sint32(x_3) /\ is_sint32(x_2) /\
-      is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_6) /\ is_sint32(x_10) /\
-      is_sint32(x_11) /\ is_sint32(x_7) /\ is_sint32(x_6 + x_10 + x_11).
-  (* Pre-condition *)
-  Have: L_OBSERVER(x_9) = nil.
-  (* Pre-condition *)
-  Have: L_RD_current(x_8) = Flash.init.
-  (* Pre-condition *)
-  Have: L_WR_current(WR_time_0) = Flash.init.
-  (* Call 'RD' *)
-  Have: (a_7 = a_5) /\ (L_OBSERVER(x_5) = [ a_1 ]) /\
-      (x_7 = L_WR_value(a_2, Flash.get(Flash.init, a_2))).
-  (* Call 'RD' *)
-  Have: (a_6 = L_RD_current(x_2)) /\ (L_OBSERVER(x_3) = [ a_1, a_3 ]).
-  (* Call 'WR' *)
-  Have: (L_WR_current(x_1) = Flash.update(Flash.init, a_2)) /\
-      (L_OBSERVER(OBSERVER_time_0) = [ a_1, a_3, a_4 ]).
-  (* Call 'RD' *)
-  Have: (L_OBSERVER(x) = [ a_1, a_3, a_4, a_1 ]) /\
-      (Flash.update(a_6, a) = L_RD_current(RD_time_0)).
-}
-Prove: (L_RD_value(a, 0) + L_RD_value(a_2, 0)) = L_WR_value(a_2, 0).
+Prove: true.
 
 ------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle
deleted file mode 100644
index f8d847b6ba4..00000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle/flash.2.res.oracle
+++ /dev/null
@@ -1,37 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing flash.c (with preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: Missing RTE guards
-------------------------------------------------------------
-  Function job
-------------------------------------------------------------
-
-Goal Post-condition 'Events' in 'job':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition 'A_reads' in 'job':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition 'B_reads' in 'job':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition 'B_writes' in 'job':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition 'ReadValues' in 'job':
-Prove: true.
-
-------------------------------------------------------------
-
-Goal Post-condition 'WriteValues' in 'job':
-Prove: true.
-
-------------------------------------------------------------
-- 
GitLab