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 981c1640a089eb28da93becc26b57a8c94ce8f96..44d2cc9df1b6f97d45c658ef5f368167a23d3d0f 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 d3b2208c9f1317bc1e3e5219040302803a0fe570..0c1f65eaa9e5293ae3ad8a75f8fb7b66caff2fd9 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 78a9e8c0f3f8beeca2bb660c464f5da3455dc46d..157a14e1b00a29ae3aa600a75936fefc2a24fc24 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 bc1f4d8ead03c9525aa99d4317548402bc40f1a8..cd60d0cd973fad59e8645ad2e6a49b760e2b2a03 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 a61b5e65e10962836fd6e80269d7b38b84b0126a..fee194ce70ab07b10bf6bdf595543c7b59b09f82 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 e838815abc14a013119915deda971041887722ba..7854eff46a02c66e3dea8967e0a5a291b04e8574 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 71f60a8745347a66874fab4ead9a29e3611c196b..84aee82ec3fc8ef59407fedf0bb80a2849af5a7f 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 e9dcd2c5a7a2cb592854cd7ce39ab81f151403c8..a3a8108a43bbd68b5a4c82cf710073c55b5469ac 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 67dde50a424bc42ba6b80701fccdf266405bc14e..799cfbbb52fed7e01069a9341b943ef5832dddc0 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 cb994356b5b0a1d0d6dfab1cf301f3069c5c05f7..77221b177c2c71ebaa90e84a7e2dea2c0a00b2ab 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 898e9cdc2f924828edf032058bd9a72fc90f9ed8..41dc0500286f88b90aa865f0290ec41013b6cec1 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 c2e202de26b33c5638730e308d0680514e515639..9c8b4033d74fa66070b3fcaf33c92e7f32e08811 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 62dbc55d245fe4e925d2a1ac63591c34370e0f28..82f100d322f129984666ad7e186bd8673fd63f5d 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 1af8a459bfdeb0960a2d12dd1ead540356b54878..2b8385a1071f30a55871d62f94d5a6374f73686e 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 4db477821a2d5675f28755aca8f3efd79f3afa9b..b27b33bf6343c817b308cfbe7c3b65707afcd864 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 74ff28899fe122380fc43713123a188e008b450d..8cc292011a2e990c06eb16a4358534a2838783b0 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 9a78b68f273bf6996386d03a365069f903433e68..f7415f64fd88de5297f7b754f8c158b87b12b6b3 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 6033f7105e78cd4d628f8150f778cbaf3f2b1b0c..390d53bf0412ddd2efdcb14ee243488d5711a702 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 354a7ea0d71689e221ef9fc4f3deda3e53b09e2c..18381fdbb2102384652057fa559505bd9ca58cfe 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 611902c77198d2497583e1192684e48bb11448db..7c556d4141806acc8dcdadc91ed88bbcb6347e44 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 9c3208e5ffa54dd8cc1b031e2e4c5e0110805c98..8b1d5a84d044fc00c49ce69f153e624bcb2868dc 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 bc588e84733e9a0de61ff9ee6dab315e55d40340..7f42f9cb83729f518fb1182d827e599231a62026 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 deffb65d65798e68d83a9da6ba2a2c9de2fa859b..23662c229a18e74fe5e3d0f7f21df5fa5ae031f6 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 1e773b52273de86d9f36b4e825be5eaec60f0c93..700bf0431199f2d502636b7fcf5848e07346f6ad 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 6e34345f147116099c1622515dd63fb4e3e7de30..282eb4ee097169d400ac6fda89f02bba2f624197 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 3d3ad3145f0e68bbe2994c8f0aded0eeb5c642e3..0a7e3253df588aa2b43899d8479bb081997009ad 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 e7b1cca13f1c7f69fbf490a84061ed866318994f..5f939cfa00682f4ce6e5265b6c8eaa39fdf68e73 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 445532eb63d57b2cfa5489a3454ad2859ac54eed..365e6a88d35790dd2586b4950b6bb33d9727a927 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 828ad921cb7fc2d46ee73514a319c1d5d5330e5c..d0b001c2edc097127a4258a4203f7296d3b6ecd4 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 4710a979b9fec752a3813171ab64bef7cab9603a..8a073f77487782051be3164c2508dd1e28e717ec 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 33a7efd8bc0ee2889c1b612813747638acc9c1ea..122f044fbd9a7094e8143e6380cdd29441734a39 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 b4b67bf6b9fc6af79eeb7a71aae4388331a80215..acfc1883f380065d8b9fdcfebbf1911785f80b77 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 0619f73d418710651fd29071598ac152e5d46f4e..696cfec43770e4113b397f51767d8f05354ec8ec 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 ab90d518152d0b9470b56a19d016b350fc73b81c..1a296d83d67ebda972d530fa0d7d997e1c5a4aa8 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 aeadf11adb3ff7326101e7ced83584da67ca0ab7..5a8aa566288b0a70932a36a91533a212901b4301 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 aa952f482657fa24e4a8d422a41045c85f63defa..296bd09f24506c7401d15f4e09972c109e1077fb 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 8d0656392ab9562d5fac2ba00346bb22c896e69d..e067872acde23064e23b12034cb86fa21ed4d955 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 32bbae5f36c05d490ab9e9ca2550da3fcd34c2b6..d304a79b974cb39d1b78cba8c20495e0a9080c7d 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 26b176ac8f201f65fc9bb05568dae7c130f0faa9..a5be47ac2193ae3620930ed953b31516bf056d01 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 26c8030d9dac191617788700e6e1cdd7118eb509..7ce65969029e1591f77b3a87d19e40e3e7469904 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 1d6e4b7c5b2eb68d7ca0b4629b29969acf284380..8ff84050d33d4acc65f7c2a20f604808f8583b3f 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 b319d2b25373519a08ebc79571aae33c600994b4..4476b69cd15b063a0bc15a8ba1d2d4817938041b 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 77732b04cfe1ee2bf3dc38ce6b3fc7dcc9bb6fd3..116c8aee7c979114cb20b8f68632667fe5781f48 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 4df28dabcef36cee5c289d21963b2625c2369075..6ab33eacbf55e5ac487ffd8da7ebfbf50b2f72c6 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 6326d96688ad9b8c8e24017e0a793f78510c8d54..8e7baea94bb527a45cca32c8dd31aef74092a96f 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 d8de2ea9bacf099e5e588b5bd027f4c83a3d4dc2..364ef5d90afbed8679c44260280c3c436524d825 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 cf9b98a9f724f9762c4a7cfe28c19da16a5f7014..9b09be2000784d88ad7babc99674f49856d96eb8 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 f5b9a5420564d1bf4008a47c8532986445da978e..5c3ff3a3d69f9efa257356a7ad8cf7dc3feaed51 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 ccb9ad6d07a333b76c3e2d3057cf3701934066e9..bd1c8449cded0a4723dacb9181908ca5204a7b29 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 a2ea10ac9b80001466ddd948bed20efb069c0c0c..e62b365166bbe3c8a244bfbcda2e78521d917315 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 b5fa183f53fd5aeb360f357364331ac1a78eb0fd..a798b27a5deff30f27bb14482e868ea5fd71c2bb 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 715daac305cf3a7f9bd3862f3a5fbdf07cf4968f..815120bdc30baaa6ff9d6135bed6322d2f2eaba7 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 f8ee684c72dff47b0f3b495a81ca8c5cd5e5785d..f907ba3b6ba1694c33cd8fa9b78da7d56a0c2b4a 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 ef6763632888b42c9e772ebbe7129a1d918ce1b5..68251eed9cb5b73d62ee65c65ebe9bc7602d5247 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 dce325df60f2bbe9a387f7a250800092f12c4ab8..9951d3d26ebdbc95abe40fea8abf1a5e380649e4 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 9c5c4e8af59db1c5d0986aad453f6510bf1d8e92..d85af980df8b7a25256cef5403d430d3db4f415e 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 3ba6b703c8f482e68d1c1f9ea2710c9d22b62720..a63cc1b831ac7698938b81ae92a70447499f3c57 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 25cc92fe77cee318b601983e2da2628116ee64f7..93bcefeddd9c134fd5e798db77b7db5486919eaa 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 d5c9648c9d9d36c855907cc05b7834a541649234..284ab16fc0448c34f1c58dac16649307a38983b3 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 285de12567f3fb8541df408749b407d2be860323..6822d60dd5bcd79a8825366fa1c45c8f3e84b68b 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 e3c4552cbe9e0350037d723724eb26bf370a4e81..d6277a5e6bf5b9ea513b433c204cb84b88e563cd 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 e25eb05dbab6975d2e0eeff52c68aa272b31be9f..105df712f0f95a13264f8bd0ca223867ce8fd395 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 7c13800bcbd80cc30eb3e33e45c258442803897a..cb7876bede3ee24d7b39b88b341b6cd775fb6d2f 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 a0f8a4094b891dde4708856b9d9314693778c2d0..c121fa495ee025823f1ad2f583a8e188e5359b76 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 57d0e72ba574007a74eaf0ae8a8eac436014c897..07a666590800053f9303aa00cc13edfa369b8ef3 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 a85d715c3e10b2255d810a9265e8cc28f6b25a69..45805894c543f51a696d25ad256eb54160f23108 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 d1038d209ce964f07956d51f84ffd6199d3aad67..e7516bcc0d49ab5fb42666ae5315a060db847072 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 cb41d88104fd80cfd5ba1d333b1b5d8aa5cc0441..d6e73f126e8f78894ced5261468f63f32e881b1e 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 fb5eda64c69306efa1eff650c49b8cc27ed34889..3b2380fd5788e454e1cdf41df8b4225ece0831a7 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 1c324eef37b4e64a5e03e2568d664d08a010b915..294ec76d1a5cc88f23e78a75739eab63c58af4f8 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 d5c0104b1871bbb379e6971fedb6b04e7b63df99..d02f6600d105c5f16965512ebc8d8c71709a5078 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 300282b34a9d81b83976ae30b4dff16febc45130..943498ad33bc556f69bbd8b64b089ae727cdbca7 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 6a9e1f868ab48a70637f17c7d4da18ed230d449f..38088c7cf0126fbce109cc8eae96e8a6f04e39d8 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 8ab82c08dc1961b269d2d78d86397a7c496ce66f..5cb16f6a76ecb28afc66eb2cc39c2dcdac436dbb 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 c1f6dc0e2ae85a7b1090fc9b62f6cff9ccf983ce..16f842993b43cc5240e408a2b841fe3c6d28c21d 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 c751f5eeda12d3bbc8a6df3537a65426a0f122a0..53e9e1ea9f7eb706569408f00de71b314720c204 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 2eba18f872743e1f50a046c98b6ee976a444222c..f9e05af007b72a6493aac803c235df0ca3470ba4 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 1677f2005a81d60cebb275c80788ae36d70017ed..8cfc20cb4a00759ee052cb50735fc5be8f85bfd7 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 5957c25a9913e5dc7ea2f26f7e16a3c8b80cb32d..50ac59f33c49a42b8b738fb7dd5317b18cf71748 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 adbf79dec6e616503039969d0cb93e2a77983207..16dfd1723cf581db8552f68c092907b3a8faefc9 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 9dadbafaa24ee1ad40967b5a885b19e4631a5c99..2257d0da19c88a25d0346850483234930298ea86 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 57e70441a4b4663e6e31b7c6169a3f605ec8bb7a..cf47b28f62f99ffdb00d0633c68245f87609579e 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 573e4b2c89b03f89d9dc2ddc907d7b20e0fac3a9..2da222911d19ad271fd2deb124a14860cc20d05f 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 2ebb69cf3ce62b852708b76ef3b632ce224546b7..a8efd0f899e481228aa9a4fa4df4a14d0363b1e2 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 5ea347ae63a08dffb3f48d416e613e98e5d2a6ff..87bd09a92c1a27a7c85f4097408b9b7e51f24636 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 e99621a4bbbab527db5d28c33f75b1b83ec2b54e..41fbe2f345b64ba99c45202a9672a835b4a28950 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 51a96c4ae5db0b737d35c75c35bf060b7de4074c..7ed8bcd4eff256a8c62f80dddb0f3132e98cd484 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 ac1e7341c077c06f0af0001fcadce668af855ad1..95860c425144cc1d000b6cc07e2ac2ad1aa4321e 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 0bdfc3c776943da644f8345d5b125927ba59928f..ca1ca40b8f993c4adfd8a8b2c7f4cdb9edc45b56 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 e91fa5af17342cd08086ab3298ca3811c62d36f5..12cb9521f415b4dda0321cbdda5c376a8acec090 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 1588ce4deb13e41cba58c14064dd7b84d43979a9..ac5a52640069fe4f37d2173e5c5c77778a44fa53 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 54c0e393099c80318ef0b908639542e56799eef3..396326b005b520a4b9cf7b9a8c19d8bc591b7d78 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 dd5a5577e64cd94e04a81eac8f0df4277d82c64b..72aefff35c4ec2292a7fa6e640346b8a154dc358 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 ce30257121484b2aec47784e9ff25785521a9566..04777edf3a4fd92a21ed96503454c1ecee85f42b 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 f2115310be12c73ff806d20a362e3eeabfcb6637..6a66fec80b66ba4f17e2b49c1845e884ff7ad725 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 1ff95155e5ec31109591b89fd9b36878a684d65c..ec2a4c65cdce9dd89599842c1ffef0cd58e983bd 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 6de56a443e7b37ed645b49c6286cfd31314cc2ed..a89ecabb4917cebd20a33a6359177f250819a3a9 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 8abf274c23d8b98c9a657d251645fee49e57786a..bd1ae53be939f5a52900951b88fff85298273b94 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 10e32d116c68418a93daaafd59a6a14c5a1030c4..73e1013877364cf56bd48cbe0c2bcf930d18f91c 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 26816b946bcc170a939be8353db3629ba7f9c343..38e6e69735bc5395f7fb440780ead0b889027d57 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 d0b99a55052bde7b45bcb91f3d9afc39187fe309..7f355b798b96c37584e731913685a1d92465281e 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 f6c7d899a1f37a9561682e1ec34d18b4ef2cbde9..023df5320174c35ff59c9d7069b36a2ab8759f92 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 9f3c90d052e8a448ea99c80edf454c9ae947581f..e18208021ccb21482035e39a7353f2c3dcf98688 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 d0dfe75fac52c9efcdae60e06be6da8e14e485d0..989780bb7368e751fdf4c5190a5c19f98798be23 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 a161e9ffe1ac8e3a7b642b9b709488ac42de314d..1f12910a8ffad576f9686a47a922db0b386fc1b6 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 9a06ba323da0f3b3a58310313fea680ea1ea3bcd..2c4e686d0068136bf3b52b8aa57a10524795fac3 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 47e4dd7697ad9feb12aac921891fdf9f55510036..48086704159f2ada6f138fe2cd1891cc34ca2d39 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 f2a287c6cab427d1267d03d387c447b8b77e2a90..92d91196a20c333a0a52ff588158e7b6cd8f4c85 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 8233499c143b401b5d27b82a69923b76ad01c976..c815416dfcb7d2425655a89eeb9d79ee32fbdf9f 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 0dd9bdf4efe543c3438e155deb4a11b58c01ee85..4644bd595c504b48d581aba08cfd9f22c425517d 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 67424143d7c240bb97b18c1e09e9776d83c403c7..602cb3ba09ce0aef042e1645775c548aa36707fb 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 9b452f762f81e2e35b836d347646f75c95a9b113..048fdb55f65aeaaa5b855ab2e3d0f83e091e16e0 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 bcc5f4a414b76a056d92bef7d68d196490e655cc..4e5bda552479845e6040464eb87f1bed0d51cab6 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 b183563a0deae7e95460759cbeb1ea38d98e6c09..dfe7c1cee8aa9e3a2d403197e5ab63d60291f38c 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 86b06c6e37c50d57f64e004b89391ceee3552108..d8f446952e2c9c38624fcc696fe56559ed491075 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 7380ed072cd7b881d8ce63f92d4a61f2d6980a1d..1782d6f5cbdacdfd1374a14380f769ed4927fad5 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 1e817d3077d7487693e557b8bf7f1a0eef442725..dad1045f7f118963bdf182199a57c44eb74d9cc3 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 da2e3b662c963251c7f6ac368a2714607b8ec0e6..10af4e85904bfedbf5d64000717fd9851833e1c0 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 45650ee45adf5e7a651050fc1fe87b9707e005a0..a1093f1b4861b2d3ae2f15713b6d96b92f040ac0 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 95ecc4413a6883e323c16403071a1dbeed4fc6b2..4ea3ccfbe028f77077cf70ac789a2df3dfeeccdf 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 9b576523536c99e990f8e19427637bdbdbc03739..8361dfbe06c2a3ca456908944745b3358bc40fa3 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 6bcbed6d8bc5e7a4504e35264367d7194cb802e2..04c1d1900f3eafd5005f09ee9ac19469ce4c9b02 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 7f5deafd0c144b5123461d94624167bcb8bf78b4..257e195abe6200da67ee5fb7ab2bfbc5debc38aa 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 30dcd6fe79eccde523862af001b34620751e4679..fd19084848e4bb69f62e11eb504bddccc1dc1684 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 3b6766f387365dc2d167cf6f46cbc22309010830..c940f2f257828dc9727ce00e8e9b816985ee3865 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 0526455b58b5dc46bc8f17946d407ab15427b10b..76f1cf10976f98790acb2a5b72ea22247bc40741 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 93ab36295ede189b5f83413707fe2f79f5e44939..43d789adfdc7cb9ea5c9b4195d6d1cedce936f39 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 e99bbe5258183342cb25e77f585efb9108504d2b..410aec2eb75a43e16863bad4b9b24456ab301491 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 4abab0bd7afe096e8c3a153f482ac9e378135d5f..a4124a02b3e8974b416f926770aed2c4c6e19168 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 2559e2a4b9d05a3b8b3cbec56f4ebabaee63c66a..f2836be71fc2b21813b17e0dcbdcf2b9476b3b67 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 374012968858e66f768f7d9849c4718d417c7403..5200a07c4488d044c1d38dea63b8d9016c62020f 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 635a026579adb9e650a60f95550f2fe18c387ea9..5ff495a8da302893b1a21a52717275a885809ca8 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 1d743b2e6bb3f3c5094dcdd081b4f631a38bb40b..09ce81e04f0428c816e90cdfb6557544702d93bb 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 c34aa5aa74d08ed80530de1041ad854b48d17a96..fddcff86c508b3a6356705a7dfbabee3a451889e 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 fdb495c53576560391b99eb6381076f968a2386f..44b0803a513dd7dab83b26f51789f5570aa9d39f 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 483dc58e36e489c94a8816342e9294de9d3b0439..b16a952d48e905f930846091359a3517e9838920 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 7fa9591a61becc59477b16b43a6397fef16010a2..2f6b498eb88fc5bedd8b1789c3bdaf343cbf8430 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 ec5da8c77e12e512f94b967b80ce3aa01586ff44..66d00763f16308f1cb25fdc1d4786f5a58d06528 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 0eda5beada338fe9c6267459a72a281b97a488eb..8ba6d1158dca607ea86d6cae0c500c620fbaa152 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 fdaf378128c2a1d26a9c3c4bcef66b3f95b3f653..ca355f5d5cd658ef062f0714511e9e8be3939b77 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 7cbec9994f85d3b9a87ec5b66316298e3c4402b9..5bfd4b969d1181a464dfba7b4c2af80db87bcd2d 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 7bf755e5732115dc829fc36879b22a3351e4328c..6ae999d7186054806041fd1f2d52e9c0ab58d1e8 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 66d473a27d59405842479224eeea1aa7688dfc5a..74f07f5036c8bc135f8ff3f59ce1d4c1e6553ffc 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 0eb100dcd2f23c19775b47cc46664a0e8c4d85d8..7de8fa06743f941a264c3524e75d330b87e4bfeb 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 42b8084aefbaca04e2ef438c16c01e6c3bbc72c4..52c22ca6ebd22555710a1e25f6c286643cadbae1 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 3ff1c5aa732ecbf34df088f12321dff3de625cbc..bdc927c48c219b7eef9959b40bfe5d898d8524c9 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 e0af8eb53799fbef86d2bfdd619a92a101474602..646eb1516ce72a4b7aad5cbb78e02d3390957c74 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 6fc49b800d3c589ae76b0869deadd7ad2793ab9b..1dc1b577aae1af624cfa88538e4f7f219f9fee43 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 053a73d1166b3a091a0984815497ce179273e72f..6f80bff20c45fd87f851cdfef06e10d470d4b85a 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 09dcba792d0c72d1783d78b2192292735dd860b2..863d5beb28bf605c847983917157ffd99d0f4057 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 35e9b6933aa7d334cc0cafe94f3af6114b81fc1c..388a727ed98a1ef38821ed9cb29fa3c1ded9981d 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 10ae7236816c170cf89c24590a5c7a7a7f7f328c..f2386c16780fa0cb08d02fcfd8d38fd4025d97b9 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 dfed13cf9c87b853b2ba18d147efe3d33f8d42e1..9bf2920a577e20f2bf68b2578105ae89a024135f 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 32502e791d3adc44f89e06ea6c9145cd2db5a38a..f857fec4d7ee5b68ae103e9eba3e3e69a857bd99 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 f5023a17dc26e36ee3e34f50e5fbb11f897a7313..0ad90b197499cd6fe689dec7b1c2eb9869b85cf5 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 c1c8354536c7f9ab00785d857bc8efc610538785..a9577c59998c8287c3513a2f1c02642ebd056f5a 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 3749d98a6ad36a1e047d362ed40c4eeb00dcec9c..5bc109acf7a85a1b6883a74fd34729ddba7df872 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 5a6a837e1f40fb311ab80e1027efac39f016df83..a9fb5006c5628e2864ab6cfcdbd24cfc5c426a30 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 1c817abc79dab4752323fb0bbc7f40d711070d22..e2333a2acdc2db9f6a13713185d468dc73581e4a 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 06f3a95d39e4054810095c9fc8d3b7375019cb13..5841b9f41a04c4cd3421d672b1d48249ae51fc45 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 b891bec1a72b0dcb219f3c43738bfe781322f85a..5e34d21ac6158afc5fcc6cc95d490740f7439ff3 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 cd836f893d9450075f4900dc7dde4b8def2dc3b2..deeda948d383dbed1e4a1bb242c0d6923c7a6041 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 5d5925a673ed1be9f1420df468cdb4b363b26237..71fab82397e56fe025f8f43b7b9e9e97f745d8e7 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 14cfd26a07272ceb668fc4d14781895b05cbb320..1ee633fed3a3cdec96286839ec24cdf8e9cb870b 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 bf2ffa73ad31c0478dd9788517833a3f646b4659..326d5fff53c35a06468dc4799b65d4dc4f0bda93 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 b6125143bf15f8dae93ff247ff52bea8fdd42c62..0c8d87d6a6b472b42c0bf6934828bb3f5766d192 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 2c19f508dd4fd32298bdcf4d0869d6625af79e4f..afd697426f5cb34653ab23d84fc6ade5ad1f5d8f 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 6ce8eaf3651a1fb1b04a513c56de8fd3e36fe498..5c821da84d4800bd92180a37b866c797cc9e02e8 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 8a4e9399f451a852b7e1338479604b6bf9f45d7a..7cae1e5971dd42cf8a11e746dfb58a853c273089 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 b8aa2126915eed425245450cd6ce34e76a1a1f1d..fa61ef3d94b05772f2a88bb6a68652720de557c1 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 1106baba2b2508b2d93a9bbadc0f80d9923d922e..a59963da14df412c078c9ffaec48d5d7d62c043a 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 66190d57ab983a44e2f9f0832eaecc922d9601d1..bf77aed24b207a9860e72022144157bb927be5fc 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 3dc493d3e125df62da6e67c67b416ffa02179d8b..009ad4902358722519a90bf226a04a77a108cb02 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 c491cb3a4d48773069e4040377eb707baf7aa35b..ef2e7cc9a81a7ab6af13e7aed3b14b3690a14621 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 f024426f2efb92f729f5a8d479f90290696787d8..1978be6ecd1453a86b9fb7dfc8907a24d789fbc6 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 c11cdf6e7134b4bd112c68082f8c10628d23f91b..066b6e99fb74d574ce570e37831dc2d8af94e401 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 55bc508f1a96391f8b5e8b3406c870b63b80a93f..dce5ad05602a5171a4162be6357f773d175f017b 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 87594e50f05a223f6f149c05b3225c34f67e5f5c..71bf98b23654c011b197791a6cd3efb81ff51b0f 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 ea8b44d41a6028c7b9384312669efae2c618bb68..1ab646357155a36acfbb66f17d23ca1922a3c1e9 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 bc4d77cc431790076dbb90c61072acdb5f86a902..2c09f2a29b7f2bb4fdc82a85cba78533cd379f94 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 2ef7db89cdd4f28c0e01042bb9d4c958f3cdaf5f..d2f900f731ba1401d59a4b70b5cdc7c809a461a8 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 afbfa61d8da8bc9c3ef4cf1f1ed99ae5ca36ea28..62e63ecccc14f0099ac49f86ccc412452798ea7b 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 7a194c5adbf9c96f8495e0d8e9581a0a37ae53b5..8042ad8094d6baa4f69f46077eda52f61d8be3a0 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 a595a3d3871839388679af679265d1bb0c8c12c8..fe4620e5d8ab7231a566dd762147708117d566bc 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 07921fa2d8e21c72ed45aca656d02ac7fb582c10..537c54ddc92494293928a0491c6c910b73fc85e6 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 73abc007aa249cdc35e80d82383efda4fd7b59b5..2c2a8a3c9aff36f9b75a4c890cf6a54eb81b1637 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 67b88136c1a976993c2693f338f304b817fae021..b3a209937560b00d196babe03d520f6fd0a0beda 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 0bc7e2733a382db0f26543c61fb90b1017700553..92af795f9ed319748186f2c7a153796abc0605c9 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 8e9d20e5c7387bf1c1a5a36137a9a7353329aa1f..419e4dca2d7cbd907d9a70bd52b5752c13ef7aa7 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 911633abb53918de798479223d34a5dc6ead8be5..de308aaa970e18802dd41372444c08e2134b8bef 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 2bf33e40c9f2eac3d57bcd02040efbae8ab93899..0953d5b7dff66ee612ccc9efb9e3249b78b5e6b3 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 7e46e25582e8429d100714ee198f8b908d97bdfd..de344cecde49795f3fc4a32185e94e118f62ef88 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 20ba906fa590daff417528bb0f15233addf2d1bb..862caecbcc65754d04152176e542a349e30d43bd 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 7227cb987de43a153c9ed0c16e54ffe88f7b972f..7b03321d59e121dcea0ce52d3de5492d0cff7192 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 3d3c8a01300184dcaea4550d2fd3a2d11f8ad975..8fabfa0574c11028a4b6b53c8a4087669163a65a 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 5bc492834ba6ae6bf598ea37d07a0a8abc89de5b..57cb79e4e5a416143989117851269d90800912ee 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 36b4aa5e260103639b72a2bc50fd5c932602fabe..b4265807aa1c2ebd6a577e25b605aca8d2748045 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 de8017ed01f1bc776acbb2cbaa2e6cd0427c006e..919588fef2ed2d62e387c64e154587439ccfdfe5 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 93cfd59ec4c2bfbea470e88d39c0e2542fb7424a..083278e533f835c498a660190f0ecf4a8846f044 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 27f38791eabe7e1acc381b905d9a26eeb0f7d48c..ea315d4efb9b1d9bb3dd32a24f43ade84b3586da 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 fd7d9e0c8a0ebfa438db6fea1f129d4742391219..f402d529b83c73c95cc42ab0f468d396febb7668 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 d070510e463505c14c26282d9e79141e24594088..c19aec44bf2d1a4a2c8e1c61570927128bff84b0 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 849e9f492f0adecf9aeadf786c6cfc72d2c870ae..8676944fb53b5219663b759b05710eb35ea5ee66 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 4f2b39175f74f0cfd99af1fef3f3e369e2dc8310..6f23e12122e5977d74d6f3134b3006ec57b5ee79 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 6f0d6cc19cc8713e8e96e37c4d9ac57c90256bd9..f4bd7a31924dad1a92bddc9cce789d79398b8502 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 c2931cef0f2e16299f2fd4670d21c35a6468007e..fcb48c244ad82a7c1d19e95e52f14d51aa7a857c 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 5661eb3f32c1555b8971f937cf7337c7edb420e6..74907ae59530f8119f5a9981ba4dba4a2854b85f 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 cf3e048e553914572b5690448ec6824fc6df3fe0..53c11f170b98ca7576a5e4e69b617258ecd9a742 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 356adba64938e304be0caacaa490824307ccac05..dce97b342db62f913776f650de1307fd9acf062e 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 906d590a10fc8344139ea08b1193f85600b1aa05..a7c01546b43e518519d717831544e818131e20a5 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 eb0898c7235b24479b7dcae99ec585a2bdaf16ef..76a422fc787616b3c5be5e76282b84f5a19db89c 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 fbb344e827fa5dfd38b923032eb6904c1d32a5e4..fb74863e50493ba17b8e5c9b4f0fc5870aeb5a95 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 9e0dd0e1713a5e0b06fd9241ffe1ddbc67d80c72..0e1dae6a162627b16bef41e26e86f2edb84b9ad5 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 94fca76c2fe618788f35b401717eb76847b78f12..03bd04b55253e501bdbcb02f435e49686437ca12 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%