From c2f3bf4b82cc98c35c42b51021a4b93605b296c4 Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Wed, 24 Feb 2021 11:37:11 +0100 Subject: [PATCH] [wp] Changed warning for terminates clause --- tests/bugs/oracle/term.res.oracle | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/tests/bugs/oracle/term.res.oracle b/tests/bugs/oracle/term.res.oracle index 9b5a7ccd..75a043ab 100644 --- a/tests/bugs/oracle/term.res.oracle +++ b/tests/bugs/oracle/term.res.oracle @@ -2,10 +2,12 @@ [kernel] Parsing tests/bugs/term.cpp (external front-end) Now output intermediate result [wp] Running WP plugin... -[wp] tests/bugs/term.cpp:49: Warning: - Ignored 'terminates' specification: - \true [wp] Warning: Missing RTE guards +[wp] tests/bugs/term.cpp:11: Warning: Terminates not implemented yet (skipped). +[wp] tests/bugs/term.cpp:17: Warning: Terminates not implemented yet (skipped). +[wp] tests/bugs/term.cpp:43: Warning: Terminates not implemented yet (skipped). +[wp] tests/bugs/term.cpp:26: Warning: Terminates not implemented yet (skipped). +[wp] tests/bugs/term.cpp:34: Warning: Terminates not implemented yet (skipped). [wp] 3 goals scheduled [wp] [Qed] Goal typed_Z2m2_ensures : Valid [wp] [Qed] Goal typed_Z2m3_c_ensures : Valid -- GitLab