From 5555e04d00113bf4dd67b53a10964ef48ca8bcaf Mon Sep 17 00:00:00 2001 From: Patrick Baudin <patrick.baudin@cea.fr> Date: Fri, 29 Jan 2021 10:28:18 +0100 Subject: [PATCH] [WP] fixes a typo in a test. --- .../oracle_qualif/issue_A228.res.oracle | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/issue_A228.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/issue_A228.res.oracle index e1e22036ebe..00dd592c9b8 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/issue_A228.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/issue_A228.res.oracle @@ -1,11 +1,12 @@ # frama-c -wp [...] [kernel] Parsing tests/wp_acsl/issue_A228.c (with preprocessing) -[kernel] :0: - syntax error: - Location: between <unknown> and 1:5, before or at token: A - - 1 Bool A, B; - - 2 - 3 /*@ -[kernel] Frama-C aborted: invalid user input. +[wp] Running WP plugin... +[wp] Warning: Missing RTE guards +[wp] 1 goal scheduled +[wp] [Alt-Ergo] Goal typed_job_ensures_GOAL : Timeout (Qed:4ms) (10s) (missing cache) +[wp] Proved goals: 0 / 1 + Alt-Ergo: 0 (unsuccess: 1) +------------------------------------------------------------ + Functions WP Alt-Ergo Total Success + job - - 1 0.0% +------------------------------------------------------------ -- GitLab