From 6e68160ae6a23967667559fe21fa71f95dc24492 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Mon, 6 Jul 2020 19:24:39 +0200 Subject: [PATCH] update oracles --- tests/ppwp/oracle/expand.res.oracle | 1 - tests/ppwp/oracle/expandf.res.oracle | 1 - tests/ppwp/oracle/simple.res.oracle | 1 - tests/ppwp/oracle/z.res.oracle | 1 - 4 files changed, 4 deletions(-) diff --git a/tests/ppwp/oracle/expand.res.oracle b/tests/ppwp/oracle/expand.res.oracle index 258b33c6..51e6b1b0 100644 --- 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 */ diff --git a/tests/ppwp/oracle/expandf.res.oracle b/tests/ppwp/oracle/expandf.res.oracle index 69cf5301..b3239b7f 100644 --- 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 */ diff --git a/tests/ppwp/oracle/simple.res.oracle b/tests/ppwp/oracle/simple.res.oracle index 6812a5e8..80373643 100644 --- 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 */ diff --git a/tests/ppwp/oracle/z.res.oracle b/tests/ppwp/oracle/z.res.oracle index 36b86705..fbc8797c 100644 --- 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 */ -- GitLab