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 0000000000000000000000000000000000000000..17a701f571cf6dbe5cfed605ec9b9613c7b168d2
--- /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 0000000000000000000000000000000000000000..23c6014c8c98bb6ceee65521782a49f50bd479a8
--- /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 0000000000000000000000000000000000000000..37b6284cd8341bc20f787cf249590fd876b80e33
--- /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 0000000000000000000000000000000000000000..c9b4abc0b34fba30c01071e1f47fe4f2e8c8ce92
--- /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 0000000000000000000000000000000000000000..a3e18b8a1f10b2629a4c2dcfc0d7d34e0c338e01
--- /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 0000000000000000000000000000000000000000..80f3747514082652f99e49c34a3b92ac8f7c16f2
--- /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 0000000000000000000000000000000000000000..891942e3737f988096e849f341cc263e7f0e383f
--- /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 0000000000000000000000000000000000000000..5c43681476a52c2a6ea5ee88fdcf36fbe3395998
--- /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 0000000000000000000000000000000000000000..8ab9ce87bfcce6699c3d4d058f75fa169519f276
--- /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 0000000000000000000000000000000000000000..ed396bf7e2986b4e9eee657b6c51541ae3c34d3d
--- /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 0000000000000000000000000000000000000000..3d33c8c50aa7c8d908c3718f8ff99be5e4a3bac1
--- /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 0000000000000000000000000000000000000000..4ed4a7c4e6305b0311d13850278f63d06912e2c8
--- /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 0000000000000000000000000000000000000000..badcee8deb06c806b1e1fba397198f03ad075183
--- /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 0000000000000000000000000000000000000000..79fbcb44621bbe66323dc1c13c9b7b044015f84a
--- /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 0000000000000000000000000000000000000000..bd9ed2f82998f182289b0babad662f514f75e1cb
--- /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 0000000000000000000000000000000000000000..6c8cdc3f855be7fa51140fe38517e7171e44eb05
--- /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 0000000000000000000000000000000000000000..cce14a76fc5d3c4f15f0d5cc158f65973abdc826
--- /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 0000000000000000000000000000000000000000..0719103e8bc1d5263f550516f702cf3c0b923272
--- /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 0000000000000000000000000000000000000000..c8f7254db678407b637fbbd5630ad7138b8d784f
--- /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 0000000000000000000000000000000000000000..20f18a7e95a515ebdf59eef3ef5be2c0db1a115a
--- /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 0000000000000000000000000000000000000000..406e1c61d89ad35e2df5c92b839eec586460153d
--- /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 0000000000000000000000000000000000000000..576a872d9dac3477f1c9f345a8c56e3e1dc28634
--- /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 0000000000000000000000000000000000000000..d88f27e56ce60eaa0fc2d103da5b57f681cf1fef
--- /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 0000000000000000000000000000000000000000..414c3cf94d8eb41a5b1a4767cdfbacd5c6e2fc60
--- /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 0000000000000000000000000000000000000000..cd95b6d3b7037691df3e75897d0bde9976d48581
--- /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 0000000000000000000000000000000000000000..8add84a6b5d7f48c762f4162d0a1f437623fe410
--- /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 0000000000000000000000000000000000000000..f93f10055789723c4cd79cb694034af2fd44c014
--- /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 0000000000000000000000000000000000000000..6deccb7f511907d2da384a9fb2bb7691f959eb63
--- /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 0000000000000000000000000000000000000000..d2c13e606a02ea298d5cecf7a69d686f94725326
--- /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 0000000000000000000000000000000000000000..3c5b3035ee9db86d27daf0fc87aac84d1e2b9a7a
--- /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 0000000000000000000000000000000000000000..f12a169da4eebf3f8cc384e0249786c3c213bd82
--- /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 0000000000000000000000000000000000000000..e77f053555a9f51db8cc48a9b7e86d70610299a5
--- /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 0000000000000000000000000000000000000000..993d6f800871b136aa491a8594e86226bb0f56c8
--- /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 0000000000000000000000000000000000000000..9a8167e262cb87df9f383456020522e3da05829b
--- /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 0000000000000000000000000000000000000000..a0b3ada7192541ab9bf0e9b1b2d8f0638c6c4d66
--- /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 0000000000000000000000000000000000000000..a4b1808ed9992cba37a7296ea0dc3c6e31d556e3
--- /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 0000000000000000000000000000000000000000..a4b1808ed9992cba37a7296ea0dc3c6e31d556e3
--- /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 0000000000000000000000000000000000000000..371ffd8abf6614efa173e397dd7d1a3b238adec5
--- /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 0000000000000000000000000000000000000000..b6fbb01b2b7c160c1fa6a3c1e53cb7c5cbb51084
--- /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 0000000000000000000000000000000000000000..dbda73ffeddfd55206f94a3f1e8d23e4b278c486
--- /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 0000000000000000000000000000000000000000..71511e374d5cd66fb7c663cd5ed201c7ef5af01b
--- /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 0000000000000000000000000000000000000000..3b66b225e199599ed38e049346fd6313fe305abf
--- /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 0000000000000000000000000000000000000000..91af25677a2d0e6d4b4bb2afabbf859e7872fa25
--- /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 0000000000000000000000000000000000000000..77c7cca104076f8c762244872f1d7dbbc56b96e0
--- /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 0000000000000000000000000000000000000000..96cd0a3fb5d51f6122e4a4ffb1e9568d7d1e7ede
--- /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 0000000000000000000000000000000000000000..910cff1aa784f7f216414880ab65cc8d0e445a24
--- /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 0000000000000000000000000000000000000000..72d2a74fbb82e4fc45b67ca97ac5f1db82478a1b
--- /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 0000000000000000000000000000000000000000..1902a622817eb3a2f2bdbfca9fb9a8b2af0e803f
--- /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 0000000000000000000000000000000000000000..b967bd53ad6fbf82e01cbb737f76c074cf36dbfa
--- /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 0000000000000000000000000000000000000000..8d566a55f49681c4d13c773501c3210ad075c9e9
--- /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 0000000000000000000000000000000000000000..c86162e95a5989e56b6aef1c30cc7356377e1d0f
--- /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 0000000000000000000000000000000000000000..c8fc7843294bb16b26a3bd0c4c054cd60a220604
--- /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 0000000000000000000000000000000000000000..aa80bc9b41856925c58a85de4760691e5d42d51c
--- /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 0000000000000000000000000000000000000000..4497f6d5e8d209a556521cb6c092103e5968ccc9
--- /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 0000000000000000000000000000000000000000..57fb10b150427ac2a1e2193406b66f389eef9364
--- /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 0000000000000000000000000000000000000000..dccb3ae91700c6d94a3efb6356fd8391b552ef2a
--- /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 0000000000000000000000000000000000000000..a01a9ebd0062ff5aa4bea699da100f9b157bc0d7
--- /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 0000000000000000000000000000000000000000..82596921df3cab5fe74c13950bd75a29c96526ed
--- /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 0000000000000000000000000000000000000000..f7399a08a68535d5112bcf985aa8a7a4d07d590c
--- /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 0000000000000000000000000000000000000000..94fcb00c3cbadaa18a5c6cefcd550c33b094e592
--- /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 0000000000000000000000000000000000000000..015bc871fc4ca3961f0f6378b2f719cd527944b2
--- /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 0000000000000000000000000000000000000000..0c477e292bcb88d7a05f12953775444074bdf5d1
--- /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 0000000000000000000000000000000000000000..468e2635821f7ad20427d9ad8e769224e74815b2
--- /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 0000000000000000000000000000000000000000..c9e63bb2e44fadbd3a8a0d8b596c7aea85211d4b
--- /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 0000000000000000000000000000000000000000..ab542867843fc6404fdda10d57a55a10cec8af43
--- /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 0000000000000000000000000000000000000000..98742804d934e2b76dec4f7b5645fe4e23160666
--- /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 } } } } }