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 e1e22036ebeeb00c2a9180ae68268033e3304f15..00dd592c9b80b78da3fd915dd5bff62123e68fa2 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% +------------------------------------------------------------