From 38bef5b1aefd62cec9ce37385870372fc88d1a08 Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Thu, 10 Sep 2020 08:59:57 +0200 Subject: [PATCH] [wp-qualif] update oracles --- .../oracle_qualif/generalized_checks.res.oracle | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle index 1673f54ff07..4b3a0044393 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle @@ -4,7 +4,7 @@ [wp] Loading driver 'share/wp.driver' [wp] Warning: Missing RTE guards [wp] 17 goals scheduled -[wp] [Alt-Ergo] Goal typed_lemma_C_ko : Unsuccess +[wp] [Alt-Ergo] Goal typed_check_lemma_C_ko : Unsuccess [wp] [Alt-Ergo] Goal typed_lemma_L_ko : Unsuccess [wp] [Qed] Goal typed_caller_ensures_R : Valid [wp] [Alt-Ergo] Goal typed_caller_ensures_R1_ko : Unsuccess @@ -13,11 +13,11 @@ [wp] [Qed] Goal typed_caller_assigns_normal_part1 : Valid [wp] [Qed] Goal typed_caller_assigns_normal_part2 : Valid [wp] [Qed] Goal typed_caller_call_job_requires_A : Valid -[wp] [Qed] Goal typed_caller_call_job_requires_CA1 : Valid -[wp] [Alt-Ergo] Goal typed_caller_call_job_requires_CA2_ko : Unsuccess +[wp] [Qed] Goal typed_caller_call_job_check_requires_CA1 : Valid +[wp] [Alt-Ergo] Goal typed_caller_call_job_check_requires_CA2_ko : Unsuccess [wp] [Alt-Ergo] Goal typed_job_ensures_B : Valid -[wp] [Alt-Ergo] Goal typed_job_ensures_CB1 : Valid -[wp] [Alt-Ergo] Goal typed_job_ensures_CB2_ko : Unsuccess +[wp] [Alt-Ergo] Goal typed_job_check_ensures_CB1 : Valid +[wp] [Alt-Ergo] Goal typed_job_check_ensures_CB2_ko : Unsuccess [wp] [Qed] Goal typed_job_assigns_exit : Valid [wp] [Qed] Goal typed_job_assigns_normal_part1 : Valid [wp] [Qed] Goal typed_job_assigns_normal_part2 : Valid -- GitLab