From 3c596215e8688e11d760010ace8cf6ec23f20d55 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 25 Feb 2019 11:40:29 +0100
Subject: [PATCH] [wp] adding quail reports as oracles
---
.../wp/oracle_qualif/sharing.0.report.json | 14 ++
.../stmtcompiler_test.0.report.json | 204 ++++++++++++++++++
.../wp/oracle_qualif/wp_eqb.0.report.json | 14 ++
.../oracle_qualif/assign_array.0.report.json | 18 ++
.../oracle_qualif/assigns_path.0.report.json | 45 ++++
.../oracle_qualif/bitwise2.0.report.json | 42 ++++
.../wp_acsl/oracle_qualif/ctor.0.report.json | 14 ++
.../wp_acsl/oracle_qualif/equal.0.report.json | 86 ++++++++
.../oracle_qualif/float_compare.0.report.json | 39 ++++
.../implicit_enum_cast.0.report.json | 14 ++
.../oracle_qualif/init_label.0.report.json | 41 ++++
.../oracle_qualif/intbool.0.report.json | 10 +
.../wp_acsl/oracle_qualif/logic.0.report.json | 138 ++++++++++++
.../wp_acsl/oracle_qualif/null.0.report.json | 33 +++
.../oracle_qualif/sizeof.0.report.json | 20 ++
.../oracle_qualif/unit_bit_test.0.report.json | 38 ++++
.../oracle_qualif/unit_bool.0.report.json | 14 ++
.../oracle_qualif/bts_1462.0.report.json | 64 ++++++
.../oracle_qualif/bts_1586.0.report.json | 39 ++++
.../oracle_qualif/bts_1588.0.report.json | 12 ++
.../oracle_qualif/bts_1601.0.report.json | 45 ++++
.../oracle_qualif/bts_2040.0.report.json | 10 +
.../oracle_qualif/bts_2159.0.report.json | 14 ++
.../ergo_typecheck.0.report.json | 36 ++++
.../oracle_qualif/issue-364.0.report.json | 20 ++
.../oracle_qualif/issue_198.0.report.json | 14 ++
.../oracle_qualif/issue_447.0.report.json | 14 ++
.../oracle_qualif/issue_453.0.report.json | 30 +++
.../oracle_qualif/issue_494.0.report.json | 35 +++
.../oracle_qualif/issue_508.0.report.json | 19 ++
.../wp_plugin/oracle_qualif/asm.0.report.json | 22 ++
.../oracle_qualif/copy.0.report.json | 61 ++++++
.../oracle_qualif/frame.0.report.json | 53 +++++
.../oracle_qualif/ground_real.0.report.json | 12 ++
.../oracle_qualif/init_valid.0.report.json | 30 +++
.../oracle_qualif/loopcurrent.0.report.json | 13 ++
.../oracle_qualif/loopentry.0.report.json | 13 ++
.../oracle_qualif/loopextra.0.report.json | 14 ++
.../oracle_qualif/mask.0.report.json | 14 ++
.../oracle_qualif/overarray.0.report.json | 51 +++++
.../oracle_qualif/overassign.0.report.json | 61 ++++++
.../oracle_qualif/params.0.report.json | 14 ++
.../oracle_qualif/plet.0.report.json | 14 ++
.../oracle_qualif/polarity.0.report.json | 10 +
.../oracle_qualif/repeat.0.report.json | 122 +++++++++++
.../oracle_qualif/string_c.0.report.json | 193 +++++++++++++++++
.../oracle_qualif/subset.0.report.json | 14 ++
.../oracle_qualif/subset_fopen.0.report.json | 36 ++++
.../oracle_qualif/unsafe-arrays.0.report.json | 24 +++
.../unsupported_init.0.report.json | 16 ++
.../oracle_qualif/array.0.report.json | 16 ++
.../oracle_qualif/natural.0.report.json | 12 ++
.../oracle_qualif/struct.0.report.json | 49 +++++
.../wp_typed/oracle_qualif/avar.0.report.json | 8 +
.../oracle_qualif/shift_lemma.0.report.json | 33 +++
.../struct_array_type.0.report.json | 14 ++
.../oracle_qualif/unit_call.0.report.json | 14 ++
.../oracle_qualif/unit_cast.0.report.json | 14 ++
.../oracle_qualif/unit_cst.0.report.json | 11 +
.../oracle_qualif/unit_hard.0.report.json | 26 +++
.../oracle_qualif/unit_ite.0.report.json | 10 +
.../oracle_qualif/unit_labels.0.report.json | 26 +++
.../oracle_qualif/unit_matrix.0.report.json | 29 +++
.../oracle_qualif/user_collect.0.report.json | 181 ++++++++++++++++
.../oracle_qualif/user_init.0.report.json | 50 +++++
.../oracle_qualif/user_string.0.report.json | 63 ++++++
66 files changed, 2479 insertions(+)
create mode 100644 src/plugins/wp/tests/wp/oracle_qualif/sharing.0.report.json
create mode 100644 src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.0.report.json
create mode 100644 src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/null.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.0.report.json
create mode 100644 src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/params.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.0.report.json
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.0.report.json
create mode 100644 src/plugins/wp/tests/wp_store/oracle_qualif/array.0.report.json
create mode 100644 src/plugins/wp/tests/wp_store/oracle_qualif/natural.0.report.json
create mode 100644 src/plugins/wp/tests/wp_store/oracle_qualif/struct.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/avar.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.report.json
create mode 100644 src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.0.report.json
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/sharing.0.report.json b/src/plugins/wp/tests/wp/oracle_qualif/sharing.0.report.json
new file mode 100644
index 00000000000..17a701f571c
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle_qualif/sharing.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 13 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 13 } },
+ "wp:functions": { "f": { "f_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 13 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 13 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 13 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 13 } } } } }
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.0.report.json b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.0.report.json
new file mode 100644
index 00000000000..23c6014c8c9
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.0.report.json
@@ -0,0 +1,204 @@
+{ "wp:global": { "alt-ergo": { "total": 9, "valid": 1, "unknown": 8,
+ "rank": 2 },
+ "qed": { "total": 18, "valid": 18 },
+ "wp:main": { "total": 27, "valid": 19, "unknown": 8,
+ "rank": 2 } },
+ "wp:functions": { "empty": { "empty_assert": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "one_assign": { "one_assign_assert": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "one_if": { "one_if_assert": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "some_seq": { "some_seq_assert_2": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "some_seq_assert": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } },
+ "main_ensures_result": { "main_ensures_result_assert":
+ { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } } },
+ "main": { "main_assert": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "not_main": { "not_main_assert_bad": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } } },
+ "main_assigns_global": { "main_assigns_global_assert_bad":
+ { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "main_assigns_global_assert_2":
+ { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "main_assigns_global_assert":
+ { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main":
+ { "total": 3,
+ "valid": 2,
+ "unknown": 1 } } },
+ "zloop": { "zloop_assert_bad": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "zloop_assert_3": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "zloop_assert_2": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "zloop_assert": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "zloop_loop_invariant": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 1,
+ "unknown": 1 } },
+ "zloop_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 3,
+ "unknown": 3 },
+ "qed": { "total": 4,
+ "valid": 4 },
+ "wp:main": { "total": 7,
+ "valid": 4,
+ "unknown": 3 } } },
+ "behavior2": { "behavior2_assert": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "behavior3": { "behavior3_assert": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "behavior4": { "behavior4_assert": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "behavior5": { "behavior5_assert_bad": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } } },
+ "if_assert": { "if_assert_assert_missing_return":
+ { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "if_assert_assert_3": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "if_assert_assert_2": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "if_assert_assert": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 2 } },
+ "wp:section": { "alt-ergo": { "total": 3,
+ "valid": 1,
+ "unknown": 2,
+ "rank": 2 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 4,
+ "valid": 2,
+ "unknown": 2,
+ "rank": 2 } } },
+ "compare": { "compare_assert": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.0.report.json b/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.0.report.json
new file mode 100644
index 00000000000..37b6284cd83
--- /dev/null
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 10 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 10 } },
+ "wp:functions": { "f": { "f_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 10 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 10 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 10 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 10 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.0.report.json
new file mode 100644
index 00000000000..c9b4abc0b34
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.0.report.json
@@ -0,0 +1,18 @@
+{ "wp:global": { "qed": { "total": 4, "valid": 4 },
+ "wp:main": { "total": 4, "valid": 4 } },
+ "wp:functions": { "jobA": { "jobA_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } },
+ "jobG": { "jobG_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.0.report.json
new file mode 100644
index 00000000000..a3e18b8a1f1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.0.report.json
@@ -0,0 +1,45 @@
+{ "wp:global": { "alt-ergo": { "total": 3, "valid": 3, "rank": 6 },
+ "qed": { "total": 6, "valid": 6 },
+ "wp:main": { "total": 9, "valid": 9, "rank": 6 } },
+ "wp:functions": { "job": { "job_loop_invariant_2": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 6 } },
+ "job_loop_invariant": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 4 } },
+ "job_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "job_loop_assigns": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "job_ensures_A": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 5 } },
+ "job_ensures_N": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 3,
+ "valid": 3,
+ "rank": 6 },
+ "qed": { "total": 6,
+ "valid": 6 },
+ "wp:main": { "total": 9,
+ "valid": 9,
+ "rank": 6 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.0.report.json
new file mode 100644
index 00000000000..80f37475140
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.0.report.json
@@ -0,0 +1,42 @@
+{ "wp:global": { "qed": { "total": 5, "valid": 5 },
+ "wp:main": { "total": 5, "valid": 5 } },
+ "wp:functions": { "job1": { "job1_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "job1bis": { "job1bis_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "job2": { "job2_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "job3": { "job3_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "job4": { "job4_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.0.report.json
new file mode 100644
index 00000000000..891942e3737
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/ctor.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 2, "valid": 2 } },
+ "wp:axiomatics": { "Event": { "lemma_diff": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "lemma_cons": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.report.json
new file mode 100644
index 00000000000..5c43681476a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/equal.0.report.json
@@ -0,0 +1,86 @@
+{ "wp:global": { "alt-ergo": { "total": 5, "valid": 5, "rank": 8 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 6, "valid": 6, "rank": 8 } },
+ "wp:functions": { "simple_struct": { "simple_struct_ensures": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "simple_array": { "simple_array_ensures": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 4 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 4 } } },
+ "with_array_struct": { "with_array_struct_ensures":
+ { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 4 } },
+ "wp:section": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 4 } } },
+ "with_ptr_struct": { "with_ptr_struct_ensures": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 2 } },
+ "wp:section": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 2 } } },
+ "with_ptr_array": { "with_ptr_array_ensures": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 4 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 4 } } },
+ "with_ptr_and_array_struct": { "with_ptr_and_array_struct_ensures":
+ { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "wp:section": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.report.json
new file mode 100644
index 00000000000..8ab9ce87bfc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.0.report.json
@@ -0,0 +1,39 @@
+{ "wp:global": { "alt-ergo": { "total": 4, "valid": 4, "rank": 8 },
+ "wp:main": { "total": 4, "valid": 4, "rank": 8 } },
+ "wp:axiomatics": { "": { "lemma_test_float_compare_greater": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "lemma_test_float_compare": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "lemma_test_double_compare_greater": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "lemma_test_double_compare": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "wp:section": { "alt-ergo": { "total": 4,
+ "valid": 4,
+ "rank": 8 },
+ "wp:main": { "total": 4,
+ "valid": 4,
+ "rank": 8 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.0.report.json
new file mode 100644
index 00000000000..ed396bf7e29
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/implicit_enum_cast.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "qed": { "total": 9, "valid": 9 },
+ "wp:main": { "total": 9, "valid": 9 } },
+ "wp:functions": { "bar": { "bar_assigns": { "qed": { "total": 8,
+ "valid": 8 },
+ "wp:main": { "total": 8,
+ "valid": 8 } },
+ "bar_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 9,
+ "valid": 9 },
+ "wp:main": { "total": 9,
+ "valid": 9 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.0.report.json
new file mode 100644
index 00000000000..3d33c8c50aa
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.0.report.json
@@ -0,0 +1,41 @@
+{ "wp:global": { "alt-ergo": { "total": 2, "valid": 1, "unknown": 1,
+ "rank": 5 },
+ "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 4, "valid": 3, "unknown": 1,
+ "rank": 5 } },
+ "wp:functions": { "main": { "main_requires_OK": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "job": { "job_ensures_OK": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 5 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 5 } } },
+ "foreign": { "foreign_ensures_OK": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "extra": { "extra_ensures_KO": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.0.report.json
new file mode 100644
index 00000000000..4ed4a7c4e63
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/intbool.0.report.json
@@ -0,0 +1,10 @@
+{ "wp:global": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1, "valid": 1 } },
+ "wp:functions": { "bug": { "bug_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.report.json
new file mode 100644
index 00000000000..badcee8deb0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/logic.0.report.json
@@ -0,0 +1,138 @@
+{ "wp:global": { "alt-ergo": { "total": 18, "valid": 2, "unknown": 16,
+ "rank": 16 },
+ "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 21, "valid": 5, "unknown": 16,
+ "rank": 16 } },
+ "wp:functions": { "h": { "h_assigns": { "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "h_ensures": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 3,
+ "valid": 2,
+ "unknown": 1 } } },
+ "main": { "main_requires_qed_ok_18": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_17": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_16": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_15": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_14": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_13": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_12": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_11": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_10": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_9": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_8": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_7": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_6": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_5": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_4": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_qed_ok_3": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 16 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 16 } },
+ "main_requires_qed_ok_2": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 16 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 16 } },
+ "main_requires_qed_ok": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 17,
+ "valid": 2,
+ "unknown": 15,
+ "rank": 16 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 18,
+ "valid": 3,
+ "unknown": 15,
+ "rank": 16 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.0.report.json
new file mode 100644
index 00000000000..79fbcb44621
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.0.report.json
@@ -0,0 +1,33 @@
+{ "wp:global": { "alt-ergo": { "total": 2, "valid": 2, "rank": 1 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 3, "valid": 3, "rank": 1 } },
+ "wp:axiomatics": { "": { "lemma_valid_read_non_null": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 1 } },
+ "lemma_valid_non_null": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "valid": 2,
+ "rank": 1 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 1 } } } },
+ "wp:functions": { "null_is_zero": { "null_is_zero_ensures": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json
new file mode 100644
index 00000000000..bd9ed2f8299
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json
@@ -0,0 +1,20 @@
+{ "wp:global": { "alt-ergo": { "total": 2, "valid": 2, "rank": 1 },
+ "wp:main": { "total": 2, "valid": 2, "rank": 1 } },
+ "wp:functions": { "foo": { "foo_assert_B": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } },
+ "foo_assert_A": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "valid": 2,
+ "rank": 1 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.0.report.json
new file mode 100644
index 00000000000..6c8cdc3f855
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bit_test.0.report.json
@@ -0,0 +1,38 @@
+{ "wp:global": { "alt-ergo": { "total": 2, "valid": 1, "unknown": 1,
+ "rank": 13 },
+ "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 4, "valid": 3, "unknown": 1,
+ "rank": 13 } },
+ "wp:functions": { "sum": { "sum_ensures_ko": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "sum_ensures_ok": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 1,
+ "unknown": 1 } } },
+ "rotate_left": { "rotate_left_ensures_other_bits":
+ { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 13 },
+ "wp:main": { "total": 1, "valid": 1,
+ "rank": 13 } },
+ "rotate_left_ensures_bit_zero":
+ { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 13 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 13 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.0.report.json
new file mode 100644
index 00000000000..cce14a76fc5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/unit_bool.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 1 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 1 } },
+ "wp:axiomatics": { "Foo": { "lemma_f_1": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.0.report.json
new file mode 100644
index 00000000000..0719103e8bc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1462.0.report.json
@@ -0,0 +1,64 @@
+{ "wp:global": { "alt-ergo": { "total": 3, "valid": 2, "unknown": 1,
+ "rank": 2 },
+ "qed": { "total": 10, "valid": 10 },
+ "wp:main": { "total": 13, "valid": 12, "unknown": 1,
+ "rank": 2 } },
+ "wp:functions": { "wrong": { "wrong_assert_consequence_of_false_invariant":
+ { "alt-ergo": { "total": 1, "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1, "valid": 1,
+ "rank": 2 } },
+ "wrong_loop_invariant_C": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2 } },
+ "wrong_loop_invariant_B": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2 } },
+ "wrong_loop_invariant_A_KO": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 1,
+ "unknown": 1 } },
+ "wrong_assert_for_value": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 1 } },
+ "wrong_loop_assigns": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 3,
+ "valid": 2,
+ "unknown": 1,
+ "rank": 2 },
+ "qed": { "total": 6,
+ "valid": 6 },
+ "wp:main": { "total": 9,
+ "valid": 8,
+ "unknown": 1,
+ "rank": 2 } } },
+ "local": { "local_loop_invariant": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "local_loop_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 4,
+ "valid": 4 },
+ "wp:main": { "total": 4,
+ "valid": 4 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.0.report.json
new file mode 100644
index 00000000000..c8f7254db67
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1586.0.report.json
@@ -0,0 +1,39 @@
+{ "wp:global": { "alt-ergo": { "total": 2, "unknown": 2 },
+ "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 4, "valid": 2, "unknown": 2 } },
+ "wp:functions": { "compute_bizarre": { "compute_bizarre_Bizarre_ensures_TRANS":
+ { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "compute_normal": { "compute_normal_Normal_ensures_TRANS":
+ { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } },
+ "main_bizarre_KO": { "main_bizarre_KO_assert_FALSE":
+ { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } } },
+ "main_normal_KO": { "main_normal_KO_assert_FALSE":
+ { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.0.report.json
new file mode 100644
index 00000000000..20f18a7e95a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1588.0.report.json
@@ -0,0 +1,12 @@
+{ "wp:global": { "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 3, "valid": 3 } },
+ "wp:functions": { "f": { "f_assert_a1": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_loop_invariant_l1_2": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 3,
+ "valid": 3 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.0.report.json
new file mode 100644
index 00000000000..406e1c61d89
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1601.0.report.json
@@ -0,0 +1,45 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 5 },
+ "qed": { "total": 7, "valid": 7 },
+ "wp:main": { "total": 8, "valid": 8, "rank": 5 } },
+ "wp:functions": { "foo": { "foo_assert_7": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "foo_assert_6": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "foo_assert_5": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "foo_assert_4": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "foo_assert_3": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "foo_assert_2": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "foo_assert": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 5 } },
+ "foo_basic_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "qed": { "total": 7,
+ "valid": 7 },
+ "wp:main": { "total": 8,
+ "valid": 8,
+ "rank": 5 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.0.report.json
new file mode 100644
index 00000000000..576a872d9da
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2040.0.report.json
@@ -0,0 +1,10 @@
+{ "wp:global": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1, "valid": 1 } },
+ "wp:functions": { "call": { "call_assert": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.0.report.json
new file mode 100644
index 00000000000..d88f27e56ce
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_2159.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 16 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 16 } },
+ "wp:functions": { "job": { "job_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 16 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 16 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 16 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 16 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.0.report.json
new file mode 100644
index 00000000000..414c3cf94d8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/ergo_typecheck.0.report.json
@@ -0,0 +1,36 @@
+{ "wp:global": { "qed": { "total": 8, "valid": 8 },
+ "wp:main": { "total": 8, "valid": 8 } },
+ "wp:functions": { "f": { "f_assigns": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_ensures_var_unit4": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_ensures_var_unit3": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_ensures_var_unit2": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_ensures_var_unit1": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_ensures_var_unit0": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_ensures_var_inline": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_ensures_var_divded": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 8, "valid": 8 },
+ "wp:main": { "total": 8,
+ "valid": 8 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.0.report.json
new file mode 100644
index 00000000000..cd95b6d3b70
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue-364.0.report.json
@@ -0,0 +1,20 @@
+{ "wp:global": { "alt-ergo": { "total": 2, "valid": 2, "rank": 8 },
+ "wp:main": { "total": 2, "valid": 2, "rank": 8 } },
+ "wp:functions": { "main": { "main_assert_OVER": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "main_assert_ZERO": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 6 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "valid": 2,
+ "rank": 8 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 8 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.0.report.json
new file mode 100644
index 00000000000..8add84a6b5d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_198.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 2 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 2 } },
+ "wp:axiomatics": { "": { "lemma_broken": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 2 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 2 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json
new file mode 100644
index 00000000000..f93f1005578
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 1 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 1 } },
+ "wp:axiomatics": { "": { "lemma_foo": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.0.report.json
new file mode 100644
index 00000000000..6deccb7f511
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_453.0.report.json
@@ -0,0 +1,30 @@
+{ "wp:global": { "qed": { "total": 6, "valid": 6 },
+ "wp:main": { "total": 6, "valid": 6 } },
+ "wp:functions": { "f1": { "f1_assigns": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f1_loop_assigns": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f1_ensures_Sincr": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 3,
+ "valid": 3 } } },
+ "f2": { "f2_assigns": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f2_loop_assigns": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f2_ensures_Sincr": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 3,
+ "valid": 3 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.0.report.json
new file mode 100644
index 00000000000..d2c13e606a0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_494.0.report.json
@@ -0,0 +1,35 @@
+{ "wp:global": { "alt-ergo": { "total": 3, "valid": 1, "unknown": 2,
+ "rank": 3 },
+ "wp:main": { "total": 3, "valid": 1, "unknown": 2,
+ "rank": 3 } },
+ "wp:functions": { "f": { "f_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 3 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 3 } } },
+ "job_ko_fixed": { "job_ko_fixed_assert_Wrong": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } } },
+ "job_ko_success": { "job_ko_success_assert_Wrong":
+ { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.0.report.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.0.report.json
new file mode 100644
index 00000000000..3c5b3035ee9
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_508.0.report.json
@@ -0,0 +1,19 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 15 },
+ "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 3, "valid": 3, "rank": 15 } },
+ "wp:functions": { "add": { "add_assigns": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 15 },
+ "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 3,
+ "valid": 3,
+ "rank": 15 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 15 },
+ "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 3,
+ "valid": 3,
+ "rank": 15 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.0.report.json
new file mode 100644
index 00000000000..f12a169da4e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/asm.0.report.json
@@ -0,0 +1,22 @@
+{ "wp:global": { "alt-ergo": { "total": 2, "unknown": 2 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 3, "valid": 1, "unknown": 2 } },
+ "wp:functions": { "main": { "main_assert_KO": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "main_assert_OK": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "main_assigns": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 3,
+ "valid": 1,
+ "unknown": 2 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.0.report.json
new file mode 100644
index 00000000000..e77f053555a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/copy.0.report.json
@@ -0,0 +1,61 @@
+{ "wp:global": { "alt-ergo": { "total": 6, "valid": 6, "rank": 39 },
+ "qed": { "total": 4, "valid": 4 },
+ "wp:main": { "total": 10, "valid": 10, "rank": 39 } },
+ "wp:functions": { "copy": { "copy_assert_B": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 39 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 39 } },
+ "copy_assert_A": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 32 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 32 } },
+ "copy_loop_invariant_Copy": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 8 } },
+ "copy_loop_invariant_Range": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 5 } },
+ "copy_assigns": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "copy_loop_assigns": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 23 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 23 } },
+ "copy_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 6 } },
+ "wp:section": { "alt-ergo": { "total": 6,
+ "valid": 6,
+ "rank": 39 },
+ "qed": { "total": 4,
+ "valid": 4 },
+ "wp:main": { "total": 10,
+ "valid": 10,
+ "rank": 39 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.0.report.json
new file mode 100644
index 00000000000..993d6f80087
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/frame.0.report.json
@@ -0,0 +1,53 @@
+{ "wp:global": { "alt-ergo": { "total": 4, "unknown": 4 },
+ "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 6, "valid": 2, "unknown": 4 } },
+ "wp:functions": { "local": { "local_ensures_KO": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "local_ensures_FRAMED": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 1,
+ "unknown": 1 } } },
+ "global": { "global_ensures_KO": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } } },
+ "localref": { "localref_assert_FRAMED": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "localref_ensures_KO": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 1,
+ "unknown": 1 } } },
+ "alias": { "alias_ensures_KO": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.0.report.json
new file mode 100644
index 00000000000..9a8167e262c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/ground_real.0.report.json
@@ -0,0 +1,12 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 0 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 0 } },
+ "wp:axiomatics": { "": { "lemma_R": { "alt-ergo": { "total": 1, "valid": 1,
+ "rank": 0 },
+ "wp:main": { "total": 1, "valid": 1,
+ "rank": 0 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 0 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 0 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.0.report.json
new file mode 100644
index 00000000000..a0b3ada7192
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/init_valid.0.report.json
@@ -0,0 +1,30 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "unknown": 1 },
+ "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 4, "valid": 3, "unknown": 1 } },
+ "wp:functions": { "validA": { "validA_assert_OK_2": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "validA_assert_OK": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } },
+ "validB": { "validB_assert_KO": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "validB_assert_OK": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 1,
+ "unknown": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.0.report.json
new file mode 100644
index 00000000000..a4b1808ed99
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopcurrent.0.report.json
@@ -0,0 +1,13 @@
+{ "wp:global": { "qed": { "total": 4, "valid": 4 },
+ "wp:main": { "total": 4, "valid": 4 } },
+ "wp:functions": { "f": { "f_loop_invariant_2": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "f_loop_invariant": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 4, "valid": 4 },
+ "wp:main": { "total": 4,
+ "valid": 4 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.0.report.json
new file mode 100644
index 00000000000..a4b1808ed99
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopentry.0.report.json
@@ -0,0 +1,13 @@
+{ "wp:global": { "qed": { "total": 4, "valid": 4 },
+ "wp:main": { "total": 4, "valid": 4 } },
+ "wp:functions": { "f": { "f_loop_invariant_2": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "f_loop_invariant": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 4, "valid": 4 },
+ "wp:main": { "total": 4,
+ "valid": 4 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.0.report.json
new file mode 100644
index 00000000000..371ffd8abf6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/loopextra.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 3, "valid": 3 } },
+ "wp:functions": { "f": { "f_assert_3": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_assert_2": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_assert": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 3,
+ "valid": 3 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.0.report.json
new file mode 100644
index 00000000000..b6fbb01b2b7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/mask.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 2, "valid": 2 } },
+ "wp:functions": { "compute": { "compute_ensures_B": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "compute_ensures_A": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.0.report.json
new file mode 100644
index 00000000000..dbda73ffedd
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overarray.0.report.json
@@ -0,0 +1,51 @@
+{ "wp:global": { "alt-ergo": { "total": 4, "unknown": 4 },
+ "qed": { "total": 8, "valid": 8 },
+ "wp:main": { "total": 12, "valid": 8, "unknown": 4 } },
+ "wp:functions": { "f1_ok": { "f1_ok_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } },
+ "f2_ok": { "f2_ok_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } },
+ "f3_ok": { "f3_ok_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } },
+ "f4_ok": { "f4_ok_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } },
+ "f5_ko": { "f5_ko_assigns": { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } } },
+ "f6_ko": { "f6_ko_assigns": { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.0.report.json
new file mode 100644
index 00000000000..71511e374d5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/overassign.0.report.json
@@ -0,0 +1,61 @@
+{ "wp:global": { "alt-ergo": { "total": 8, "valid": 4, "unknown": 4,
+ "rank": 6 },
+ "qed": { "total": 4, "valid": 4 },
+ "wp:main": { "total": 12, "valid": 8, "unknown": 4,
+ "rank": 6 } },
+ "wp:functions": { "f1_ok": { "f1_ok_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } },
+ "f2_ok": { "f2_ok_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "wp:section": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } },
+ "f3_ok": { "f3_ok_assigns": { "alt-ergo": { "total": 2,
+ "valid": 2,
+ "rank": 6 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 6 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "valid": 2,
+ "rank": 6 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 6 } } },
+ "f4_ok": { "f4_ok_assigns": { "alt-ergo": { "total": 2,
+ "valid": 2,
+ "rank": 5 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 5 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "valid": 2,
+ "rank": 5 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 5 } } },
+ "f5_ko": { "f5_ko_assigns": { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } } },
+ "f6_ko": { "f6_ko_assigns": { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "unknown": 2 },
+ "wp:main": { "total": 2,
+ "unknown": 2 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.0.report.json
new file mode 100644
index 00000000000..3b66b225e19
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/params.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 1 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 1 } },
+ "wp:axiomatics": { "": { "lemma_lem": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.0.report.json
new file mode 100644
index 00000000000..91af25677a2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/plet.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 3 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 3 } },
+ "wp:axiomatics": { "Test": { "lemma_GOAL": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 3 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 3 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.0.report.json
new file mode 100644
index 00000000000..77c7cca1040
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/polarity.0.report.json
@@ -0,0 +1,10 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "unknown": 1 },
+ "wp:main": { "total": 1, "unknown": 1 } },
+ "wp:functions": { "f": { "f_assert": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.0.report.json
new file mode 100644
index 00000000000..96cd0a3fb5d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/repeat.0.report.json
@@ -0,0 +1,122 @@
+{ "wp:global": { "alt-ergo": { "total": 5, "valid": 5, "rank": 12 },
+ "qed": { "total": 42, "valid": 42 },
+ "wp:main": { "total": 47, "valid": 47, "rank": 12 } },
+ "wp:functions": { "master": { "master_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "master_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 3,
+ "valid": 3 },
+ "wp:main": { "total": 3,
+ "valid": 3 } } },
+ "unroll": { "unroll_loop_invariant": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2 } },
+ "unroll_assigns": { "qed": { "total": 22,
+ "valid": 22 },
+ "wp:main": { "total": 22,
+ "valid": 22 } },
+ "unroll_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 25,
+ "valid": 25 },
+ "wp:main": { "total": 25,
+ "valid": 25 } } },
+ "induction": { "induction_loop_invariant_2": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 12 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 12 } },
+ "induction_loop_invariant": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 5 } },
+ "induction_assigns": { "qed": { "total": 3,
+ "valid": 3 },
+ "wp:main":
+ { "total": 3,
+ "valid": 3 } },
+ "induction_loop_assigns": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "induction_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "valid": 2,
+ "rank": 12 },
+ "qed": { "total": 7,
+ "valid": 7 },
+ "wp:main": { "total": 9,
+ "valid": 9,
+ "rank": 12 } } },
+ "shifted": { "shifted_loop_invariant_2": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 12 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 12 } },
+ "shifted_loop_invariant": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 5 } },
+ "shifted_assigns": { "qed": { "total": 4,
+ "valid": 4 },
+ "wp:main": { "total": 4,
+ "valid": 4 } },
+ "shifted_loop_assigns": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "shifted_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 11 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 11 } },
+ "wp:section": { "alt-ergo": { "total": 3,
+ "valid": 3,
+ "rank": 12 },
+ "qed": { "total": 7,
+ "valid": 7 },
+ "wp:main": { "total": 10,
+ "valid": 10,
+ "rank": 12 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.0.report.json
new file mode 100644
index 00000000000..910cff1aa78
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/string_c.0.report.json
@@ -0,0 +1,193 @@
+{ "wp:global": { "alt-ergo": { "total": 21, "valid": 21, "rank": 81 },
+ "qed": { "total": 23, "valid": 23 },
+ "wp:main": { "total": 44, "valid": 44, "rank": 81 } },
+ "wp:functions": { "memcpy": { "memcpy_loop_invariant_no_eva_2": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 62 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 62 } },
+ "memcpy_loop_invariant_no_eva": { "alt-ergo":
+ { "total": 2,
+ "valid": 2,
+ "rank": 16 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 16 } },
+ "memcpy_loop_variant": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 16 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 16 } },
+ "memcpy_assigns": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "memcpy_loop_assigns": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 40 },
+ "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 3,
+ "valid": 3,
+ "rank": 40 } },
+ "memcpy_ensures_result_ptr": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "memcpy_ensures_copied_contents": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 48 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 48 } },
+ "wp:section": { "alt-ergo": { "total": 6,
+ "valid": 6,
+ "rank": 62 },
+ "qed": { "total": 6,
+ "valid": 6 },
+ "wp:main": { "total": 12,
+ "valid": 12,
+ "rank": 62 } } },
+ "memmove": { "memmove_loop_invariant_no_eva_6": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 54 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 54 } },
+ "memmove_loop_invariant_no_eva_5": { "alt-ergo":
+ { "total": 2,
+ "valid": 2,
+ "rank": 39 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 39 } },
+ "memmove_loop_invariant_no_eva_4": { "alt-ergo":
+ { "total": 2,
+ "valid": 2,
+ "rank": 18 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 18 } },
+ "memmove_loop_invariant_no_eva_3": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 81 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 81 } },
+ "memmove_loop_invariant_no_eva_2": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 38 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 38 } },
+ "memmove_loop_invariant_no_eva": { "alt-ergo":
+ { "total": 2,
+ "valid": 2,
+ "rank": 18 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 18 } },
+ "memmove_loop_variant_2": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 18 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 18 } },
+ "memmove_loop_variant": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 18 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 18 } },
+ "memmove_assigns": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "qed": { "total": 7,
+ "valid": 7 },
+ "wp:main": { "total": 8,
+ "valid": 8,
+ "rank": 6 } },
+ "memmove_loop_assigns_2": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 48 },
+ "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main":
+ { "total": 3,
+ "valid": 3,
+ "rank": 48 } },
+ "memmove_loop_assigns": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 57 },
+ "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main":
+ { "total": 3,
+ "valid": 3,
+ "rank": 57 } },
+ "memmove_ensures_result_ptr": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "memmove_ensures_copied_contents": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 63 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 63 } },
+ "wp:section": { "alt-ergo": { "total": 15,
+ "valid": 15,
+ "rank": 81 },
+ "qed": { "total": 17,
+ "valid": 17 },
+ "wp:main": { "total": 32,
+ "valid": 32,
+ "rank": 81 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.0.report.json
new file mode 100644
index 00000000000..72d2a74fbb8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 24 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 24 } },
+ "wp:functions": { "mem": { "mem_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 24 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 24 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 24 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 24 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.0.report.json
new file mode 100644
index 00000000000..1902a622817
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/subset_fopen.0.report.json
@@ -0,0 +1,36 @@
+{ "wp:global": { "alt-ergo": { "total": 2, "valid": 1, "unknown": 1,
+ "rank": 20 },
+ "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 5, "valid": 4, "unknown": 1,
+ "rank": 20 } },
+ "wp:functions": { "f": { "f_assert_Ok_E": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 20 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 20 } },
+ "f_assert_Ok_D": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_assert_Ok_C": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_assert_Ok_B": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_assert_Ok_A": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "valid": 1,
+ "unknown": 1,
+ "rank": 20 },
+ "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 5,
+ "valid": 4,
+ "unknown": 1,
+ "rank": 20 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.0.report.json
new file mode 100644
index 00000000000..b967bd53ad6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsafe-arrays.0.report.json
@@ -0,0 +1,24 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 5 },
+ "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 3, "valid": 3, "rank": 5 } },
+ "wp:functions": { "f": { "f_ensures_INDIRP": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 5 } },
+ "f_ensures_STRUCT": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_ensures_ARRAYS": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 3,
+ "valid": 3,
+ "rank": 5 } } } } }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.0.report.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.0.report.json
new file mode 100644
index 00000000000..8d566a55f49
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsupported_init.0.report.json
@@ -0,0 +1,16 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "unknown": 1 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2, "valid": 1, "unknown": 1 } },
+ "wp:functions": { "f": { "cp_requires_r1": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "f_assert_a1": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 1,
+ "unknown": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/array.0.report.json b/src/plugins/wp/tests/wp_store/oracle_qualif/array.0.report.json
new file mode 100644
index 00000000000..c86162e95a5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/array.0.report.json
@@ -0,0 +1,16 @@
+{ "wp:global": { "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 2, "valid": 2 } },
+ "wp:functions": { "g": { "g_ensures_P_addr_shift_qed_ok": { "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "g_ensures_P_startof_qed_ok": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } } } }
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/natural.0.report.json b/src/plugins/wp/tests/wp_store/oracle_qualif/natural.0.report.json
new file mode 100644
index 00000000000..c8fc7843294
--- /dev/null
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/natural.0.report.json
@@ -0,0 +1,12 @@
+{ "wp:global": { "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 3, "valid": 3 } },
+ "wp:functions": { "f": { "f_assigns": { "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "f_ensures_qed_ok": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 3,
+ "valid": 3 } } } } }
diff --git a/src/plugins/wp/tests/wp_store/oracle_qualif/struct.0.report.json b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.0.report.json
new file mode 100644
index 00000000000..aa80bc9b418
--- /dev/null
+++ b/src/plugins/wp/tests/wp_store/oracle_qualif/struct.0.report.json
@@ -0,0 +1,49 @@
+{ "wp:global": { "alt-ergo": { "total": 3, "valid": 3, "rank": 10 },
+ "qed": { "total": 3, "valid": 3 },
+ "wp:main": { "total": 6, "valid": 6, "rank": 10 } },
+ "wp:functions": { "g": { "g_assigns": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "g_ensures": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } },
+ "f": { "g_requires": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 5 } },
+ "f_assert_qed_ok": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 5 } } },
+ "main": { "main_ensures_Q_qed_ok": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 10 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 10 } },
+ "main_ensures_P_qed_ok": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 10 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 10 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "valid": 2,
+ "rank": 10 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 10 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.0.report.json
new file mode 100644
index 00000000000..4497f6d5e8d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.0.report.json
@@ -0,0 +1,8 @@
+{ "wp:global": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1, "valid": 1 } },
+ "wp:functions": { "g": { "f_requires": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.0.report.json
new file mode 100644
index 00000000000..57fb10b1504
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/shift_lemma.0.report.json
@@ -0,0 +1,33 @@
+{ "wp:global": { "alt-ergo": { "total": 3, "valid": 3, "rank": 6 },
+ "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 5, "valid": 5, "rank": 6 } },
+ "wp:functions": { "f": { "f_assert_5": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 3 } },
+ "f_assert_4": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_assert_3": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_assert_2": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 6 } },
+ "f_assert": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "wp:main": { "total": 1, "valid": 1,
+ "rank": 4 } },
+ "wp:section": { "alt-ergo": { "total": 3,
+ "valid": 3,
+ "rank": 6 },
+ "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 5,
+ "valid": 5,
+ "rank": 6 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.0.report.json
new file mode 100644
index 00000000000..dccb3ae9170
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/struct_array_type.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 4 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 4 } },
+ "wp:functions": { "f": { "f_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 4 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 4 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.0.report.json
new file mode 100644
index 00000000000..a01a9ebd006
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 1 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 1 } },
+ "wp:functions": { "job": { "job_assert": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.0.report.json
new file mode 100644
index 00000000000..82596921df3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cast.0.report.json
@@ -0,0 +1,14 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 5 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 5 } },
+ "wp:functions": { "f": { "f_assert_OUT": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 5 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 5 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.0.report.json
new file mode 100644
index 00000000000..f7399a08a68
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_cst.0.report.json
@@ -0,0 +1,11 @@
+{ "wp:global": { "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 2, "valid": 2 } },
+ "wp:functions": { "f": { "f_ensures_B": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "f_ensures_A": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.0.report.json
new file mode 100644
index 00000000000..94fcb00c3cb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_hard.0.report.json
@@ -0,0 +1,26 @@
+{ "wp:global": { "alt-ergo": { "total": 1, "unknown": 1 },
+ "qed": { "total": 2, "valid": 2 },
+ "wp:main": { "total": 3, "valid": 2, "unknown": 1 } },
+ "wp:functions": { "main": { "main_requires_r_is_q1_ko": { "alt-ergo":
+ { "total": 1,
+ "unknown": 1 },
+ "wp:main":
+ { "total": 1,
+ "unknown": 1 } },
+ "main_requires_q_is_66F0": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "main_requires_p_is_33FF": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 3,
+ "valid": 2,
+ "unknown": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.0.report.json
new file mode 100644
index 00000000000..015bc871fc4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_ite.0.report.json
@@ -0,0 +1,10 @@
+{ "wp:global": { "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 1, "valid": 1 } },
+ "wp:functions": { "check": { "check_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.0.report.json
new file mode 100644
index 00000000000..0c477e292bc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_labels.0.report.json
@@ -0,0 +1,26 @@
+{ "wp:global": { "alt-ergo": { "total": 3, "valid": 3, "rank": 6 },
+ "wp:main": { "total": 3, "valid": 3, "rank": 6 } },
+ "wp:functions": { "duplet": { "duplet_assert_PJ": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 6 } },
+ "duplet_assert_PI": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 6 } },
+ "duplet_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 6 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 6 } },
+ "wp:section": { "alt-ergo": { "total": 3,
+ "valid": 3,
+ "rank": 6 },
+ "wp:main": { "total": 3,
+ "valid": 3,
+ "rank": 6 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.0.report.json
new file mode 100644
index 00000000000..468e2635821
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_matrix.0.report.json
@@ -0,0 +1,29 @@
+{ "wp:global": { "alt-ergo": { "total": 2, "valid": 1, "unknown": 1,
+ "rank": 3 },
+ "qed": { "total": 1, "valid": 1 },
+ "wp:main": { "total": 3, "valid": 2, "unknown": 1,
+ "rank": 3 } },
+ "wp:functions": { "make": { "make_ensures_KO": { "alt-ergo": { "total": 1,
+ "unknown": 1 },
+ "wp:main": { "total": 1,
+ "unknown": 1 } },
+ "make_ensures_OK2": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "make_ensures_OK1": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 3 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 3 } },
+ "wp:section": { "alt-ergo": { "total": 2,
+ "valid": 1,
+ "unknown": 1,
+ "rank": 3 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 3,
+ "valid": 2,
+ "unknown": 1,
+ "rank": 3 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.0.report.json
new file mode 100644
index 00000000000..c9e63bb2e44
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_collect.0.report.json
@@ -0,0 +1,181 @@
+{ "wp:global": { "alt-ergo": { "total": 15, "valid": 15, "rank": 13 },
+ "qed": { "total": 17, "valid": 17 },
+ "wp:main": { "total": 32, "valid": 32, "rank": 13 } },
+ "wp:functions": { "job": { "job_assigns": { "qed": { "total": 3,
+ "valid": 3 },
+ "wp:main": { "total": 3,
+ "valid": 3 } },
+ "job_ensures_P": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "job_ensures_K": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 5,
+ "valid": 5 },
+ "wp:main": { "total": 5,
+ "valid": 5 } } },
+ "job2": { "job2_assigns": { "qed": { "total": 3,
+ "valid": 3 },
+ "wp:main": { "total": 3,
+ "valid": 3 } },
+ "job2_ensures_Q": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "job2_ensures_K": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "qed": { "total": 5,
+ "valid": 5 },
+ "wp:main": { "total": 5,
+ "valid": 5 } } },
+ "job3": { "job3_assigns": { "qed": { "total": 3,
+ "valid": 3 },
+ "wp:main": { "total": 3,
+ "valid": 3 } },
+ "job3_ensures_Q": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 5 } },
+ "job3_ensures_K": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "qed": { "total": 4,
+ "valid": 4 },
+ "wp:main": { "total": 5,
+ "valid": 5,
+ "rank": 5 } } },
+ "caller": { "job_requires_2": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 4 } },
+ "job_requires": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 2 } },
+ "caller_ensures_P2": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 9 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 9 } },
+ "caller_ensures_P1": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 9 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 9 } },
+ "caller_ensures_K": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 4,
+ "valid": 4,
+ "rank": 9 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 5,
+ "valid": 5,
+ "rank": 9 } } },
+ "caller2": { "job2_requires_2": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 4 } },
+ "job2_requires": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 2 } },
+ "caller2_ensures_R": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 13 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 13 } },
+ "caller2_ensures_Q2": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 13 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 13 } },
+ "caller2_ensures_Q1": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 13 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 13 } },
+ "caller2_ensures_K": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 5,
+ "valid": 5,
+ "rank": 13 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 6,
+ "valid": 6,
+ "rank": 13 } } },
+ "caller3": { "job3_requires_2": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 4 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 4 } },
+ "job3_requires": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 2 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 2 } },
+ "caller3_ensures_R": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 13 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 13 } },
+ "caller3_ensures_Q2": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 13 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 13 } },
+ "caller3_ensures_Q1": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 13 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 13 } },
+ "caller3_ensures_K": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 5,
+ "valid": 5,
+ "rank": 13 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 6,
+ "valid": 6,
+ "rank": 13 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.report.json
new file mode 100644
index 00000000000..ab542867843
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.report.json
@@ -0,0 +1,50 @@
+{ "wp:global": { "alt-ergo": { "total": 4, "valid": 4, "rank": 19 },
+ "qed": { "total": 4, "valid": 4 },
+ "wp:main": { "total": 8, "valid": 8, "rank": 19 } },
+ "wp:functions": { "init": { "init_loop_invariant_Partial": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 9 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 9 } },
+ "init_loop_invariant_Range": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 5 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 5 } },
+ "init_assigns": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "init_loop_assigns": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 19 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 19 } },
+ "init_ensures": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 7 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 7 } },
+ "wp:section": { "alt-ergo": { "total": 4,
+ "valid": 4,
+ "rank": 19 },
+ "qed": { "total": 4,
+ "valid": 4 },
+ "wp:main": { "total": 8,
+ "valid": 8,
+ "rank": 19 } } } } }
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.0.report.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.0.report.json
new file mode 100644
index 00000000000..98742804d93
--- /dev/null
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_string.0.report.json
@@ -0,0 +1,63 @@
+{ "wp:global": { "alt-ergo": { "total": 5, "valid": 5, "rank": 34 },
+ "qed": { "total": 8, "valid": 8 },
+ "wp:main": { "total": 13, "valid": 13, "rank": 34 } },
+ "wp:functions": { "strlen": { "strlen_assert_END": { "alt-ergo": { "total": 1,
+ "valid": 1,
+ "rank": 19 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 19 } },
+ "strlen_loop_invariant_ZERO": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 11 },
+ "qed":
+ { "total": 1,
+ "valid": 1 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 11 } },
+ "strlen_loop_invariant_RANGE": { "alt-ergo":
+ { "total": 2,
+ "valid": 2,
+ "rank": 34 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2,
+ "rank": 34 } },
+ "strlen_loop_invariant_BASE": { "qed":
+ { "total": 2,
+ "valid": 2 },
+ "wp:main":
+ { "total": 2,
+ "valid": 2 } },
+ "strlen_loop_variant": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 14 },
+ "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 2,
+ "valid": 2,
+ "rank": 14 } },
+ "strlen_assigns": { "qed": { "total": 2,
+ "valid": 2 },
+ "wp:main": { "total": 2,
+ "valid": 2 } },
+ "strlen_loop_assigns": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "strlen_ensures": { "qed": { "total": 1,
+ "valid": 1 },
+ "wp:main": { "total": 1,
+ "valid": 1 } },
+ "wp:section": { "alt-ergo": { "total": 5,
+ "valid": 5,
+ "rank": 34 },
+ "qed": { "total": 8,
+ "valid": 8 },
+ "wp:main": { "total": 13,
+ "valid": 13,
+ "rank": 34 } } } } }
--
GitLab