From ff6d0d73f3edbc43fd262f47ab97719ce4e90d3b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Mon, 18 Jul 2022 17:53:26 +0200 Subject: [PATCH] [report] update wp oracles --- src/plugins/report/tests/report/oracle/classify.0.res.oracle | 4 ++-- src/plugins/report/tests/report/oracle/classify.1.res.oracle | 4 ++-- src/plugins/report/tests/report/oracle/classify.2.res.oracle | 4 ++-- src/plugins/report/tests/report/oracle/classify.3.res.oracle | 4 ++-- src/plugins/report/tests/report/oracle/classify.4.res.oracle | 4 ++-- 5 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/plugins/report/tests/report/oracle/classify.0.res.oracle b/src/plugins/report/tests/report/oracle/classify.0.res.oracle index e6166cb1e51..19736779d85 100644 --- a/src/plugins/report/tests/report/oracle/classify.0.res.oracle +++ b/src/plugins/report/tests/report/oracle/classify.0.res.oracle @@ -5,8 +5,8 @@ [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] 2 goals scheduled -[wp] [Qed] Goal typed_f_assigns : Valid -[wp] [Qed] Goal typed_f_ensures : Valid +[wp] [Valid] typed_f_assigns (Qed) +[wp] [Valid] typed_f_ensures (Qed) [wp] Proved goals: 2 / 2 Qed: 2 [report] Classification diff --git a/src/plugins/report/tests/report/oracle/classify.1.res.oracle b/src/plugins/report/tests/report/oracle/classify.1.res.oracle index 0d9e671f1db..4f8eb215841 100644 --- a/src/plugins/report/tests/report/oracle/classify.1.res.oracle +++ b/src/plugins/report/tests/report/oracle/classify.1.res.oracle @@ -6,8 +6,8 @@ [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] 2 goals scheduled -[wp] [Qed] Goal typed_f_assigns : Valid -[wp] [Qed] Goal typed_f_ensures : Valid +[wp] [Valid] typed_f_assigns (Qed) +[wp] [Valid] typed_f_ensures (Qed) [wp] Proved goals: 2 / 2 Qed: 2 [report] Classification diff --git a/src/plugins/report/tests/report/oracle/classify.2.res.oracle b/src/plugins/report/tests/report/oracle/classify.2.res.oracle index 43a0913a194..2393e02477b 100644 --- a/src/plugins/report/tests/report/oracle/classify.2.res.oracle +++ b/src/plugins/report/tests/report/oracle/classify.2.res.oracle @@ -6,8 +6,8 @@ [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] 2 goals scheduled -[wp] [Qed] Goal typed_f_assigns : Valid -[wp] [Qed] Goal typed_f_ensures : Valid +[wp] [Valid] typed_f_assigns (Qed) +[wp] [Valid] typed_f_ensures (Qed) [wp] Proved goals: 2 / 2 Qed: 2 [report] Classification diff --git a/src/plugins/report/tests/report/oracle/classify.3.res.oracle b/src/plugins/report/tests/report/oracle/classify.3.res.oracle index 3e2df0958b0..897c0360e1b 100644 --- a/src/plugins/report/tests/report/oracle/classify.3.res.oracle +++ b/src/plugins/report/tests/report/oracle/classify.3.res.oracle @@ -7,8 +7,8 @@ [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] 2 goals scheduled -[wp] [Qed] Goal typed_f_assigns : Valid -[wp] [Qed] Goal typed_f_ensures : Valid +[wp] [Valid] typed_f_assigns (Qed) +[wp] [Valid] typed_f_ensures (Qed) [wp] Proved goals: 2 / 2 Qed: 2 [report] Classification diff --git a/src/plugins/report/tests/report/oracle/classify.4.res.oracle b/src/plugins/report/tests/report/oracle/classify.4.res.oracle index 70a9452ce06..359e58337ce 100644 --- a/src/plugins/report/tests/report/oracle/classify.4.res.oracle +++ b/src/plugins/report/tests/report/oracle/classify.4.res.oracle @@ -7,8 +7,8 @@ [wp] Running WP plugin... [wp] Warning: Missing RTE guards [wp] 2 goals scheduled -[wp] [Qed] Goal typed_f_assigns : Valid -[wp] [Qed] Goal typed_f_ensures : Valid +[wp] [Valid] typed_f_assigns (Qed) +[wp] [Valid] typed_f_ensures (Qed) [wp] Proved goals: 2 / 2 Qed: 2 [report] Classification -- GitLab