From eae625934ac0282a520d0f0e4d0ed5d9e1be8eba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Mon, 25 Feb 2019 11:45:01 +0100 Subject: [PATCH] [wp] validating output of all tests --- src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle | 3 ++- .../wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle | 3 ++- .../wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle | 5 +++-- .../wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle | 3 ++- .../wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle | 3 ++- src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle | 5 +++-- .../wp/tests/wp/oracle_qualif/wp_strategy.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle | 3 ++- .../tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle | 3 ++- .../tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle | 3 ++- .../wp_acsl/oracle_qualif/classify_float.0.res.oracle | 5 +++-- .../wp_acsl/oracle_qualif/classify_float.1.res.oracle | 3 ++- .../wp_acsl/oracle_qualif/classify_float.2.res.oracle | 3 ++- src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle | 3 ++- src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/equal.res.oracle | 7 ++++--- .../tests/wp_acsl/oracle_qualif/float_compare.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle | 3 ++- .../wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle | 3 ++- .../tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle | 3 ++- .../tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle | 3 ++- .../tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/logic.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle | 3 ++- src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/range.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle | 3 ++- .../tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle | 3 ++- .../wp_acsl/oracle_qualif/struct_use_case.0.res.oracle | 3 ++- .../wp_acsl/oracle_qualif/struct_use_case.1.res.oracle | 3 ++- src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle | 3 ++- .../tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle | 3 ++- .../wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle | 3 ++- .../wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle | 3 ++- .../wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle | 6 ++++-- .../wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle | 5 +++-- .../wp/tests/wp_bts/oracle_qualif/bts779.res.oracle | 5 +++-- .../wp/tests/wp_bts/oracle_qualif/bts788.res.oracle | 5 +++-- .../wp/tests/wp_bts/oracle_qualif/bts986.res.oracle | 5 +++-- .../wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle | 5 +++-- .../wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle | 5 +++-- .../wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle | 5 +++-- .../wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle | 5 +++-- .../tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle | 3 ++- .../wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle | 5 +++-- .../tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle | 3 ++- .../binary-multiplication-without-overflow.res.oracle | 6 ++++-- .../oracle_qualif/binary-multiplication.res.oracle | 6 ++++-- .../oracle_qualif/frama_c_exo1_solved.res.oracle | 6 ++++-- .../oracle_qualif/frama_c_exo2_solved.res.oracle | 6 ++++-- .../oracle_qualif/frama_c_exo3_solved.old.res.oracle | 6 ++++-- .../oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle | 6 ++++-- .../frama_c_exo3_solved.simplified.res.oracle | 6 ++++-- .../oracle_qualif/frama_c_hashtbl_solved.res.oracle | 6 ++++-- .../wp_gallery/oracle_qualif/loop-statement.res.oracle | 3 ++- .../wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle | 3 ++- .../wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle | 3 ++- .../tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle | 3 ++- .../wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle | 3 ++- .../wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle | 3 ++- .../wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle | 3 ++- .../wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle | 3 ++- .../wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle | 3 ++- .../wp_hoare/oracle_qualif/logicref_simple.res.oracle | 3 ++- .../wp/tests/wp_hoare/oracle_qualif/reference.res.oracle | 3 ++- .../wp_hoare/oracle_qualif/reference_and_struct.res.oracle | 3 ++- .../wp_hoare/oracle_qualif/reference_array.res.oracle | 7 ++++--- .../oracle_qualif/reference_array_simple.res.oracle | 3 ++- .../wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle | 3 ++- .../wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle | 3 ++- .../wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/asm.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/bool.1.res.oracle | 5 +++-- .../wp/tests/wp_plugin/oracle_qualif/copy.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle | 3 ++- .../wp_plugin/oracle_qualif/float_format.0.res.oracle | 3 ++- .../wp_plugin/oracle_qualif/float_format.1.res.oracle | 3 ++- .../wp_plugin/oracle_qualif/float_format.2.res.oracle | 3 ++- .../tests/wp_plugin/oracle_qualif/float_real.0.res.oracle | 3 ++- .../tests/wp_plugin/oracle_qualif/float_real.1.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/frame.res.oracle | 3 ++- .../tests/wp_plugin/oracle_qualif/ground_real.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle | 3 ++- .../wp_plugin/oracle_qualif/init_const_guard.res.oracle | 3 ++- .../tests/wp_plugin/oracle_qualif/init_extern.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/loop.res.oracle | 3 ++- .../tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/mask.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/params.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/plet.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/rte.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/struct.res.oracle | 3 ++- .../tests/wp_plugin/oracle_qualif/struct_hack.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/subset.res.oracle | 5 +++-- .../tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle | 5 +++-- .../wp/tests/wp_plugin/oracle_qualif/trig.res.oracle | 3 ++- .../tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle | 3 ++- .../wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle | 3 ++- .../wp_plugin/oracle_qualif/unsupported_init.res.oracle | 3 ++- .../wp/tests/wp_store/oracle_qualif/array.res.oracle | 3 ++- .../wp/tests/wp_store/oracle_qualif/natural.res.oracle | 3 ++- .../tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle | 3 ++- .../tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle | 3 ++- .../wp/tests/wp_store/oracle_qualif/struct.res.oracle | 5 +++-- .../wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle | 3 ++- .../wp_typed/oracle_qualif/array_initialized.0.res.oracle | 5 +++-- .../wp_typed/oracle_qualif/array_initialized.1.res.oracle | 5 +++-- .../wp/tests/wp_typed/oracle_qualif/avar.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle | 3 ++- .../wp_typed/oracle_qualif/struct_array_type.res.oracle | 5 +++-- .../tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle | 3 ++- .../tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle | 3 ++- .../tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle | 7 ++++--- .../tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle | 5 +++-- .../wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle | 3 ++- .../tests/wp_typed/oracle_qualif/unit_local.0.res.oracle | 5 +++-- .../tests/wp_typed/oracle_qualif/unit_local.1.res.oracle | 7 ++++--- .../wp_typed/oracle_qualif/unit_loopscope.0.res.oracle | 3 ++- .../wp_typed/oracle_qualif/unit_loopscope.1.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle | 3 ++- .../tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle | 3 ++- .../tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle | 3 ++- .../tests/wp_typed/oracle_qualif/user_collect.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/user_init.res.oracle | 3 ++- .../wp_typed/oracle_qualif/user_injector.0.res.oracle | 3 ++- .../wp_typed/oracle_qualif/user_injector.1.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/user_string.res.oracle | 5 +++-- .../wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle | 3 ++- .../wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle | 3 ++- .../wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle | 3 ++- .../tests/wp_usage/oracle_qualif/caveat_range.res.oracle | 3 ++- .../wp_usage/oracle_qualif/issue-189-bis.0.res.oracle | 3 ++- .../wp_usage/oracle_qualif/issue-189-bis.1.res.oracle | 3 ++- 214 files changed, 476 insertions(+), 253 deletions(-) diff --git a/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle index 981c1640a08..44d2cc9df1b 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle @@ -8,7 +8,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp/sharing.c.0.report.json' +[wp] Report in: 'tests/wp/oracle_qualif/sharing.0.report.json' +[wp] Report out: 'tests/wp/result_qualif/sharing.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - 1 (48..60) 1 100% diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle index d3b2208c9f1..0c1f65eaa9e 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle @@ -40,7 +40,8 @@ [wp] Proved goals: 19 / 27 Qed: 18 Alt-Ergo: 1 (unsuccess: 8) -[wp] Report 'tests/wp/stmtcompiler_test.i.0.report.json' +[wp] Report in: 'tests/wp/oracle_qualif/stmtcompiler_test.0.report.json' +[wp] Report out: 'tests/wp/result_qualif/stmtcompiler_test.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success empty 1 - 1 100% diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle index 78a9e8c0f3f..157a14e1b00 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle @@ -55,12 +55,13 @@ [wp] Proved goals: 32 / 38 Qed: 30 Alt-Ergo: 2 (unsuccess: 6) -[wp] Report 'tests/wp/wp_behav.c.0.report.json' +[wp] Report in: 'tests/wp/oracle_qualif/wp_behav.0.report.json' +[wp] Report out: 'tests/wp/result_qualif/wp_behav.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 5 - 5 100% min 4 - 4 100% -bhv 2 1 (8..20) 3 100% +bhv 2 1 (4..16) 3 100% stmt_contract 3 - 3 100% stmt_contract_label 2 - 2 100% stmt_contract_assigns 5 - 5 100% diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle index bc1f4d8ead0..cd60d0cd973 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle @@ -18,7 +18,8 @@ [wp] [Alt-Ergo] Goal typed_stmt_contract_assigns_ko_ensures_qed_ko : Unsuccess [wp] Proved goals: 0 / 8 Alt-Ergo: 0 (unsuccess: 8) -[wp] Report 'tests/wp/wp_behav.c.1.report.json' +[wp] Report in: 'tests/wp/oracle_qualif/wp_behav.1.report.json' +[wp] Report out: 'tests/wp/result_qualif/wp_behav.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - - 3 0.0% diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle index a61b5e65e10..fee194ce70a 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle @@ -21,7 +21,8 @@ [wp] Proved goals: 10 / 10 Qed: 9 Alt-Ergo: 1 -[wp] Report 'tests/wp/wp_call_pre.c.0.report.json' +[wp] Report in: 'tests/wp/oracle_qualif/wp_call_pre.0.report.json' +[wp] Report out: 'tests/wp/result_qualif/wp_call_pre.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success double_call 1 1 (4..16) 2 100% diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle index e838815abc1..7854eff46a0 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle @@ -8,8 +8,9 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp/wp_eqb.i.0.report.json' +[wp] Report in: 'tests/wp/oracle_qualif/wp_eqb.0.report.json' +[wp] Report out: 'tests/wp/result_qualif/wp_eqb.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -f - 1 (32..44) 1 100% +f - 1 (36..48) 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle index 71f60a87453..84aee82ec3f 100644 --- a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle +++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle @@ -39,7 +39,8 @@ [wp] Proved goals: 17 / 25 Qed: 17 Alt-Ergo: 0 (unsuccess: 8) -[wp] Report 'tests/wp/wp_strategy.c.0.report.json' +[wp] Report in: 'tests/wp/oracle_qualif/wp_strategy.0.report.json' +[wp] Report out: 'tests/wp/result_qualif/wp_strategy.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success bts0513 - - 2 0.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle index e9dcd2c5a7a..a3a8108a43b 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle @@ -31,7 +31,8 @@ [wp] Proved goals: 24 / 24 Qed: 21 Alt-Ergo: 3 -[wp] Report 'tests/wp_acsl/arith.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/arith.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/arith.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma 20 1 (1..8) 21 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle index 67dde50a424..799cfbbb52f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle @@ -7,7 +7,8 @@ [wp] [Alt-Ergo] Goal typed_cast_sgn_usgn_ensures_qed_ko_KO : Unsuccess [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_acsl/arith.i.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/arith.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/arith.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success cast_sgn_usgn - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle index cb994356b5b..77221b177c2 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle @@ -10,7 +10,8 @@ [wp] [Qed] Goal typed_jobG_assigns_normal : Valid [wp] Proved goals: 4 / 4 Qed: 4 -[wp] Report 'tests/wp_acsl/assign_array.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/assign_array.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/assign_array.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success jobA 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle index 898e9cdc2f9..41dc0500286 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle @@ -16,7 +16,8 @@ [wp] Proved goals: 9 / 9 Qed: 6 Alt-Ergo: 3 -[wp] Report 'tests/wp_acsl/assigns_path.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/assigns_path.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/assigns_path.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job 6 3 (20..32) 9 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle index c2e202de26b..9c8b4033d74 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle @@ -24,7 +24,8 @@ [wp] Proved goals: 17 / 17 Qed: 12 Alt-Ergo: 5 -[wp] Report 'tests/wp_acsl/assigns_range.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/assigns_range.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/assigns_range.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success call_assigns_all 12 2 (8..20) 14 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle index 62dbc55d245..82f100d322f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle @@ -12,7 +12,8 @@ [wp] [Alt-Ergo] Goal typed_call_assigns_t4_assigns_normal : Unsuccess [wp] Proved goals: 0 / 6 Alt-Ergo: 0 (unsuccess: 6) -[wp] Report 'tests/wp_acsl/assigns_range.i.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/assigns_range.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/assigns_range.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success call_assigns_t1 - - 2 0.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle index 1af8a459bfd..2b8385a1071 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle @@ -17,7 +17,8 @@ [wp] Proved goals: 8 / 10 Qed: 3 Alt-Ergo: 5 (unsuccess: 2) -[wp] Report 'tests/wp_acsl/axioms.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/axioms.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/axioms.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 3 5 (104..128) 10 80.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle index 4db477821a2..b27b33bf634 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 3 / 3 Qed: 2 Alt-Ergo: 1 -[wp] Report 'tests/wp_acsl/base_offset.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/base_offset.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/base_offset.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 2 1 (8..20) 3 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle index 74ff28899fe..8cc292011a2 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle @@ -36,7 +36,8 @@ [wp] Proved goals: 26 / 29 Qed: 25 Alt-Ergo: 1 (unsuccess: 3) -[wp] Report 'tests/wp_acsl/bitwise.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/bitwise.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/bitwise.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success band 8 - 8 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle index 9a78b68f273..f7415f64fd8 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle @@ -11,7 +11,8 @@ [wp] [Qed] Goal typed_job4_ensures : Valid [wp] Proved goals: 5 / 5 Qed: 5 -[wp] Report 'tests/wp_acsl/bitwise2.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/bitwise2.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/bitwise2.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job1 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle index 6033f7105e7..390d53bf041 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle @@ -16,7 +16,8 @@ [wp] [Qed] Goal typed_f_ensures_Pts1 : Valid [wp] Proved goals: 10 / 10 Qed: 10 -[wp] Report 'tests/wp_acsl/block_length.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/block_length.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/block_length.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 10 - 10 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle index 354a7ea0d71..18381fdbb21 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle @@ -9,8 +9,9 @@ [wp] Proved goals: 3 / 3 Qed: 0 Alt-Ergo: 3 -[wp] Report 'tests/wp_acsl/classify_float.c.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/classify_float.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/classify_float.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success -Lemma - 3 (1..12) 3 100% +Lemma - 3 (4..16) 3 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle index 611902c7719..7c556d41418 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle @@ -9,7 +9,8 @@ [wp] Proved goals: 3 / 3 Qed: 0 alt-ergo: 3 -[wp] Report 'tests/wp_acsl/classify_float.c.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/classify_float.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/classify_float.1.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma - - 3 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle index 9c3208e5ffa..8b1d5a84d04 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.2.res.oracle @@ -12,7 +12,8 @@ [wp] Proved goals: 3 / 3 Qed: 0 Coq: 3 -[wp] Report 'tests/wp_acsl/classify_float.c.2.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/classify_float.2.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/classify_float.2.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma - - 3 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle index bc588e84733..7f42f9cb837 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/cnf.res.oracle @@ -303,7 +303,8 @@ [wp] Proved goals: 43 / 43 Qed: 11 Alt-Ergo: 32 -[wp] Report 'tests/wp_acsl/cnf.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/cnf.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/cnf.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 11 32 (336..384) 43 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle index deffb65d657..23662c229a1 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.res.oracle @@ -7,7 +7,8 @@ [wp] [Qed] Goal typed_lemma_diff : Valid [wp] Proved goals: 2 / 2 Qed: 2 -[wp] Report 'tests/wp_acsl/ctor.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/ctor.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/ctor.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic Event 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle index 1e773b52273..700bf043119 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.0.res.oracle @@ -29,7 +29,8 @@ [wp] Proved goals: 22 / 22 Qed: 0 Alt-Ergo: 22 -[wp] Report 'tests/wp_acsl/div_mod.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/div_mod.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/div_mod.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - 22 (8..20) 22 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle index 6e34345f147..282eb4ee097 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.1.res.oracle @@ -29,7 +29,8 @@ [wp] Proved goals: 22 / 22 Qed: 0 alt-ergo: 22 -[wp] Report 'tests/wp_acsl/div_mod.i.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/div_mod.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/div_mod.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - - 22 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle index 3d3ad3145f0..0a7e3253df5 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/div_mod.2.res.oracle @@ -8,7 +8,8 @@ [wp] [Alt-Ergo] Goal typed_f_ensures_m7_mod_0_x_ko : Unsuccess [wp] Proved goals: 0 / 2 Alt-Ergo: 0 (unsuccess: 2) -[wp] Report 'tests/wp_acsl/div_mod.i.2.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/div_mod.2.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/div_mod.2.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - - 2 0.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle index e7b1cca13f1..5f939cfa006 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle @@ -50,7 +50,8 @@ [wp] Proved goals: 119 / 119 Qed: 8 Alt-Ergo: 111 -[wp] Report 'tests/wp_acsl/e_imply.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/e_imply.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/e_imply.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma - 77 (8..20) 77 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle index 445532eb63d..365e6a88d35 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.res.oracle @@ -13,13 +13,14 @@ [wp] Proved goals: 6 / 6 Qed: 1 Alt-Ergo: 5 -[wp] Report 'tests/wp_acsl/equal.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/equal.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/equal.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success simple_struct 1 - 1 100% simple_array - 1 (12..24) 1 100% with_array_struct - 1 (12..24) 1 100% -with_ptr_struct - 1 (8..20) 1 100% +with_ptr_struct - 1 (4..16) 1 100% with_ptr_array - 1 (12..24) 1 100% -with_ptr_and_array_struct - 1 (24..36) 1 100% +with_ptr_and_array_struct - 1 (28..40) 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle index 828ad921cb7..d0b001c2edc 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 4 / 4 Qed: 0 Alt-Ergo: 4 -[wp] Report 'tests/wp_acsl/float_compare.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/float_compare.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/float_compare.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma - 4 (28..40) 4 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle index 4710a979b9f..8a073f77487 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/funvar_inv.res.oracle @@ -9,7 +9,8 @@ [wp] [Qed] Goal typed_ref_g_loop_assigns : Valid [wp] Proved goals: 3 / 3 Qed: 3 -[wp] Report 'tests/wp_acsl/funvar_inv.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/funvar_inv.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/funvar_inv.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle index 33a7efd8bc0..122f044fbd9 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.res.oracle @@ -15,7 +15,8 @@ [wp] [Qed] Goal typed_bar_assigns_normal_part5 : Valid [wp] Proved goals: 9 / 9 Qed: 9 -[wp] Report 'tests/wp_acsl/implicit_enum_cast.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/implicit_enum_cast.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/implicit_enum_cast.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success bar 9 - 9 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle index b4b67bf6b9f..acfc1883f38 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle @@ -13,7 +13,8 @@ [wp] Proved goals: 3 / 4 Qed: 2 Alt-Ergo: 1 (unsuccess: 1) -[wp] Report 'tests/wp_acsl/init_label.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/init_label.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/init_label.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success main 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle index 0619f73d418..696cfec4377 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.0.res.oracle @@ -31,7 +31,8 @@ [wp] Proved goals: 24 / 24 Qed: 17 Alt-Ergo: 7 -[wp] Report 'tests/wp_acsl/init_value.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/init_value.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/init_value.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success main 14 6 (28..40) 20 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle index ab90d518152..1a296d83d67 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value.1.res.oracle @@ -24,7 +24,8 @@ [wp] [Alt-Ergo] Goal typed_main_ko_requires_qed_ko_indirect_init_union_t : Unsuccess [wp] Proved goals: 0 / 18 Alt-Ergo: 0 (unsuccess: 18) -[wp] Report 'tests/wp_acsl/init_value.i.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/init_value.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/init_value.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success main_ko - - 9 0.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle index aeadf11adb3..5a8aa566288 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_value_mem.res.oracle @@ -9,7 +9,8 @@ [wp] Proved goals: 2 / 2 Qed: 0 Alt-Ergo: 2 -[wp] Report 'tests/wp_acsl/init_value_mem.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/init_value_mem.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/init_value_mem.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success main - 2 (36..48) 2 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle index aa952f48265..296bd09f245 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.res.oracle @@ -7,7 +7,8 @@ [wp] [Qed] Goal typed_bug_ensures : Valid [wp] Proved goals: 1 / 1 Qed: 1 -[wp] Report 'tests/wp_acsl/intbool.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/intbool.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/intbool.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success bug 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle index 8d0656392ab..e067872acde 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.0.res.oracle @@ -7,7 +7,8 @@ [wp] [Qed] Goal typed_g_assert_qed_ok_ok : Valid [wp] Proved goals: 1 / 1 Qed: 1 -[wp] Report 'tests/wp_acsl/label_escape.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/label_escape.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/label_escape.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success g 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle index 32bbae5f36c..d304a79b974 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/label_escape.1.res.oracle @@ -7,7 +7,8 @@ [wp] [Alt-Ergo] Goal typed_f_assert_qed_ko_oracle_ko : Unsuccess [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_acsl/label_escape.i.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/label_escape.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/label_escape.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle index 26b176ac8f2..a5be47ac219 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.res.oracle @@ -65,7 +65,8 @@ [wp] Proved goals: 5 / 21 Qed: 3 Alt-Ergo: 2 (unsuccess: 16) -[wp] Report 'tests/wp_acsl/logic.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/logic.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/logic.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success h 2 - 3 66.7% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle index 26c8030d9da..7ce65969029 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/looplabels.res.oracle @@ -15,7 +15,8 @@ [wp] Proved goals: 8 / 8 Qed: 3 Alt-Ergo: 5 -[wp] Report 'tests/wp_acsl/looplabels.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/looplabels.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/looplabels.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success copy 3 5 (256..304) 8 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle index 1d6e4b7c5b2..8ff84050d33 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 3 / 3 Qed: 1 Alt-Ergo: 2 -[wp] Report 'tests/wp_acsl/null.c.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/null.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/null.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma - 2 (1..12) 2 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle index b319d2b2537..4476b69cd15 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.0.res.oracle @@ -18,7 +18,8 @@ [wp] Proved goals: 3 / 9 Qed: 3 Alt-Ergo: 0 (unsuccess: 6) -[wp] Report 'tests/wp_acsl/pointer.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/pointer.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/pointer.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success array 3 - 3 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle index 77732b04cfe..116c8aee7c9 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/pointer.1.res.oracle @@ -18,7 +18,8 @@ [wp] Proved goals: 3 / 9 Qed: 3 Alt-Ergo: 0 (unsuccess: 6) -[wp] Report 'tests/wp_acsl/pointer.i.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/pointer.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/pointer.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success array 3 - 3 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle index 4df28dabcef..6ab33eacbf5 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/post_result.res.oracle @@ -9,7 +9,8 @@ [wp] Proved goals: 1 / 2 Qed: 1 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_acsl/post_result.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/post_result.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/post_result.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success correct 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle index 6326d96688a..8e7baea94bb 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.0.res.oracle @@ -95,7 +95,8 @@ [wp] Proved goals: 52 / 52 Qed: 51 Alt-Ergo: 1 -[wp] Report 'tests/wp_acsl/precedence.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/precedence.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/precedence.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success predicate 29 1 (4..16) 30 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle index d8de2ea9bac..364ef5d90af 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/precedence.1.res.oracle @@ -79,7 +79,8 @@ [wp] [Alt-Ergo] Goal typed_predicate_ensures_ko_l_assoc_naming : Unsuccess [wp] Proved goals: 0 / 37 Alt-Ergo: 0 (unsuccess: 37) -[wp] Report 'tests/wp_acsl/precedence.i.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/precedence.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/precedence.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success predicate - - 23 0.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle index cf9b98a9f72..9b09be20007 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/range.res.oracle @@ -10,7 +10,8 @@ [wp] [Qed] Goal typed_test_call_val_assigns_q_requires_HQ_ok : Valid [wp] Proved goals: 4 / 4 Qed: 4 -[wp] Report 'tests/wp_acsl/range.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/range.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/range.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success test 4 - 4 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle index f5b9a542056..5c3ff3a3d69 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.0.res.oracle @@ -14,7 +14,8 @@ [wp] Proved goals: 5 / 7 Qed: 3 Alt-Ergo: 2 (unsuccess: 2) -[wp] Report 'tests/wp_acsl/reads.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/reads.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/reads.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - 1 (12..24) 1 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle index ccb9ad6d07a..bd1c8449cde 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/reads.1.res.oracle @@ -9,7 +9,8 @@ [wp] [Alt-Ergo] Goal typed_modifies_y_ensures_qed_ko_H_KO : Unsuccess [wp] Proved goals: 0 / 3 Alt-Ergo: 0 (unsuccess: 3) -[wp] Report 'tests/wp_acsl/reads.i.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/reads.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/reads.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success modifies_y - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle index a2ea10ac9b8..e62b365166b 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.0.res.oracle @@ -18,7 +18,8 @@ [wp] Proved goals: 11 / 11 Qed: 9 Alt-Ergo: 2 -[wp] Report 'tests/wp_acsl/record.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/record.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/record.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 9 2 (12..24) 11 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle index b5fa183f53f..a798b27a5de 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/record.1.res.oracle @@ -7,7 +7,8 @@ [wp] [Alt-Ergo] Goal typed_f_ensures_KP5_qed_ko : Unsuccess [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_acsl/record.i.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/record.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/record.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle index 715daac305c..815120bdc30 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/simpl_is_type.res.oracle @@ -22,7 +22,8 @@ [wp] Proved goals: 15 / 15 Qed: 6 Alt-Ergo: 9 -[wp] Report 'tests/wp_acsl/simpl_is_type.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/simpl_is_type.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/simpl_is_type.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 3 6 (88..112) 9 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle index f8ee684c72d..f907ba3b6ba 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.res.oracle @@ -9,7 +9,8 @@ [wp] Proved goals: 2 / 2 Qed: 0 Alt-Ergo: 2 -[wp] Report 'tests/wp_acsl/sizeof.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/sizeof.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/sizeof.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success foo - 2 (1..12) 2 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle index ef676363288..68251eed9cb 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.0.res.oracle @@ -9,7 +9,8 @@ [wp] Proved goals: 2 / 2 Qed: 1 Alt-Ergo: 1 -[wp] Report 'tests/wp_acsl/struct_use_case.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/struct_use_case.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/struct_use_case.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - 1 (16..28) 1 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle index dce325df60f..9951d3d26eb 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/struct_use_case.1.res.oracle @@ -8,7 +8,8 @@ [wp] [Alt-Ergo] Goal typed_caveat_g_ensures_ko : Unsuccess [wp] Proved goals: 0 / 2 Alt-Ergo: 0 (unsuccess: 2) -[wp] Report 'tests/wp_acsl/struct_use_case.i.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/struct_use_case.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/struct_use_case.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle index 9c5c4e8af59..d85af980df8 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/tset.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 4 / 4 Qed: 2 Alt-Ergo: 2 -[wp] Report 'tests/wp_acsl/tset.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/tset.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/tset.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma 2 2 (4..16) 4 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle index 3ba6b703c8f..a63cc1b831a 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.0.res.oracle @@ -8,7 +8,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_acsl/type_guard.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/type_guard.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/type_guard.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - 1 (12..24) 1 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle index 25cc92fe77c..93bcefeddd9 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/type_guard.1.res.oracle @@ -7,7 +7,8 @@ [wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_acsl/type_guard.i.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/type_guard.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/type_guard.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle index d5c9648c9d9..284ab16fc04 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.res.oracle @@ -11,7 +11,8 @@ [wp] Proved goals: 3 / 4 Qed: 2 Alt-Ergo: 1 (unsuccess: 1) -[wp] Report 'tests/wp_acsl/unit_bit_test.c.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/unit_bit_test.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/unit_bit_test.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success sum 1 - 2 50.0% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle index 285de12567f..6822d60dd5b 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.res.oracle @@ -7,7 +7,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_acsl/unit_bool.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/unit_bool.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/unit_bool.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic Foo - 1 (1..12) 1 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle index e3c4552cbe9..d6277a5e6bf 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.0.res.oracle @@ -8,7 +8,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_acsl/user_def_type_guard.i.0.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/user_def_type_guard.0.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/user_def_type_guard.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - 1 (12..24) 1 100% diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle index e25eb05dbab..105df712f0f 100644 --- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle +++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/user_def_type_guard.1.res.oracle @@ -7,7 +7,8 @@ [wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko : Unsuccess [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_acsl/user_def_type_guard.i.1.report.json' +[wp] Report in: 'tests/wp_acsl/oracle_qualif/user_def_type_guard.1.report.json' +[wp] Report out: 'tests/wp_acsl/result_qualif/user_def_type_guard.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle index 7c13800bcbd..cb7876bede3 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0708.res.oracle @@ -8,7 +8,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_bts/bts0708.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts0708.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts0708.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - 1 (4..16) 1 100% @@ -20,7 +21,8 @@ f - 1 (4..16) 1 100% [wp] Proved goals: 2 / 2 Qed: 0 Alt-Ergo: 2 -[wp] Report 'tests/wp_bts/bts0708.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts0708.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts0708.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - 2 (4..16) 2 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle index a0f8a4094b8..c121fa495ee 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle @@ -11,9 +11,10 @@ [wp] Proved goals: 4 / 4 Qed: 2 Alt-Ergo: 2 -[wp] Report 'tests/wp_bts/bts0843.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts0843.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts0843.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f3 1 - 1 100% -g3 1 2 (8..20) 3 100% +g3 1 2 (12..24) 3 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle index 57d0e72ba57..07a66659080 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle @@ -9,8 +9,9 @@ [wp] Proved goals: 1 / 2 Qed: 0 Alt-Ergo: 1 (unsuccess: 1) -[wp] Report 'tests/wp_bts/bts779.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts779.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts779.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -f - 1 (12..24) 2 50.0% +f - 1 (16..28) 2 50.0% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle index a85d715c3e1..45805894c54 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts788.res.oracle @@ -10,8 +10,9 @@ [wp] Proved goals: 3 / 3 Qed: 1 Alt-Ergo: 2 -[wp] Report 'tests/wp_bts/bts788.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts788.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts788.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -main 1 2 (8..20) 3 100% +main 1 2 (12..24) 3 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle index d1038d209ce..e7516bcc0d4 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts986.res.oracle @@ -8,8 +8,9 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_bts/bts986.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts986.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts986.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -f - 1 (8..20) 1 100% +f - 1 (12..24) 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle index cb41d88104f..d6e73f126e8 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1174.res.oracle @@ -9,7 +9,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Coq: 1 -[wp] Report 'tests/wp_bts/bts_1174.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_1174.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts_1174.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job - - 1 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle index fb5eda64c69..3b2380fd578 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1176.res.oracle @@ -7,7 +7,8 @@ [wp] [Qed] Goal typed_f_assert_qed_ok : Valid [wp] Proved goals: 1 / 1 Qed: 1 -[wp] Report 'tests/wp_bts/bts_1176.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_1176.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts_1176.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle index 1c324eef37b..294ec76d1a5 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle @@ -18,9 +18,10 @@ [wp] Proved goals: 9 / 10 Qed: 8 Alt-Ergo: 1 (unsuccess: 1) -[wp] Report 'tests/wp_bts/bts_1360.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_1360.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts_1360.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success foo_wrong 4 - 5 80.0% -foo_correct 4 1 (12..24) 5 100% +foo_correct 4 1 (16..28) 5 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle index d5c0104b187..d02f6600d10 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.res.oracle @@ -20,7 +20,8 @@ [wp] Proved goals: 12 / 13 Qed: 10 Alt-Ergo: 2 (unsuccess: 1) -[wp] Report 'tests/wp_bts/bts_1462.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_1462.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts_1462.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success wrong 6 2 (4..16) 9 88.9% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle index 300282b34a9..943498ad33b 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.res.oracle @@ -11,7 +11,8 @@ [wp] Proved goals: 2 / 4 Qed: 2 Alt-Ergo: 0 (unsuccess: 2) -[wp] Report 'tests/wp_bts/bts_1586.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_1586.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts_1586.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success compute_bizarre 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle index 6a9e1f868ab..38088c7cf01 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.res.oracle @@ -13,7 +13,8 @@ [wp] [Qed] Goal typed_f_assert_a1 : Valid [wp] Proved goals: 3 / 3 Qed: 3 -[wp] Report 'tests/wp_bts/bts_1588.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_1588.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts_1588.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 3 - 3 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle index 8ab82c08dc1..5cb16f6a76e 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.res.oracle @@ -15,7 +15,8 @@ [wp] Proved goals: 8 / 8 Qed: 7 Alt-Ergo: 1 -[wp] Report 'tests/wp_bts/bts_1601.c.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_1601.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts_1601.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success foo 7 1 (16..28) 8 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle index c1f6dc0e2ae..16f842993b4 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.0.res.oracle @@ -13,10 +13,11 @@ [wp] Proved goals: 4 / 6 Qed: 3 Alt-Ergo: 1 (unsuccess: 2) -[wp] Report 'tests/wp_bts/bts_1828.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_1828.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts_1828.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -local_frame - 1 (8..20) 1 100% +local_frame - 1 (4..16) 1 100% global_frame 3 - 5 60.0% ------------------------------------------------------------- [wp] Warning: Memory model hypotheses for function 'global_frame': diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle index c751f5eeda1..53e9e1ea9f7 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1828.1.res.oracle @@ -13,10 +13,11 @@ [wp] Proved goals: 6 / 6 Qed: 5 Alt-Ergo: 1 -[wp] Report 'tests/wp_bts/bts_1828.i.1.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_1828.1.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts_1828.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -local_frame - 1 (8..20) 1 100% +local_frame - 1 (4..16) 1 100% global_frame 5 - 5 100% ------------------------------------------------------------- [wp] Warning: Memory model hypotheses for function 'global_frame': diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle index 2eba18f8727..f9e05af007b 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.res.oracle @@ -7,7 +7,8 @@ [wp] [Qed] Goal typed_call_assert : Valid [wp] Proved goals: 1 / 1 Qed: 1 -[wp] Report 'tests/wp_bts/bts_2040.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_2040.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts_2040.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success call 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle index 1677f2005a8..8cfc20cb4a0 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2079.res.oracle @@ -8,7 +8,8 @@ [wp] [Qed] Goal typed_main_ensures_Eval_Q : Valid [wp] Proved goals: 2 / 2 Qed: 2 -[wp] Report 'tests/wp_bts/bts_2079.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_2079.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts_2079.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success main 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle index 5957c25a991..50ac59f33c4 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.res.oracle @@ -8,8 +8,9 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_bts/bts_2159.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/bts_2159.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/bts_2159.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -job - 1 (56..68) 1 100% +job - 1 (56..80) 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle index adbf79dec6e..16dfd1723cf 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.res.oracle @@ -14,7 +14,8 @@ [wp] [Qed] Goal typed_f_assigns : Valid [wp] Proved goals: 8 / 8 Qed: 8 -[wp] Report 'tests/wp_bts/ergo_typecheck.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/ergo_typecheck.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/ergo_typecheck.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 8 - 8 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle index 9dadbafaa24..2257d0da19c 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.res.oracle @@ -9,7 +9,8 @@ [wp] Proved goals: 2 / 2 Qed: 0 Alt-Ergo: 2 -[wp] Report 'tests/wp_bts/issue-364.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/issue-364.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/issue-364.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success main - 2 (28..40) 2 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle index 57e70441a4b..cf47b28f62f 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle @@ -8,7 +8,8 @@ [wp] Proved goals: 2 / 2 Qed: 0 Alt-Ergo: 2 -[wp] Report 'tests/wp_bts/issue_143.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_143.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/issue_143.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic A - 1 (1..12) 1 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle index 573e4b2c89b..2da222911d1 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle @@ -16,7 +16,8 @@ Alt-Ergo: 0 (failed: 2) Coq: 0 (failed: 2) alt-ergo: 0 (failed: 2) -[wp] Report 'tests/wp_bts/issue_143.i.1.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_143.1.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/issue_143.1.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic A - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle index 2ebb69cf3ce..a8efd0f899e 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle @@ -9,7 +9,8 @@ Command './tests/inexistant-prover' not found [wp] Proved goals: 0 / 2 Alt-Ergo: 0 (failed: 2) -[wp] Report 'tests/wp_bts/issue_143.i.2.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_143.2.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/issue_143.2.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic A - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle index 5ea347ae63a..87bd09a92c1 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle @@ -10,7 +10,8 @@ Command './tests/inexistant-prover' not found [wp] Proved goals: 0 / 2 Coq: 0 (failed: 2) -[wp] Report 'tests/wp_bts/issue_143.i.3.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_143.3.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/issue_143.3.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic A - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle index e99621a4bbb..41fbe2f345b 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.res.oracle @@ -7,7 +7,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_bts/issue_198.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_198.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/issue_198.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma - 1 (4..16) 1 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle index 51a96c4ae5d..7ed8bcd4eff 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle @@ -7,7 +7,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_bts/issue_447.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_447.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/issue_447.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma - 1 (1..12) 1 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle index ac1e7341c07..95860c42514 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.res.oracle @@ -12,7 +12,8 @@ [wp] [Qed] Goal typed_f2_assigns : Valid [wp] Proved goals: 6 / 6 Qed: 6 -[wp] Report 'tests/wp_bts/issue_453.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_453.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/issue_453.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f1 3 - 3 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle index 0bdfc3c7769..ca1ca40b8f9 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 1 / 3 Qed: 0 Alt-Ergo: 1 (unsuccess: 2) -[wp] Report 'tests/wp_bts/issue_494.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_494.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/issue_494.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - 1 (8..20) 1 100% diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle index e91fa5af173..12cb9521f41 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.res.oracle @@ -10,8 +10,9 @@ [wp] Proved goals: 3 / 3 Qed: 2 Alt-Ergo: 1 -[wp] Report 'tests/wp_bts/issue_508.c.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_508.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/issue_508.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -add 2 1 (52..64) 3 100% +add 2 1 (56..68) 3 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle index 1588ce4deb1..ac5a5264006 100644 --- a/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle +++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.res.oracle @@ -20,7 +20,8 @@ [wp] [Qed] Goal typed_unreachable_smt_with_contract_call_f_with_precond_requires_ok : Valid [wp] Proved goals: 8 / 8 Qed: 8 -[wp] Report 'tests/wp_bts/nupw-bcl-bts1120.i.0.report.json' +[wp] Report in: 'tests/wp_bts/oracle_qualif/nupw-bcl-bts1120.0.report.json' +[wp] Report out: 'tests/wp_bts/result_qualif/nupw-bcl-bts1120.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success g 6 - 6 100% diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle index 54c0e393099..396326b005b 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle @@ -17,7 +17,8 @@ [wp] Proved goals: 10 / 10 Qed: 3 alt-ergo: 7 -[wp] Report 'tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication-without-overflow.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic mult 1 - 1 100% @@ -45,7 +46,8 @@ BinaryMultiplication 2 - 9 100% [wp] Proved goals: 11 / 14 Qed: 0 alt-ergo: 11 -[wp] Report 'tests/wp_gallery/binary-multiplication-without-overflow.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication-without-overflow.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic mult 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle index dd5a5577e64..72aefff35c4 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle @@ -21,7 +21,8 @@ [wp] Proved goals: 14 / 14 Qed: 3 alt-ergo: 11 -[wp] Report 'tests/wp_gallery/binary-multiplication.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic mult 1 - 3 100% @@ -49,7 +50,8 @@ BinaryMultiplication 2 - 11 100% [wp] Proved goals: 11 / 14 Qed: 0 alt-ergo: 11 -[wp] Report 'tests/wp_gallery/binary-multiplication.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/binary-multiplication.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/binary-multiplication.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic mult 1 - 3 100% diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle index ce302571214..04777edf3a4 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle @@ -17,7 +17,8 @@ [wp] Proved goals: 10 / 10 Qed: 6 Alt-Ergo: 4 -[wp] Report 'tests/wp_gallery/frama_c_exo1_solved.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo1_solved.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success exo1 6 4 (176..224) 10 100% @@ -43,7 +44,8 @@ exo1 6 4 (176..224) 10 100% [wp] Proved goals: 9 / 15 Qed: 0 Alt-Ergo: 9 -[wp] Report 'tests/wp_gallery/frama_c_exo1_solved.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo1_solved.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success exo1 6 9 (176..224) 15 100% diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle index f2115310be1..6a66fec80b6 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle @@ -29,7 +29,8 @@ [wp] Proved goals: 22 / 22 Qed: 9 Alt-Ergo: 13 -[wp] Report 'tests/wp_gallery/frama_c_exo2_solved.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo2_solved.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success max_subarray 9 13 (272..320) 22 100% @@ -63,7 +64,8 @@ max_subarray 9 13 (272..320) 22 100% [wp] Proved goals: 14 / 23 Qed: 0 Alt-Ergo: 14 -[wp] Report 'tests/wp_gallery/frama_c_exo2_solved.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo2_solved.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success max_subarray 9 14 (272..320) 23 100% diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle index 1ff95155e5e..ec2a4c65cdc 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle @@ -41,7 +41,8 @@ [wp] Proved goals: 34 / 34 Qed: 18 Alt-Ergo: 16 -[wp] Report 'tests/wp_gallery/frama_c_exo3_solved.old.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo3_solved.old.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success equal_elements 18 16 (672..768) 34 100% @@ -110,7 +111,8 @@ equal_elements 18 16 (672..768) 34 100% [wp] Proved goals: 32 / 50 Qed: 11 Alt-Ergo: 21 -[wp] Report 'tests/wp_gallery/frama_c_exo3_solved.old.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo3_solved.old.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success equal_elements 29 21 (672..768) 50 100% diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle index 6de56a443e7..a89ecabb491 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle @@ -42,7 +42,8 @@ [wp] Proved goals: 35 / 35 Qed: 17 Alt-Ergo: 18 -[wp] Report 'tests/wp_gallery/frama_c_exo3_solved.old.v2.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo3_solved.old.v2.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success equal_elements 17 18 (288..336) 35 100% @@ -112,7 +113,8 @@ equal_elements 17 18 (288..336) 35 100% [wp] Proved goals: 34 / 51 Qed: 11 Alt-Ergo: 23 -[wp] Report 'tests/wp_gallery/frama_c_exo3_solved.old.v2.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo3_solved.old.v2.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success equal_elements 28 23 (288..336) 51 100% diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle index 8abf274c23d..bd1ae53be93 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle @@ -33,7 +33,8 @@ [wp] Proved goals: 26 / 26 Qed: 16 Alt-Ergo: 10 -[wp] Report 'tests/wp_gallery/frama_c_exo3_solved.simplified.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo3_solved.simplified.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success pair 16 10 (104..128) 26 100% @@ -79,7 +80,8 @@ pair 16 10 (104..128) 26 100% [wp] Proved goals: 19 / 35 Qed: 4 Alt-Ergo: 15 -[wp] Report 'tests/wp_gallery/frama_c_exo3_solved.simplified.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_exo3_solved.simplified.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success pair 20 15 (104..128) 35 100% diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle index 10e32d116c6..73e10138773 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.res.oracle @@ -110,7 +110,8 @@ [wp] Proved goals: 102 / 102 Qed: 69 Alt-Ergo: 33 -[wp] Report 'tests/wp_gallery/frama_c_hashtbl_solved.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_hashtbl_solved.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success eq_string 11 4 (48..60) 15 100% @@ -274,7 +275,8 @@ mem_binding 18 8 (192..240) 26 100% [wp] Proved goals: 74 / 143 Qed: 16 Alt-Ergo: 58 -[wp] Report 'tests/wp_gallery/frama_c_hashtbl_solved.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/frama_c_hashtbl_solved.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/frama_c_hashtbl_solved.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success eq_string 11 7 (112..136) 18 100% diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle index 26816b946bc..38e6e69735b 100644 --- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle +++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/loop-statement.res.oracle @@ -22,7 +22,8 @@ [wp] Proved goals: 15 / 15 Qed: 11 Alt-Ergo: 4 -[wp] Report 'tests/wp_gallery/loop-statement.c.0.report.json' +[wp] Report in: 'tests/wp_gallery/oracle_qualif/loop-statement.0.report.json' +[wp] Report out: 'tests/wp_gallery/result_qualif/loop-statement.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic Ploop - 1 (176..200) 1 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle index d0b99a55052..7f355b798b9 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.0.res.oracle @@ -19,7 +19,8 @@ [wp] Proved goals: 11 / 12 Qed: 11 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_hoare/byref.i.0.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/byref.0.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/byref.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle index f6c7d899a1f..023df532017 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/byref.1.res.oracle @@ -18,7 +18,8 @@ [wp] [Qed] Goal typed_ref_wrong_without_ref_call_f_requires : Valid [wp] Proved goals: 12 / 12 Qed: 12 -[wp] Report 'tests/wp_hoare/byref.i.1.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/byref.1.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/byref.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle index 9f3c90d052e..e18208021cc 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var.res.oracle @@ -84,7 +84,8 @@ [wp] [Qed] Goal typed_ref_ref_bd_assigns : Valid [wp] Proved goals: 78 / 78 Qed: 78 -[wp] Report 'tests/wp_hoare/dispatch_var.i.0.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/dispatch_var.0.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/dispatch_var.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success call_ref_ctr 4 - 4 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle index d0dfe75fac5..989780bb736 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.0.res.oracle @@ -40,7 +40,8 @@ [wp] [Qed] Goal typed_ref_reset_assigns : Valid [wp] Proved goals: 34 / 34 Qed: 34 -[wp] Report 'tests/wp_hoare/dispatch_var2.i.0.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/dispatch_var2.0.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/dispatch_var2.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success reset 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle index a161e9ffe1a..1f12910a8ff 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/dispatch_var2.1.res.oracle @@ -40,7 +40,8 @@ [wp] [Qed] Goal typed_ref_reset_assigns : Valid [wp] Proved goals: 34 / 34 Qed: 34 -[wp] Report 'tests/wp_hoare/dispatch_var2.i.1.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/dispatch_var2.1.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/dispatch_var2.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success reset 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle index 9a06ba323da..2c4e686d006 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/isHoare.res.oracle @@ -7,7 +7,8 @@ [wp] [Qed] Goal typed_ref_cmp_invalid_addr_as_int_ensures_ok : Valid [wp] Proved goals: 1 / 1 Qed: 1 -[wp] Report 'tests/wp_hoare/isHoare.i.0.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/isHoare.0.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/isHoare.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success cmp_invalid_addr_as_int 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle index 47e4dd7697a..48086704159 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicarr.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 3 / 3 Qed: 0 Alt-Ergo: 3 -[wp] Report 'tests/wp_hoare/logicarr.i.0.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/logicarr.0.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/logicarr.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job - 3 (64..88) 3 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle index f2a287c6cab..92d91196a20 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref.res.oracle @@ -12,7 +12,8 @@ [wp] Proved goals: 5 / 5 Qed: 4 Alt-Ergo: 1 -[wp] Report 'tests/wp_hoare/logicref.i.0.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/logicref.0.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/logicref.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success fvrange_n 2 1 (96..120) 3 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle index 8233499c143..c815416dfcb 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/logicref_simple.res.oracle @@ -16,7 +16,8 @@ [wp] Proved goals: 9 / 9 Qed: 5 Alt-Ergo: 4 -[wp] Report 'tests/wp_hoare/logicref_simple.i.0.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/logicref_simple.0.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/logicref_simple.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success fsimple 1 1 (8..20) 2 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle index 0dd9bdf4efe..4644bd595c5 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference.res.oracle @@ -30,7 +30,8 @@ [wp] Proved goals: 21 / 23 Qed: 21 Alt-Ergo: 0 (unsuccess: 2) -[wp] Report 'tests/wp_hoare/reference.i.0.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/reference.0.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/reference.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success g 7 - 7 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle index 67424143d7c..602cb3ba09c 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle @@ -39,7 +39,8 @@ [wp] Proved goals: 32 / 32 Qed: 27 Alt-Ergo: 5 -[wp] Report 'tests/wp_hoare/reference_and_struct.i.0.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/reference_and_struct.0.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/reference_and_struct.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success reset 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle index 9b452f762f8..048fdb55f65 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array.res.oracle @@ -43,12 +43,13 @@ [wp] Proved goals: 36 / 36 Qed: 24 Alt-Ergo: 12 -[wp] Report 'tests/wp_hoare/reference_array.i.0.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/reference_array.0.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/reference_array.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success reset_1_5 3 1 (16..28) 4 100% -load_1_5 3 1 (12..24) 4 100% -add_1_5 3 1 (12..24) 4 100% +load_1_5 3 1 (16..28) 4 100% +add_1_5 3 1 (16..28) 4 100% calls_on_array_dim_1 5 3 (8..20) 8 100% calls_on_array_dim_2_to_1 5 3 (8..20) 8 100% calls_on_array_dim_2 5 3 (4..16) 8 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle index bcc5f4a414b..4e5bda55247 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_array_simple.res.oracle @@ -9,7 +9,8 @@ [wp] [Qed] Goal typed_ref_call_f3_ensures : Valid [wp] Proved goals: 3 / 3 Qed: 3 -[wp] Report 'tests/wp_hoare/reference_array_simple.i.0.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/reference_array_simple.0.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/reference_array_simple.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success call_f1 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle index b183563a0de..dfe7c1cee8a 100644 --- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle +++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/refguards.res.oracle @@ -16,7 +16,8 @@ [wp] Proved goals: 8 / 9 Qed: 7 Alt-Ergo: 1 (unsuccess: 1) -[wp] Report 'tests/wp_hoare/refguards.i.0.report.json' +[wp] Report in: 'tests/wp_hoare/oracle_qualif/refguards.0.report.json' +[wp] Report out: 'tests/wp_hoare/result_qualif/refguards.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle index 86b06c6e37c..d8f446952e2 100644 --- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle +++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.0.res.oracle @@ -11,7 +11,8 @@ [wp] Proved goals: 2 / 2 Qed: 1 Alt-Ergo: 1 -[wp] Report 'tests/wp_manual/manual.i.0.report.json' +[wp] Report in: 'tests/wp_manual/oracle_qualif/manual.0.report.json' +[wp] Report out: 'tests/wp_manual/result_qualif/manual.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success swap 1 1 (12..24) 2 100% diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle index 7380ed072cd..1782d6f5cbd 100644 --- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle +++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle @@ -17,7 +17,8 @@ [wp] Proved goals: 8 / 8 Qed: 5 Alt-Ergo: 3 -[wp] Report 'tests/wp_manual/manual.i.1.report.json' +[wp] Report in: 'tests/wp_manual/oracle_qualif/manual.1.report.json' +[wp] Report out: 'tests/wp_manual/result_qualif/manual.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success swap 5 3 (16..28) 8 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle index 1e817d3077d..dad1045f7f1 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.0.res.oracle @@ -8,7 +8,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_plugin/abs.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/abs.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/abs.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success abs - 1 (4..16) 1 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle index da2e3b662c9..10af4e85904 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.1.res.oracle @@ -9,7 +9,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Coq: 1 -[wp] Report 'tests/wp_plugin/abs.i.1.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/abs.1.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/abs.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success abs - - 1 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle index 45650ee45ad..a1093f1b486 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/abs.2.res.oracle @@ -8,7 +8,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 alt-ergo: 1 -[wp] Report 'tests/wp_plugin/abs.i.2.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/abs.2.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/abs.2.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success abs - - 1 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle index 95ecc4413a6..4ea3ccfbe02 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 1 / 3 Qed: 1 Alt-Ergo: 0 (unsuccess: 2) -[wp] Report 'tests/wp_plugin/asm.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/asm.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/asm.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success main 1 - 3 33.3% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle index 9b576523536..8361dfbe06c 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.0.res.oracle @@ -14,7 +14,8 @@ [wp] Proved goals: 3 / 7 Qed: 2 Alt-Ergo: 1 (unsuccess: 4) -[wp] Report 'tests/wp_plugin/bool.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/bool.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/bool.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.1.res.oracle index 6bcbed6d8bc..04c1d1900f3 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bool.1.res.oracle @@ -14,11 +14,12 @@ [wp] Proved goals: 7 / 7 Qed: 2 Alt-Ergo: 5 -[wp] Report 'tests/wp_plugin/bool.i.1.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/bool.1.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/bool.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job - 1 (12..24) 1 100% -bor_bool - 2 (12..24) 2 100% +bor_bool - 2 (8..20) 2 100% band_bool 1 1 (20..32) 2 100% bxor_bool 1 1 (8..20) 2 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle index 7f5deafd0c1..257e195abe6 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.res.oracle @@ -17,7 +17,8 @@ [wp] Proved goals: 10 / 10 Qed: 4 Alt-Ergo: 6 -[wp] Report 'tests/wp_plugin/copy.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/copy.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/copy.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success copy 4 6 (288..336) 10 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle index 30dcd6fe79e..fd19084848e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/dynamic.res.oracle @@ -59,7 +59,8 @@ [wp] Proved goals: 50 / 51 Qed: 47 Alt-Ergo: 3 (unsuccess: 1) -[wp] Report 'tests/wp_plugin/dynamic.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/dynamic.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/dynamic.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success call 2 2 (56..80) 4 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle index 3b6766f3873..c940f2f2578 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.0.res.oracle @@ -13,7 +13,8 @@ [wp] Proved goals: 1 / 6 Qed: 1 Alt-Ergo: 0 (unsuccess: 5) -[wp] Report 'tests/wp_plugin/flash.c.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/flash.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/flash.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job 1 - 6 16.7% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle index 0526455b58b..76f1cf10976 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.1.res.oracle @@ -15,7 +15,8 @@ [wp] Proved goals: 6 / 6 Qed: 1 Alt-Ergo: 5 -[wp] Report 'tests/wp_plugin/flash.c.1.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/flash.1.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/flash.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job 1 5 (88..112) 6 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle index 93ab36295ed..43d789adfdc 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/flash.2.res.oracle @@ -12,7 +12,8 @@ [wp] [Qed] Goal typed_flash_job_ensures_WriteValues : Valid [wp] Proved goals: 6 / 6 Qed: 6 -[wp] Report 'tests/wp_plugin/flash.c.2.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/flash.2.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/flash.2.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job 6 - 6 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle index e99bbe52581..410aec2eb75 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.0.res.oracle @@ -11,7 +11,8 @@ [wp] [Coq] Goal typed_output_ensures_KO : Unsuccess [wp] Proved goals: 0 / 1 Coq: 0 (unsuccess: 1) -[wp] Report 'tests/wp_plugin/float_format.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/float_format.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/float_format.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success output - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle index 4abab0bd7af..a4124a02b3e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.1.res.oracle @@ -10,7 +10,8 @@ [wp] [Alt-Ergo] Goal typed_output_ensures_KO : Unsuccess [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_plugin/float_format.i.1.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/float_format.1.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/float_format.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success output - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle index 2559e2a4b9d..f2836be71fc 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_format.2.res.oracle @@ -10,7 +10,8 @@ [wp] [alt-ergo] Goal typed_output_ensures_KO : Unsuccess [wp] Proved goals: 0 / 1 alt-ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_plugin/float_format.i.2.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/float_format.2.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/float_format.2.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success output - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle index 37401296885..5200a07c448 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.0.res.oracle @@ -11,7 +11,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_plugin/float_real.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/float_real.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/float_real.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success dequal - 1 (12..24) 1 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle index 635a026579a..5ff495a8da3 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/float_real.1.res.oracle @@ -10,7 +10,8 @@ [wp] [Alt-Ergo] Goal typed_dequal_ensures : Unsuccess [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_plugin/float_real.i.1.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/float_real.1.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/float_real.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success dequal - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle index 1d743b2e6bb..09ce81e04f0 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.res.oracle @@ -13,7 +13,8 @@ [wp] Proved goals: 2 / 6 Qed: 2 Alt-Ergo: 0 (unsuccess: 4) -[wp] Report 'tests/wp_plugin/frame.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/frame.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/frame.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success local 1 - 2 50.0% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle index c34aa5aa74d..fddcff86c50 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.res.oracle @@ -7,7 +7,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_plugin/ground_real.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/ground_real.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/ground_real.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma - 1 (1..8) 1 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle index fdb495c5357..44b0803a513 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/inductive.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 2 / 2 Qed: 0 Coq: 2 -[wp] Report 'tests/wp_plugin/inductive.c.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/inductive.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/inductive.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma - - 2 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle index 483dc58e36e..b16a952d48e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const.res.oracle @@ -11,7 +11,8 @@ [wp] Proved goals: 2 / 4 Qed: 2 Alt-Ergo: 0 (unsuccess: 2) -[wp] Report 'tests/wp_plugin/init_const.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/init_const.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/init_const.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success fA - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle index 7fa9591a61b..2f6b498eb88 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_const_guard.res.oracle @@ -14,7 +14,8 @@ [wp] Proved goals: 6 / 7 Qed: 4 Alt-Ergo: 2 (unsuccess: 1) -[wp] Report 'tests/wp_plugin/init_const_guard.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/init_const_guard.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/init_const_guard.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 3 1 (16..28) 4 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle index ec5da8c77e1..66d00763f16 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_extern.res.oracle @@ -11,7 +11,8 @@ [wp] Proved goals: 1 / 3 Qed: 1 Alt-Ergo: 0 (unsuccess: 2) -[wp] Report 'tests/wp_plugin/init_extern.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/init_extern.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/init_extern.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 1 - 3 33.3% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle index 0eda5beada3..8ba6d1158dc 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.res.oracle @@ -11,7 +11,8 @@ [wp] Proved goals: 3 / 4 Qed: 3 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_plugin/init_valid.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/init_valid.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/init_valid.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success validA 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle index fdaf378128c..ca355f5d5cd 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/initarr.res.oracle @@ -9,7 +9,8 @@ [wp] Proved goals: 2 / 2 Qed: 0 Alt-Ergo: 2 -[wp] Report 'tests/wp_plugin/initarr.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/initarr.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/initarr.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job - 2 (40..52) 2 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle index 7cbec9994f8..5bfd4b969d1 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.0.res.oracle @@ -19,7 +19,8 @@ [wp] [Qed] Goal typed_f_SUCCESS_ensures_qed_ok_4 : Valid [wp] Proved goals: 13 / 13 Qed: 13 -[wp] Report 'tests/wp_plugin/injector.c.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/injector.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/injector.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 13 - 13 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle index 7bf755e5732..6ae999d7186 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/injector.1.res.oracle @@ -10,7 +10,8 @@ [wp] [Alt-Ergo] Goal typed_f_ko_1_ensures_qed_ko_3 : Unsuccess [wp] Proved goals: 0 / 4 Alt-Ergo: 0 (unsuccess: 4) -[wp] Report 'tests/wp_plugin/injector.c.1.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/injector.1.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/injector.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - - 4 0.0% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle index 66d473a27d5..74f07f5036c 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loop.res.oracle @@ -16,7 +16,8 @@ [wp] Proved goals: 8 / 9 Qed: 3 Alt-Ergo: 5 (unsuccess: 1) -[wp] Report 'tests/wp_plugin/loop.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/loop.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/loop.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success init 3 5 (104..128) 9 88.9% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle index 0eb100dcd2f..7de8fa06743 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.res.oracle @@ -12,7 +12,8 @@ [wp] [Qed] Goal typed_f_loop_invariant_2_established : Valid [wp] Proved goals: 4 / 4 Qed: 4 -[wp] Report 'tests/wp_plugin/loopcurrent.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/loopcurrent.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/loopcurrent.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 4 - 4 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle index 42b8084aefb..52c22ca6ebd 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.res.oracle @@ -12,7 +12,8 @@ [wp] [Qed] Goal typed_f_loop_invariant_2_established : Valid [wp] Proved goals: 4 / 4 Qed: 4 -[wp] Report 'tests/wp_plugin/loopentry.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/loopentry.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/loopentry.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 4 - 4 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle index 3ff1c5aa732..bdc927c48c2 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.res.oracle @@ -13,7 +13,8 @@ [wp] [Qed] Goal typed_f_assert_3 : Valid [wp] Proved goals: 3 / 3 Qed: 3 -[wp] Report 'tests/wp_plugin/loopextra.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/loopextra.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/loopextra.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 3 - 3 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle index e0af8eb5379..646eb1516ce 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.res.oracle @@ -8,7 +8,8 @@ [wp] [Qed] Goal typed_compute_ensures_B : Valid [wp] Proved goals: 2 / 2 Qed: 2 -[wp] Report 'tests/wp_plugin/mask.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/mask.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/mask.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success compute 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle index 6fc49b800d3..1dc1b577aae 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle @@ -9,7 +9,8 @@ [wp] Proved goals: 3 / 3 Qed: 1 Alt-Ergo: 2 -[wp] Report 'tests/wp_plugin/nth.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/nth.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/nth.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic Nth 1 2 (72..96) 3 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle index 053a73d1166..6f80bff20c4 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 4 / 4 Qed: 1 alt-ergo: 3 -[wp] Report 'tests/wp_plugin/nth.i.1.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/nth.1.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/nth.1.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic Nth 1 - 4 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle index 09dcba792d0..863d5beb28b 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.res.oracle @@ -19,7 +19,8 @@ [wp] Proved goals: 8 / 12 Qed: 8 Alt-Ergo: 0 (unsuccess: 4) -[wp] Report 'tests/wp_plugin/overarray.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/overarray.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/overarray.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f1_ok 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle index 35e9b6933aa..388a727ed98 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.res.oracle @@ -19,7 +19,8 @@ [wp] Proved goals: 8 / 12 Qed: 4 Alt-Ergo: 4 (unsuccess: 4) -[wp] Report 'tests/wp_plugin/overassign.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/overassign.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/overassign.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f1_ok 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle index 10ae7236816..f2386c16780 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.res.oracle @@ -7,7 +7,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_plugin/params.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/params.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/params.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma - 1 (1..12) 1 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle index dfed13cf9c8..9bf2920a577 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.res.oracle @@ -7,7 +7,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_plugin/plet.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/plet.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/plet.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Axiomatic Test - 1 (8..20) 1 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle index 32502e791d3..f857fec4d7e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.res.oracle @@ -10,7 +10,8 @@ [wp] [Alt-Ergo] Goal typed_f_assert : Unsuccess (Stronger) [wp] Proved goals: 0 / 1 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_plugin/polarity.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/polarity.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/polarity.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle index f5023a17dc2..0ad90b19749 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/prenex.res.oracle @@ -19,7 +19,8 @@ [wp] Proved goals: 12 / 12 Qed: 7 Alt-Ergo: 5 -[wp] Report 'tests/wp_plugin/prenex.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/prenex.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/prenex.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success diag 7 5 (64..88) 12 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle index c1c8354536c..a9577c59998 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.res.oracle @@ -56,7 +56,8 @@ [wp] Proved goals: 47 / 47 Qed: 42 Alt-Ergo: 5 -[wp] Report 'tests/wp_plugin/repeat.c.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/repeat.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/repeat.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success master 3 - 3 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle index 3749d98a6ad..5bc109acf7a 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle @@ -19,7 +19,8 @@ [wp] Proved goals: 1 / 6 Qed: 1 Alt-Ergo: 0 (unsuccess: 5) -[wp] Report 'tests/wp_plugin/rte.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/rte.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/rte.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job 1 - 5 20.0% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle index 5a6a837e1f4..a9fb5006c56 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.0.res.oracle @@ -46,7 +46,8 @@ [wp] Proved goals: 39 / 39 Qed: 25 Alt-Ergo: 14 -[wp] Report 'tests/wp_plugin/sequence.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/sequence.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/sequence.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success no_calls 5 5 (8..20) 10 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle index 1c817abc79d..e2333a2acdc 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.1.res.oracle @@ -41,7 +41,8 @@ [wp] Proved goals: 34 / 34 Qed: 22 alt-ergo: 12 -[wp] Report 'tests/wp_plugin/sequence.i.1.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/sequence.1.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/sequence.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success no_calls 2 - 5 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle index 06f3a95d39e..5841b9f41a0 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/sequence.2.res.oracle @@ -5,5 +5,6 @@ [wp] Warning: Missing RTE guards [wp] 0 goal scheduled [wp] Proved goals: 0 / 0 -[wp] Report 'tests/wp_plugin/sequence.i.2.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/sequence.2.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/sequence.2.report.json' ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle index b891bec1a72..5e34d21ac61 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/stmt.res.oracle @@ -25,7 +25,8 @@ [wp] [Qed] Goal typed_h_assert_2 : Valid [wp] Proved goals: 10 / 10 Qed: 10 -[wp] Report 'tests/wp_plugin/stmt.c.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/stmt.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/stmt.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 5 - 5 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle index cd836f893d9..deeda948d38 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.res.oracle @@ -51,7 +51,8 @@ [wp] Proved goals: 44 / 44 Qed: 23 Alt-Ergo: 21 -[wp] Report 'tests/wp_plugin/string_c.c.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/string_c.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/string_c.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success memcpy 6 6 (864..960) 12 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle index 5d5925a673e..71fab82397e 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct.res.oracle @@ -24,7 +24,8 @@ [wp] [Qed] Goal typed_id_ensures_qed_ok_P2 : Valid [wp] Proved goals: 18 / 18 Qed: 18 -[wp] Report 'tests/wp_plugin/struct.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/struct.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/struct.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success id 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle index 14cfd26a072..1ee633fed3a 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/struct_hack.res.oracle @@ -23,7 +23,8 @@ [wp] Proved goals: 10 / 10 Qed: 6 Alt-Ergo: 4 -[wp] Report 'tests/wp_plugin/struct_hack.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/struct_hack.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/struct_hack.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f0 3 2 (24..36) 5 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle index bf2ffa73ad3..326d5fff53c 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.res.oracle @@ -8,8 +8,9 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_plugin/subset.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/subset.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/subset.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -mem - 1 (128..152) 1 100% +mem - 1 (120..144) 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle index b6125143bf1..0c8d87d6a6b 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.res.oracle @@ -12,8 +12,9 @@ [wp] Proved goals: 4 / 5 Qed: 3 Alt-Ergo: 1 (unsuccess: 1) -[wp] Report 'tests/wp_plugin/subset_fopen.c.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/subset_fopen.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/subset_fopen.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -f 3 1 (80..104) 5 80.0% +f 3 1 (88..112) 5 80.0% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle index 2c19f508dd4..afd697426f5 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle @@ -11,7 +11,8 @@ [wp] Proved goals: 3 / 4 Qed: 1 Alt-Ergo: 2 (unsuccess: 1) -[wp] Report 'tests/wp_plugin/trig.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/trig.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/trig.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success foo 1 2 (48..60) 4 75.0% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle index 6ce8eaf3651..5c821da84d4 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 3 / 3 Qed: 2 Alt-Ergo: 1 -[wp] Report 'tests/wp_plugin/unsafe-arrays.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/unsafe-arrays.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/unsafe-arrays.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 2 1 (16..28) 3 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle index 8a4e9399f45..7cae1e5971d 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle @@ -7,7 +7,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Script: 1 -[wp] Report 'tests/wp_plugin/unsigned.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/unsigned.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/unsigned.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma - - (4..16) 1 100% diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle index b8aa2126915..fa61ef3d94b 100644 --- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle +++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.res.oracle @@ -12,7 +12,8 @@ [wp] Proved goals: 1 / 2 Qed: 1 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_plugin/unsupported_init.i.0.report.json' +[wp] Report in: 'tests/wp_plugin/oracle_qualif/unsupported_init.0.report.json' +[wp] Report out: 'tests/wp_plugin/result_qualif/unsupported_init.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 1 - 2 50.0% diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle index 1106baba2b2..a59963da14d 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/array.res.oracle @@ -8,7 +8,8 @@ [wp] [Qed] Goal typed_g_ensures_P_addr_shift_qed_ok : Valid [wp] Proved goals: 2 / 2 Qed: 2 -[wp] Report 'tests/wp_store/array.i.0.report.json' +[wp] Report in: 'tests/wp_store/oracle_qualif/array.0.report.json' +[wp] Report out: 'tests/wp_store/result_qualif/array.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success g 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle index 66190d57ab9..bf77aed24b2 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/natural.res.oracle @@ -9,7 +9,8 @@ [wp] [Qed] Goal typed_f_assigns_part2 : Valid [wp] Proved goals: 3 / 3 Qed: 3 -[wp] Report 'tests/wp_store/natural.i.0.report.json' +[wp] Report in: 'tests/wp_store/oracle_qualif/natural.0.report.json' +[wp] Report out: 'tests/wp_store/result_qualif/natural.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 3 - 3 100% diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle index 3dc493d3e12..009ad490235 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.0.res.oracle @@ -9,7 +9,8 @@ [wp] Proved goals: 2 / 2 Qed: 0 Alt-Ergo: 2 -[wp] Report 'tests/wp_store/nonaliasing.i.0.report.json' +[wp] Report in: 'tests/wp_store/oracle_qualif/nonaliasing.0.report.json' +[wp] Report out: 'tests/wp_store/result_qualif/nonaliasing.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - 2 (24..36) 2 100% diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle index c491cb3a4d4..ef2e7cc9a81 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/nonaliasing.1.res.oracle @@ -8,7 +8,8 @@ [wp] [Alt-Ergo] Goal typed_f_ensures_qed_ko_Q_oracle_ko : Unsuccess [wp] Proved goals: 0 / 2 Alt-Ergo: 0 (unsuccess: 2) -[wp] Report 'tests/wp_store/nonaliasing.i.1.report.json' +[wp] Report in: 'tests/wp_store/oracle_qualif/nonaliasing.1.report.json' +[wp] Report out: 'tests/wp_store/result_qualif/nonaliasing.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - - 2 0.0% diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle index f024426f2ef..1978be6ecd1 100644 --- a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle +++ b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.res.oracle @@ -13,10 +13,11 @@ [wp] Proved goals: 6 / 6 Qed: 3 Alt-Ergo: 3 -[wp] Report 'tests/wp_store/struct.i.0.report.json' +[wp] Report in: 'tests/wp_store/oracle_qualif/struct.0.report.json' +[wp] Report out: 'tests/wp_store/result_qualif/struct.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success g 2 - 2 100% -f 1 1 (20..32) 2 100% +f 1 1 (16..28) 2 100% main - 2 (36..48) 2 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle index c11cdf6e713..066b6e99fb7 100644 --- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle +++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle @@ -10,7 +10,8 @@ [wp] [Tactical] Goal typed_split_ensures_Hyp_Forall_And : Unsuccess [wp] [Tactical] Goal typed_split_ensures_Hyp_Forall_Or_bis : Unsuccess [wp] Proved goals: 0 / 5 -[wp] Report 'tests/wp_tip/tac_split_quantifiers.i.0.report.json' +[wp] Report in: 'tests/wp_tip/oracle_qualif/tac_split_quantifiers.0.report.json' +[wp] Report out: 'tests/wp_tip/result_qualif/tac_split_quantifiers.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success split - - 5 0.0% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle index 55bc508f1a9..dce5ad05602 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.0.res.oracle @@ -14,12 +14,13 @@ [wp] Proved goals: 5 / 5 Qed: 1 Alt-Ergo: 4 -[wp] Report 'tests/wp_typed/array_initialized.c.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/array_initialized.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/array_initialized.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success main1 - 1 (1..12) 1 100% main2 - 1 (96..120) 1 100% main3 1 - 1 100% -main_pointer - 1 (36..48) 1 100% +main_pointer - 1 (40..52) 1 100% simpl - 1 (16..28) 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle index 87594e50f05..71bf98b2365 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/array_initialized.1.res.oracle @@ -14,12 +14,13 @@ [wp] Proved goals: 5 / 5 Qed: 1 Alt-Ergo: 4 -[wp] Report 'tests/wp_typed/array_initialized.c.1.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/array_initialized.1.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/array_initialized.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success main1 - 1 (16..28) 1 100% main2 - 1 (112..136) 1 100% main3 1 - 1 100% -main_pointer - 1 (72..96) 1 100% +main_pointer - 1 (64..88) 1 100% simpl - 1 (16..28) 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle index ea8b44d41a6..1ab64635715 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle @@ -9,7 +9,8 @@ [wp] [Qed] Goal typed_g_call_f_requires : Valid [wp] Proved goals: 1 / 1 Qed: 1 -[wp] Report 'tests/wp_typed/avar.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/avar.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/avar.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success g 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle index bc4d77cc431..2c09f2a29b7 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.res.oracle @@ -12,7 +12,8 @@ [wp] Proved goals: 5 / 5 Qed: 2 Alt-Ergo: 3 -[wp] Report 'tests/wp_typed/shift_lemma.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/shift_lemma.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/shift_lemma.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 2 3 (20..32) 5 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle index 2ef7db89cdd..d2f900f731b 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.res.oracle @@ -8,8 +8,9 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_typed/struct_array_type.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/struct_array_type.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/struct_array_type.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -f - 1 (8..20) 1 100% +f - 1 (12..24) 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle index afbfa61d8da..62e63ecccc1 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.0.res.oracle @@ -14,7 +14,8 @@ [wp] Proved goals: 7 / 7 Qed: 4 Alt-Ergo: 3 -[wp] Report 'tests/wp_typed/unit_alloc.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_alloc.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_alloc.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job 2 2 (20..32) 4 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle index 7a194c5adbf..8042ad8094d 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_alloc.1.res.oracle @@ -14,7 +14,8 @@ [wp] Proved goals: 7 / 7 Qed: 4 Alt-Ergo: 3 -[wp] Report 'tests/wp_typed/unit_alloc.i.1.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_alloc.1.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_alloc.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job 2 2 (20..32) 4 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle index a595a3d3871..fe4620e5d8a 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle @@ -68,10 +68,11 @@ [wp] Proved goals: 61 / 61 Qed: 41 Alt-Ergo: 20 -[wp] Report 'tests/wp_typed/unit_bitwise.c.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_bitwise.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_bitwise.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success -Lemma 10 8 (28..40) 18 100% +Lemma 10 8 (32..44) 18 100% ------------------------------------------------------------- Functions WP Alt-Ergo Total Success band_int 2 - 2 100% @@ -99,7 +100,7 @@ bor_uchar 1 - 1 100% bxor_uchar 1 1 (12..24) 2 100% bnot_uchar 1 - 1 100% lshift_uchar 1 - 1 100% -rshift_uchar - 1 (24..36) 1 100% +rshift_uchar - 1 (20..32) 1 100% band1_ushort 1 1 (12..24) 2 100% band1_ulong 1 1 (12..24) 2 100% cast 8 - 8 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle index 07921fa2d8e..537c54ddc92 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.1.res.oracle @@ -10,7 +10,8 @@ [wp] [Alt-Ergo] Goal typed_cast_assert_ko : Unsuccess [wp] Proved goals: 0 / 4 Alt-Ergo: 0 (unsuccess: 4) -[wp] Report 'tests/wp_typed/unit_bitwise.c.1.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_bitwise.1.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_bitwise.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success band_int - - 1 0.0% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle index 73abc007aa2..2c2a8a3c9af 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_typed/unit_call.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_call.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_call.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job - 1 (1..12) 1 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle index 67b88136c1a..b3a20993756 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.res.oracle @@ -10,8 +10,9 @@ [wp] Proved goals: 1 / 1 Qed: 0 Alt-Ergo: 1 -[wp] Report 'tests/wp_typed/unit_cast.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_cast.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_cast.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -f - 1 (20..32) 1 100% +f - 1 (16..28) 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle index 0bc7e2733a3..92af795f9ed 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.res.oracle @@ -8,7 +8,8 @@ [wp] [Qed] Goal typed_f_ensures_B : Valid [wp] Proved goals: 2 / 2 Qed: 2 -[wp] Report 'tests/wp_typed/unit_cst.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_cst.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_cst.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle index 8e9d20e5c73..419e4dca2d7 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_float.res.oracle @@ -15,7 +15,8 @@ [wp] [Qed] Goal typed_main_ensures_VAR_D : Valid [wp] Proved goals: 6 / 6 Qed: 6 -[wp] Report 'tests/wp_typed/unit_float.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_float.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_float.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success main 6 - 6 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle index 911633abb53..de308aaa970 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 2 / 3 Qed: 2 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_typed/unit_hard.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_hard.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_hard.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success main 2 - 3 66.7% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle index 2bf33e40c9f..0953d5b7dff 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.res.oracle @@ -7,7 +7,8 @@ [wp] [Qed] Goal typed_check_ensures : Valid [wp] Proved goals: 1 / 1 Qed: 1 -[wp] Report 'tests/wp_typed/unit_ite.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_ite.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_ite.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success check 1 - 1 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle index 7e46e25582e..de344cecde4 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 3 / 3 Qed: 0 Alt-Ergo: 3 -[wp] Report 'tests/wp_typed/unit_labels.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_labels.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_labels.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success duplet - 3 (20..32) 3 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle index 20ba906fa59..862caecbcc6 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_lemma.res.oracle @@ -12,7 +12,8 @@ [wp] Proved goals: 5 / 6 Qed: 0 Alt-Ergo: 5 (unsuccess: 1) -[wp] Report 'tests/wp_typed/unit_lemma.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_lemma.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_lemma.0.report.json' ------------------------------------------------------------- Axiomatics WP Alt-Ergo Total Success Lemma - 1 (1..12) 2 50.0% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle index 7227cb987de..7b03321d59e 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.0.res.oracle @@ -10,9 +10,10 @@ [wp] Proved goals: 3 / 3 Qed: 2 Alt-Ergo: 1 -[wp] Report 'tests/wp_typed/unit_local.c.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_local.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_local.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -foo 1 1 (16..28) 2 100% +foo 1 1 (20..32) 2 100% bar 1 - 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle index 3d3c8a01300..8fabfa0574c 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_local.1.res.oracle @@ -10,9 +10,10 @@ [wp] Proved goals: 3 / 3 Qed: 0 Alt-Ergo: 3 -[wp] Report 'tests/wp_typed/unit_local.c.1.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_local.1.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_local.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -foo - 2 (20..32) 2 100% -bar - 1 (20..32) 1 100% +foo - 2 (24..36) 2 100% +bar - 1 (24..36) 1 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle index 5bc492834ba..57cb79e4e5a 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.0.res.oracle @@ -11,7 +11,8 @@ [wp] Proved goals: 1 / 2 Qed: 1 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_typed/unit_loopscope.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_loopscope.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_loopscope.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 1 - 2 50.0% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle index 36b4aa5e260..b4265807aa1 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_loopscope.1.res.oracle @@ -11,7 +11,8 @@ [wp] Proved goals: 1 / 2 Qed: 1 Alt-Ergo: 0 (unsuccess: 1) -[wp] Report 'tests/wp_typed/unit_loopscope.i.1.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_loopscope.1.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_loopscope.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f 1 - 2 50.0% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle index de8017ed01f..919588fef2e 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.res.oracle @@ -10,7 +10,8 @@ [wp] Proved goals: 2 / 3 Qed: 1 Alt-Ergo: 1 (unsuccess: 1) -[wp] Report 'tests/wp_typed/unit_matrix.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_matrix.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_matrix.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success make 1 1 (8..20) 3 66.7% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle index 93cfd59ec4c..083278e533f 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_string.res.oracle @@ -13,7 +13,8 @@ [wp] Proved goals: 6 / 6 Qed: 0 Alt-Ergo: 6 -[wp] Report 'tests/wp_typed/unit_string.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_string.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_string.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success f - 6 (128..152) 6 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle index 27f38791eab..ea315d4efb9 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_tset.res.oracle @@ -8,7 +8,8 @@ [wp] [Qed] Goal typed_complex_assigns : Valid [wp] Proved goals: 2 / 2 Qed: 2 -[wp] Report 'tests/wp_typed/unit_tset.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/unit_tset.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/unit_tset.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success complex 2 - 2 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle index fd7d9e0c8a0..f402d529b83 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle @@ -19,7 +19,8 @@ [wp] Proved goals: 12 / 12 Qed: 1 Alt-Ergo: 11 -[wp] Report 'tests/wp_typed/user_bitwise.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/user_bitwise.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/user_bitwise.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success rl1 1 1 (48..60) 2 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle index d070510e463..c19aec44bf2 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.1.res.oracle @@ -5,5 +5,6 @@ [wp] Warning: Missing RTE guards [wp] 0 goal scheduled [wp] Proved goals: 0 / 0 -[wp] Report 'tests/wp_typed/user_bitwise.i.1.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/user_bitwise.1.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/user_bitwise.1.report.json' ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle index 849e9f492f0..8676944fb53 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.res.oracle @@ -39,7 +39,8 @@ [wp] Proved goals: 32 / 32 Qed: 17 Alt-Ergo: 15 -[wp] Report 'tests/wp_typed/user_collect.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/user_collect.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/user_collect.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job 5 - 5 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle index 4f2b39175f7..6f23e12122e 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.res.oracle @@ -15,7 +15,8 @@ [wp] Proved goals: 8 / 8 Qed: 4 Alt-Ergo: 4 -[wp] Report 'tests/wp_typed/user_init.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/user_init.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/user_init.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success init 4 4 (80..104) 8 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle index 6f0d6cc19cc..f4bd7a31924 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.0.res.oracle @@ -26,7 +26,8 @@ [wp] [Qed] Goal typed_job_assigns_normal_part9 : Valid [wp] Proved goals: 20 / 20 Qed: 20 -[wp] Report 'tests/wp_typed/user_injector.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/user_injector.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/user_injector.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job 20 - 20 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle index c2931cef0f2..fcb48c244ad 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_injector.1.res.oracle @@ -22,7 +22,8 @@ [wp] [Qed] Goal typed_ref_job_assigns_normal_part6 : Valid [wp] Proved goals: 16 / 16 Qed: 16 -[wp] Report 'tests/wp_typed/user_injector.i.1.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/user_injector.1.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/user_injector.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job 16 - 16 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle index 5661eb3f32c..74907ae5953 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_rec.res.oracle @@ -25,7 +25,8 @@ [wp] Proved goals: 18 / 18 Qed: 3 Alt-Ergo: 15 -[wp] Report 'tests/wp_typed/user_rec.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/user_rec.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/user_rec.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success F1 1 5 (24..36) 6 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle index cf3e048e553..53c11f170b9 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.res.oracle @@ -20,8 +20,9 @@ [wp] Proved goals: 13 / 13 Qed: 8 Alt-Ergo: 5 -[wp] Report 'tests/wp_typed/user_string.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/user_string.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/user_string.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success -strlen 8 5 (192..240) 13 100% +strlen 8 5 (208..256) 13 100% ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle index 356adba6493..dce97b342db 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.0.res.oracle @@ -14,7 +14,8 @@ [wp] Proved goals: 7 / 7 Qed: 6 Alt-Ergo: 1 -[wp] Report 'tests/wp_typed/user_swap.i.0.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/user_swap.0.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/user_swap.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success swap 3 1 (16..28) 4 100% diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle index 906d590a10f..a7c01546b43 100644 --- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle +++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_swap.1.res.oracle @@ -12,7 +12,8 @@ [wp] [Qed] Goal typed_ref_swap_assigns : Valid [wp] Proved goals: 6 / 6 Qed: 6 -[wp] Report 'tests/wp_typed/user_swap.i.1.report.json' +[wp] Report in: 'tests/wp_typed/oracle_qualif/user_swap.1.report.json' +[wp] Report out: 'tests/wp_typed/result_qualif/user_swap.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success swap 3 - 3 100% diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle index eb0898c7235..76a422fc787 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat2.res.oracle @@ -17,7 +17,8 @@ [wp] Proved goals: 9 / 9 Qed: 6 Alt-Ergo: 3 -[wp] Report 'tests/wp_usage/caveat2.i.0.report.json' +[wp] Report in: 'tests/wp_usage/oracle_qualif/caveat2.0.report.json' +[wp] Report out: 'tests/wp_usage/result_qualif/caveat2.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success job 6 3 (20..32) 9 100% diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle index fbb344e827f..fb74863e504 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/caveat_range.res.oracle @@ -19,7 +19,8 @@ [wp] Proved goals: 12 / 12 Qed: 7 Alt-Ergo: 5 -[wp] Report 'tests/wp_usage/caveat_range.i.0.report.json' +[wp] Report in: 'tests/wp_usage/oracle_qualif/caveat_range.0.report.json' +[wp] Report out: 'tests/wp_usage/result_qualif/caveat_range.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success reset 7 5 (48..60) 12 100% diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle index 9e0dd0e1713..0e1dae6a162 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.0.res.oracle @@ -37,7 +37,8 @@ [wp] Proved goals: 30 / 30 Qed: 20 Alt-Ergo: 10 -[wp] Report 'tests/wp_usage/issue-189-bis.i.0.report.json' +[wp] Report in: 'tests/wp_usage/oracle_qualif/issue-189-bis.0.report.json' +[wp] Report out: 'tests/wp_usage/result_qualif/issue-189-bis.0.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success memcpy_alias_vars 10 5 (544..640) 15 100% diff --git a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle index 94fca76c2fe..03bd04b5525 100644 --- a/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle_qualif/issue-189-bis.1.res.oracle @@ -17,7 +17,8 @@ [wp] Proved goals: 10 / 10 Qed: 7 Alt-Ergo: 3 -[wp] Report 'tests/wp_usage/issue-189-bis.i.1.report.json' +[wp] Report in: 'tests/wp_usage/oracle_qualif/issue-189-bis.1.report.json' +[wp] Report out: 'tests/wp_usage/result_qualif/issue-189-bis.1.report.json' ------------------------------------------------------------- Functions WP Alt-Ergo Total Success memcpy_context_vars 7 3 (96..120) 10 100% -- GitLab