From 7963a687e807d395e4e3db49710ef2bf64525d2d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 13 Jan 2022 09:55:21 +0100
Subject: [PATCH] [wp] Update tests oracle wrt RTE warning
---
.../wp/tests/wp/oracle_qualif/wp_strategy.res.oracle | 4 ++--
.../wp_acsl/oracle_qualif/chunk_typing.res.oracle | 2 +-
.../oracle_qualif/chunk_typing_usable.res.oracle | 4 ++--
.../wp_acsl/oracle_qualif/gnu_zero_array.res.oracle | 2 +-
.../wp_acsl/oracle_qualif/opaque_struct.res.oracle | 12 ++++++------
.../wp/tests/wp_bts/oracle_qualif/bts779.res.oracle | 2 +-
.../tests/wp_bts/oracle_qualif/bts_1360.res.oracle | 4 ++--
...binary-multiplication-without-overflow.res.oracle | 2 +-
.../oracle_qualif/binary-multiplication.res.oracle | 2 +-
.../wp_gallery/oracle_qualif/bsearch.res.oracle | 2 +-
.../tests/wp_gallery/oracle_qualif/euclid.res.oracle | 2 +-
.../tests/wp_gallery/oracle_qualif/find.res.oracle | 6 +++---
.../oracle_qualif/frama_c_exo1_solved.res.oracle | 2 +-
.../oracle_qualif/frama_c_exo2_solved.res.oracle | 2 +-
.../oracle_qualif/frama_c_exo3_solved.old.res.oracle | 2 +-
.../frama_c_exo3_solved.old.v2.res.oracle | 2 +-
.../frama_c_exo3_solved.simplified.res.oracle | 2 +-
.../oracle_qualif/string-compare.res.oracle | 6 +++---
.../wp_manual/oracle_qualif/manual.1.res.oracle | 2 +-
.../wp_manual/oracle_qualif/manual.2.res.oracle | 2 +-
.../wp/tests/wp_plugin/oracle_qualif/rte.res.oracle | 6 +++---
21 files changed, 35 insertions(+), 35 deletions(-)
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
index dfb0a7c8139..da93d6b571b 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing wp_strategy.c (with preprocessing)
-[rte] annotating function bts0513
-[rte] annotating function bts0513_bis
+[rte:annot] annotating function bts0513
+[rte:annot] annotating function bts0513_bis
[wp] Running WP plugin...
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko1 : Unsuccess
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
index 768556112b1..98bcd996410 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing chunk_typing.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function function
+[rte:annot] annotating function function
[wp] 39 goals scheduled
[wp] [Alt-Ergo] Goal typed_function_ensures : Valid
[wp] [Alt-Ergo] Goal typed_function_loop_invariant_preserved : Valid
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
index d076d76ed0c..2c656c6f825 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/chunk_typing_usable.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing chunk_typing_usable.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function usable_axiom
-[rte] annotating function usable_lemma
+[rte:annot] annotating function usable_axiom
+[rte:annot] annotating function usable_lemma
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 3 goals scheduled
[wp] [Coq] Goal typed_lemma_provable_lemma : Saved script
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/gnu_zero_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/gnu_zero_array.res.oracle
index 26cfc3ad345..2ac1dd590cf 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/gnu_zero_array.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/gnu_zero_array.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing gnu_zero_array.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[wp] Running WP plugin...
[wp] gnu_zero_array.i:14: Warning:
Cast with incompatible pointers types (source: sint8*) (target: S*)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
index 2e8a5bd7c03..7ce463d9349 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
@@ -1,12 +1,12 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing opaque_struct.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function assigned_via_pointer
-[rte] annotating function assigns
-[rte] annotating function assigns_effect
-[rte] annotating function chunk_typing
-[rte] annotating function initialized_assigns
-[rte] annotating function uninitialized_assigns
+[rte:annot] annotating function assigned_via_pointer
+[rte:annot] annotating function assigns
+[rte:annot] annotating function assigns_effect
+[rte:annot] annotating function chunk_typing
+[rte:annot] annotating function initialized_assigns
+[rte:annot] annotating function uninitialized_assigns
[kernel:annot:missing-spec] opaque_struct.i:79: Warning:
Neither code nor specification for function use, generating default assigns from the prototype
[wp] 15 goals scheduled
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
index dbb98c6df14..ca40bafd86e 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts779.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing bts779.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function f
+[rte:annot] annotating function f
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_assert : Valid
[wp] [Alt-Ergo] Goal typed_f_assert_rte_mem_access : Unsuccess
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
index 5072e7c6182..92f813ec7b9 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/bts_1360.res.oracle
@@ -1,8 +1,8 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing bts_1360.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function foo_correct
-[rte] annotating function foo_wrong
+[rte:annot] annotating function foo_correct
+[rte:annot] annotating function foo_wrong
[wp] 10 goals scheduled
[wp] [Qed] Goal typed_foo_wrong_ensures : Valid
[wp] [Qed] Goal typed_foo_wrong_assert_rte_mem_access : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
index 8b3b8ce8f5b..fda9d1592fc 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte -wp-timeout 20 -warn-unsigned-overflow [...]
[kernel] Parsing binary-multiplication-without-overflow.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function BinaryMultiplication
+[rte:annot] annotating function BinaryMultiplication
[wp] 16 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_half : Valid
[wp] [Qed] Goal typed_lemma_size : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
index 374c185811e..c1ba4163554 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing binary-multiplication.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function BinaryMultiplication
+[rte:annot] annotating function BinaryMultiplication
[wp] 17 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ax4_ok : Valid
[wp] [Alt-Ergo] Goal typed_lemma_ax5_ok : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
index f3c3ceeb9d3..b6e73bdde32 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/bsearch.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing bsearch.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function binary_search
+[rte:annot] annotating function binary_search
[wp] 28 goals scheduled
[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_default_requires
[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_dead_loop_s3
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
index da9813c2fb9..d3aaf8ea83f 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing euclid.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function euclid_gcd
+[rte:annot] annotating function euclid_gcd
[wp] 16 goals scheduled
[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_default_requires
[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
index 0760f8c1ed9..6fc4641c2a9 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
@@ -54,9 +54,9 @@
iter_ptr 2 6 8 100%
------------------------------------------------------------
[wp] Running WP plugin...
-[rte] annotating function find
-[rte] annotating function find_ptr
-[rte] annotating function iter_ptr
+[rte:annot] annotating function find
+[rte:annot] annotating function find_ptr
+[rte:annot] annotating function iter_ptr
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_find_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed_find_assert_rte_signed_overflow : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
index 4b982f51859..472bae3aac8 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo1_solved.res.oracle
@@ -21,7 +21,7 @@
exo1 6 4 10 100%
------------------------------------------------------------
[wp] Running WP plugin...
-[rte] annotating function exo1
+[rte:annot] annotating function exo1
[wp] 5 goals scheduled
[wp] [Alt-Ergo] Goal typed_exo1_assert_rte_signed_overflow : Valid
[wp] [Alt-Ergo] Goal typed_exo1_assert_rte_mem_access : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
index 83f9d8a5be5..9fb70982525 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo2_solved.res.oracle
@@ -33,7 +33,7 @@
max_subarray 12 10 22 100%
------------------------------------------------------------
[wp] Running WP plugin...
-[rte] annotating function max_subarray
+[rte:annot] annotating function max_subarray
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_max_subarray_assert_rte_mem_access : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
index 46675ba6fcb..dfc94d8a394 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.res.oracle
@@ -54,7 +54,7 @@
*/
void equal_elements(int *a, int *v1, int *v2);
[wp] Running WP plugin...
-[rte] annotating function equal_elements
+[rte:annot] annotating function equal_elements
[wp] 16 goals scheduled
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access_2 : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
index 8dfaabe1c38..4bf9ab318fb 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.old.v2.res.oracle
@@ -55,7 +55,7 @@
*/
void equal_elements(int *a, int *v1, int *v2);
[wp] Running WP plugin...
-[rte] annotating function equal_elements
+[rte:annot] annotating function equal_elements
[wp] 16 goals scheduled
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_ref_equal_elements_assert_rte_mem_access_2 : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
index e2cf934a567..9ca1fbbad3e 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/frama_c_exo3_solved.simplified.res.oracle
@@ -37,7 +37,7 @@
pair 16 10 26 100%
------------------------------------------------------------
[wp] Running WP plugin...
-[rte] annotating function pair
+[rte:annot] annotating function pair
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_pair_assert_rte_index_bound : Valid
[wp] [Qed] Goal typed_pair_assert_rte_index_bound_2 : Valid
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
index 8ec3a7f69f5..d6ad1f485b3 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
@@ -67,9 +67,9 @@
main 5 2 7 100%
------------------------------------------------------------
[wp] Running WP plugin...
-[rte] annotating function main
-[rte] annotating function stringCompare
-[rte] annotating function stringLength
+[rte:annot] annotating function main
+[rte:annot] annotating function stringCompare
+[rte:annot] annotating function stringLength
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_stringCompare_assert_rte_mem_access : Valid
[wp] [Alt-Ergo] Goal typed_stringCompare_assert_rte_mem_access_2 : Valid
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle
index fb13236dbf6..b34ba7805c8 100644
--- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.1.res.oracle
@@ -3,7 +3,7 @@
[kernel] Parsing working_dir/swap.c (with preprocessing)
[kernel] Parsing working_dir/swap2.h (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function swap
+[rte:annot] annotating function swap
[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_swap_ensures_A : Valid
[wp] [Qed] Goal typed_swap_ensures_B : Valid
diff --git a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle
index 15ac0f70d86..f22342a0883 100644
--- a/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle
+++ b/src/plugins/wp/tests/wp_manual/oracle_qualif/manual.2.res.oracle
@@ -1,5 +1,5 @@
# frama-c -wp -wp-rte [...]
-[rte] annotating function swap
+[rte:annot] annotating function swap
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
swap 5 3 8 100%
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
index 4378c5286a8..f002fd6fea3 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/rte.res.oracle
@@ -1,9 +1,9 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing rte.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function job
-[rte] annotating function job2
-[rte] annotating function job3
+[rte:annot] annotating function job
+[rte:annot] annotating function job2
+[rte:annot] annotating function job3
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access : Unsuccess
[wp] [Alt-Ergo] Goal typed_job_assert_rte_mem_access_2 : Unsuccess
--
GitLab