From fb5c630301ff43e35ed62ab0f1a6ef5d9f5a0e62 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 11 Jul 2022 12:16:16 +0200
Subject: [PATCH] [wp/tests] changed dry-run oracles (generated only)
---
src/plugins/wp/register.ml | 2 +-
src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle | 6 +++---
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 06d51a31f71..c9595b57314 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -369,7 +369,7 @@ let do_wpo_success ~shell ~updating goal success =
| None -> ()
| Some prover ->
Wp_parameters.feedback ~ontty:`Silent
- "[%a] Goal %s : Valid" VCS.pp_prover prover (Wpo.get_gid goal)
+ "[Generated] Goal %s (%a)" (Wpo.get_gid goal) VCS.pp_prover prover
else
if Wpo.is_smoke_test goal then
begin match success with
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
index a83d4680fb0..366ce220726 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/boolean.res.oracle
@@ -3,9 +3,9 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
-[wp] [Qed] Goal typed_u8_is_continue_assigns_part3 : Valid
-[wp] [Qed] Goal typed_u8_is_continue_assigns_part2 : Valid
-[wp] [Qed] Goal typed_u8_is_continue_assigns_part1 : Valid
+[wp] [Generated] Goal typed_u8_is_continue_assigns_part3 (Qed)
+[wp] [Generated] Goal typed_u8_is_continue_assigns_part2 (Qed)
+[wp] [Generated] Goal typed_u8_is_continue_assigns_part1 (Qed)
[wp] 4 goals generated
------------------------------------------------------------
Function u8_is_continue
--
GitLab