update oracles

6e68160a · Virgile Prevosto · 742450a6 · 6e68160a · 6e68160a · 6e68160a
Commit 6e68160a authored 4 years ago by Virgile Prevosto
--- a/tests/ppwp/oracle/expand.res.oracle
+++ b/tests/ppwp/oracle/expand.res.oracle
@@ -4,7 +4,6 @@ Now output intermediate result
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_Z1m_ensures : Valid
-[wp] [Cache] not used
 [wp] Proved goals:    1 / 1
  Qed:             1
 /* Generated by Frama-C */

--- a/tests/ppwp/oracle/expandf.res.oracle
+++ b/tests/ppwp/oracle/expandf.res.oracle
@@ -4,7 +4,6 @@ Now output intermediate result
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_Z1m_ensures : Valid
-[wp] [Cache] not used
 [wp] Proved goals:    1 / 1
  Qed:             1
 /* Generated by Frama-C */

--- a/tests/ppwp/oracle/simple.res.oracle
+++ b/tests/ppwp/oracle/simple.res.oracle
@@ -4,7 +4,6 @@ Now output intermediate result
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_Z1m_ensures : Valid
-[wp] [Cache] not used
 [wp] Proved goals:    1 / 1
  Qed:             1
 /* Generated by Frama-C */

--- a/tests/ppwp/oracle/z.res.oracle
+++ b/tests/ppwp/oracle/z.res.oracle
@@ -4,7 +4,6 @@ Now output intermediate result
 [wp] Warning: Missing RTE guards
 [wp] 1 goal scheduled
 [wp] [Qed] Goal typed_Z1m_ensures : Valid
-[wp] [Cache] not used
 [wp] Proved goals:    1 / 1
  Qed:             1
 /* Generated by Frama-C */