diff --git a/src/plugins/rte/options.ml b/src/plugins/rte/options.ml
index 2e5b4d55f5bcf4ebc6b571d5a95459e2ac1ba08c..ccd4cfe0d3faee3a75ae11619f8865f2a9eaf188 100644
--- a/src/plugins/rte/options.ml
+++ b/src/plugins/rte/options.ml
@@ -125,7 +125,8 @@ module FunctionSelection =
let help = "select <fun> for analysis (default all functions)"
end)
-let warn ?source fmt = warning ?source ~current:true ~once:true fmt
+let dkey_annot = register_category "annot"
+let () = add_debug_keys dkey_annot
(*
Local Variables:
diff --git a/src/plugins/rte/options.mli b/src/plugins/rte/options.mli
index d2d78c6e139f56faf130d6bc25c0ebfb93421905..462eda7583574d75ef959ff0219ba97f2bb6e06e 100644
--- a/src/plugins/rte/options.mli
+++ b/src/plugins/rte/options.mli
@@ -35,7 +35,7 @@ module Trivial : Parameter_sig.Bool
module Warn : Parameter_sig.Bool
module FunctionSelection: Parameter_sig.Kernel_function_set
-val warn: ?source:Filepath.position -> ('a, Format.formatter, unit) format -> 'a
+val dkey_annot: category
(*
Local Variables:
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index 75b8dba172cb181233de116ec621dbbb86fb436c..4b7e902243355f0e452b7eff9bde9af57d8bc3aa 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -150,9 +150,11 @@ let _ignore =
let main () =
(* reset "rte generated" properties for all functions *)
if Options.Enabled.get () then begin
- Options.feedback ~level:2 "generating annotations";
+ Options.feedback ~dkey:Options.dkey_annot ~level:2
+ "generating annotations";
!Db.RteGen.compute ();
- Options.feedback ~level:2 "annotations computed"
+ Options.feedback ~dkey:Options.dkey_annot ~level:2
+ "annotations computed"
end
let () = Db.Main.extend main
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index 1e027d5d5f170a4c2463d74a83296d85c2cab93d..d583bf9af52bd54a07d5a7bcf4e423b2dde5dfec 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -305,7 +305,8 @@ let shift_overflow_assertion ~signed ~remove_trivial ~on_alarm (exp, op, lexp, r
let size = Cil.bitsSizeOf t in
if size <> Cil.bitsSizeOf (Cil.typeOf lexp) then
(* size of result type should be size of left (promoted) operand *)
- Options.warn "problem with bitsSize of %a: not treated" Printer.pp_exp exp;
+ Options.warning ~current:true ~once:true
+ "problem with bitsSize of %a: not treated" Printer.pp_exp exp;
if op = Shiftlt then
(* compute greatest representable "size bits" (signed) integer *)
let maxValResult =
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index d7778383f58cd0e596b43f7e09d75669a43adb54..1f754dca975a8b6b243c72b451eca58d24a3f963 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -471,12 +471,13 @@ let annotate ?flags kf =
comp Finite_float.accessor flags.finite_float |||
comp Bool_value.accessor flags.bool_value
then begin
- Options.feedback "annotating function %a" Kernel_function.pretty kf;
+ Options.feedback ~dkey:Options.dkey_annot
+ "annotating function %a" Kernel_function.pretty kf;
let warn = Options.Warn.get () in
let on_alarm stmt ~invalid alarm =
let ca, _ = register Generator.emitter kf stmt ~invalid alarm in
if warn && invalid then
- Options.warn "@[guaranteed RTE:@ %a@]"
+ Options.warning ~current:true ~once:true "@[guaranteed RTE:@ %a@]"
Printer.pp_code_annotation ca
in
let vis = new annot_visitor kf flags on_alarm in
diff --git a/src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle b/src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle
index 0de7045f16641d2abf817964791b1e6fa77ad86f..6c94a863a2d3e504a4339ae40a2af5a7d960eddb 100644
--- a/src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/bug_rte.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing bug_rte.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function bug
+[rte:annot] annotating function bug
------------------------------------------------------------
Function bug
------------------------------------------------------------
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 dfb0a7c81390b9910d10e663af4cc1bdf6d8774a..da93d6b571bbbf103a94d4fd733264cb8a94e7cb 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/chunk_typing.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
index 39676f8f40fd83404be8fbe8ee04131aaf6f2f0e..4c3b2575f9e95220d9b3b656cd14fa11ed3ed423 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/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
------------------------------------------------------------
Function function
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
index c3d335a24738053c84d4ae2e5d27fdc1d10e1275..58865eff22dc2d0733b3c82c8270a883ca4ae487 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/chunk_typing_usable.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/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] 3 goals scheduled
---------------------------------------------
--- Context 'typed_usable_lemma' Cluster 'Chunk'
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/gnu_zero_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/gnu_zero_array.res.oracle
index 68ee566322034f899302336760f0949dc31e032a..6ae5795cc78f2501a127a8484ad9e99c848971ef 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/gnu_zero_array.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/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/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
index 2fbf1bb8baf118c8b03fc92bde0a4b04b195f7c6..f327cbfec0e80f5f0ae9ea4f221f2a8c45192f7b 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/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
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
index 7b53dd016c6e985880280d6832e73462681e5930..aa0c561557224e54f9a9f121b341bba3912c6f50 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/struct_fields.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte -wp-no-let [...]
[kernel] Parsing struct_fields.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function foo
+[rte:annot] annotating function foo
[wp] 2 goals scheduled
---------------------------------------------
--- Context 'typed_foo' Cluster 'Init_S1_X'
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 768556112b11b4547149a138b6bbc0825804aa50..98bcd99641039e586c9d25533d31f4c0c9f640af 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 d076d76ed0ca7aae9c361b7cb65df1b03f11b9d5..2c656c6f82589428c5d92e8c4a8f3218879fc66a 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 26cfc3ad34548c8ce6555176bdabbf970c5b71e0..2ac1dd590cfe6848231ee11330f3a8a46de291ef 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 2e8a5bd7c03ad64457355e2bf3317d3a86a3c29d..7ce463d9349eea815c4d793dc147ec1b41d0b8bc 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/bts_1360.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/bts_1360.res.oracle
index 264756b50180129645e0f50476ac5ceea21f5bcb..81ab1a3e10f8e8817eb8199e94cd9c52c2718e86 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/bts_1360.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/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
------------------------------------------------------------
Function foo_correct
------------------------------------------------------------
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 dbb98c6df14292b6b3f805888a739fec56d47ac8..ca40bafd86e9470752fe7e8a3d7857e471e39c67 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 5072e7c6182b7fce459e1727cd69ba7b7bb4f8b5..92f813ec7b9afb87519940378b18806dc1ea12ed 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/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
index 28237b20e82952365c6dce412e7dd899aab45260..bf6099d4282e22068301bb5f3f590903ece5442c 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication-without-overflow.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte -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] Goal typed_lemma_half : not tried
[wp] Goal typed_lemma_size : trivial
[wp] Goal typed_BinaryMultiplication_ensures_product : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle
index 048a6c47d58e6ddf6a25d77e35f3c7b63d3df16e..f1fdbe0b4cc752ffa0732f9e9ad4881d6e4b515c 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/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] Goal typed_lemma_ax1_lack : not tried
[wp] Goal typed_lemma_ax2_lack : not tried
[wp] Goal typed_lemma_ax3_lack : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle
index 3404140fd4c049bd09fa26d16d0631dc65133622..1c422c3ae8060811d27de8a6d0e4e119f5b17104 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle
@@ -1,9 +1,9 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing find.i (no preprocessing)
[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] Goal typed_find_complete_found_not_found : trivial
[wp] Goal typed_find_disjoint_found_not_found : trivial
[wp] Goal typed_find_ensures_Range : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle
index a64994d35ec0157bee80e6e73d6630ffe17ffd13..a5d9db2ea1f9b22a46441e932d40a342bd3d9e7f 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo1_solved.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing frama_c_exo1_solved.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function exo1
+[rte:annot] annotating function exo1
[wp] Goal typed_exo1_ensures : not tried
[wp] Goal typed_exo1_ensures_2 : not tried
[wp] Goal typed_exo1_assert_rte_signed_overflow : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle
index 0428d0c647cd3f9919b4ddc584cbdb65cdf8d74a..9bb5d4d873d8a99cb647128fadddaaed3dc7b3be 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo2_solved.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte -no-warn-signed-overflow [...]
[kernel] Parsing frama_c_exo2_solved.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function max_subarray
+[rte:annot] annotating function max_subarray
[wp] Goal typed_max_subarray_ensures : not tried
[wp] Goal typed_max_subarray_ensures_2 : not tried
[wp] Goal typed_max_subarray_loop_invariant_preserved : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
index 27f763c44a4745e89409af9461cc176f6d1a201f..139983c87a75d6651083a4a172c6d43bc3697a9e 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte -wp-model 'Typed (Ref)' [...]
[kernel] Parsing frama_c_exo3_solved.old.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function equal_elements
+[rte:annot] annotating function equal_elements
[wp] Goal typed_ref_equal_elements_ensures : not tried
[wp] Goal typed_ref_equal_elements_ensures_2 : not tried
[wp] Goal typed_ref_equal_elements_ensures_3 : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
index 9d37bb24d584c7bf2d9b68352d093773f9e09c21..34e76d7b36b530040ca8b365d79bdc4c9570f568 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.old.v2.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte -wp-model 'Typed (Ref)' [...]
[kernel] Parsing frama_c_exo3_solved.old.v2.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function equal_elements
+[rte:annot] annotating function equal_elements
[wp] Goal typed_ref_equal_elements_ensures_v1_good : not tried
[wp] Goal typed_ref_equal_elements_ensures_v2_good : not tried
[wp] Goal typed_ref_equal_elements_ensures_v1_v2_diff : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle
index 87662055df23ba6c321a2bc60e5b5168f5b87d15..d25f2ecbefac280ca4963cd4f74790fc611fb3e6 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/frama_c_exo3_solved.simplified.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing frama_c_exo3_solved.simplified.c (with preprocessing)
[wp] Running WP plugin...
-[rte] annotating function pair
+[rte:annot] annotating function pair
[wp] Goal typed_pair_complete_has_pair_no_pair : trivial
[wp] Goal typed_pair_disjoint_has_pair_no_pair : trivial
[wp] Goal typed_pair_loop_invariant_preserved : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/string-compare.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/string-compare.res.oracle
index 871e62444cac972f6e8273ddc1c138d4ddbf3828..50c359b8fc4f871225b38f014feb9f622fd7038b 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle/string-compare.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle/string-compare.res.oracle
@@ -1,9 +1,9 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing string-compare.c (with preprocessing)
[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] [CFG] Goal stringCompare_exits_never : Valid (Unreachable)
[wp] [CFG] Goal stringLength_exits_never : Valid (Unreachable)
[wp] Goal typed_stringCompare_complete_SomeDifferent_allEqual : trivial
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 8b3b8ce8f5b18a8b19ab37dd367fb7231c48f8bf..fda9d1592fcde0fd6bf80aa7a818d7c719d0c3e7 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 374c185811eccbf13ab99836f863fcb6f43c8ccb..c1ba41635544f4f8d2771e4caff691fbc95638e7 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 f3c3ceeb9d3ee22c07392c0ef679727b0dc47798..b6e73bdde324ab5d2f6961c6773b1b4b80656deb 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 da9813c2fb9daf073f0babb7e050055580c2d224..d3aaf8ea83ff392207675938102fb74ad56eccaa 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 0760f8c1ed9a053d7dae27231140e001e240e7e1..6fc4641c2a918d26bae446e524b503705425f3df 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 4b982f51859e9264450636ff771075ff5d74795a..472bae3aac8525769125b58c733be5e59855b4e9 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 83f9d8a5be5060dfa8c264411f2da764ffe9f6ac..9fb7098252504e09573928fbe1ffe9c1284fd622 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 46675ba6fcb4418714a63d1d5c559f395d7e3c7a..dfc94d8a3943ced736b0721f08a7b01c3b7c69c7 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 8dfaabe1c3834bffe2458219be7a460bedbd26ad..4bf9ab318fb2b123882eaa5b3254c0e63fcf9f24 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 e2cf934a567dc28914fecb97236a1751f6fcb264..9ca1fbbad3e4eaf7c77acb2bd4fd7bed774c63e1 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 8ec3a7f69f5cf0634c4cb9febbde67189426537a..d6ad1f485b30f88a8479ac41b4c90ac59985ab2a 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 fb13236dbf626facd576c4934ec557d2b0285c38..b34ba7805c8a383c50e53f0ce20467d47b9a4f90 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 15ac0f70d86c802229aaf2fdac0953b775713f3f..f22342a088335ac45d7694c7767e8f5304a6906b 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/rte.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle
index 6758f5c2af389c91e2ac42aacc7c3d4716bd6156..8dea7878486065160e34eaf37406519d2dba1139 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.0.res.oracle
@@ -5,15 +5,15 @@
[wp:rte] function job: generate rte for division by zero
[wp:rte] function job: generate rte for signed overflow
[wp] Warning: -wp-rte can annotate invalid bool value because -warn-invalid-bool is not set
-[rte] annotating function job
+[rte:annot] annotating function job
[wp:rte] function job2: generate rte for memory access
[wp:rte] function job2: generate rte for division by zero
[wp:rte] function job2: generate rte for signed overflow
-[rte] annotating function job2
+[rte:annot] annotating function job2
[wp:rte] function job3: generate rte for memory access
[wp:rte] function job3: generate rte for division by zero
[wp:rte] function job3: generate rte for signed overflow
-[rte] annotating function job3
+[rte:annot] annotating function job3
[wp] Warning: Missing RTE guards
[wp] Goal typed_job_ensures : not tried
[wp] Goal typed_job_assert_rte_mem_access : not tried
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle
index 5cb9e76206e07f7c982e840bb11552c20ee680db..cda4d24119fa289b279a889046d19551a934a6ac 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.1.res.oracle
@@ -4,15 +4,15 @@
[wp:rte] function job: generate rte for memory access
[wp:rte] function job: generate rte for division by zero
[wp:rte] function job: generate rte for invalid bool value
-[rte] annotating function job
+[rte:annot] annotating function job
[wp:rte] function job2: generate rte for memory access
[wp:rte] function job2: generate rte for division by zero
[wp:rte] function job2: generate rte for invalid bool value
-[rte] annotating function job2
+[rte:annot] annotating function job2
[wp:rte] function job3: generate rte for memory access
[wp:rte] function job3: generate rte for division by zero
[wp:rte] function job3: generate rte for invalid bool value
-[rte] annotating function job3
+[rte:annot] annotating function job3
[wp] Goal typed_job_ensures : not tried
[wp] Goal typed_job_assert_rte_mem_access : not tried
[wp] Goal typed_job_assert_rte_mem_access_2 : not tried
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle
index f78e3c8930ce95f24ba6ea0847664d402e8a53a6..60b6829e7fa5e9351579f10187b566a71c6a0b79 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.2.res.oracle
@@ -6,19 +6,19 @@
[wp:rte] function job: generate rte for signed overflow
[wp:rte] function job: generate rte for unsigned overflow
[wp:rte] function job: generate rte for invalid bool value
-[rte] annotating function job
+[rte:annot] annotating function job
[wp:rte] function job2: generate rte for memory access
[wp:rte] function job2: generate rte for division by zero
[wp:rte] function job2: generate rte for signed overflow
[wp:rte] function job2: generate rte for unsigned overflow
[wp:rte] function job2: generate rte for invalid bool value
-[rte] annotating function job2
+[rte:annot] annotating function job2
[wp:rte] function job3: generate rte for memory access
[wp:rte] function job3: generate rte for division by zero
[wp:rte] function job3: generate rte for signed overflow
[wp:rte] function job3: generate rte for unsigned overflow
[wp:rte] function job3: generate rte for invalid bool value
-[rte] annotating function job3
+[rte:annot] annotating function job3
[wp] Goal typed_job_ensures : not tried
[wp] Goal typed_job_assert_rte_mem_access : not tried
[wp] Goal typed_job_assert_rte_mem_access_2 : not tried
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle
index ca65238c06beb808941b138b80fe02065816b958..d34717c7fe54a38479169fecf5d92361e3ba8f33 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.3.res.oracle
@@ -8,17 +8,17 @@
[wp] Warning: -wp-rte and model nat require kernel to warn against signed downcast
[wp] Warning: -wp-rte and model nat require kernel to warn against unsigned downcast
[wp:rte] function job: generate rte for invalid bool value
-[rte] annotating function job
+[rte:annot] annotating function job
[wp:rte] function job2: generate rte for memory access
[wp:rte] function job2: generate rte for division by zero
[wp:rte] function job2: generate rte for signed overflow
[wp:rte] function job2: generate rte for invalid bool value
-[rte] annotating function job2
+[rte:annot] annotating function job2
[wp:rte] function job3: generate rte for memory access
[wp:rte] function job3: generate rte for division by zero
[wp:rte] function job3: generate rte for signed overflow
[wp:rte] function job3: generate rte for invalid bool value
-[rte] annotating function job3
+[rte:annot] annotating function job3
[wp] Goal typed_nat_job_ensures : not tried
[wp] Goal typed_nat_job_assert_rte_mem_access : not tried
[wp] Goal typed_nat_job_assert_rte_mem_access_2 : not tried
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle
index d4211b890b2b0d7793c20f9d35ce225d18bfd9dc..73cd9373b426130604554cadfa94254f0bf2a19e 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.4.res.oracle
@@ -8,19 +8,19 @@
[wp] Warning: -wp-rte and model nat require kernel to warn against signed downcast
[wp] Warning: -wp-rte and model nat require kernel to warn against unsigned downcast
[wp:rte] function job: generate rte for invalid bool value
-[rte] annotating function job
+[rte:annot] annotating function job
[wp:rte] function job2: generate rte for memory access
[wp:rte] function job2: generate rte for division by zero
[wp:rte] function job2: generate rte for signed overflow
[wp:rte] function job2: generate rte for unsigned overflow
[wp:rte] function job2: generate rte for invalid bool value
-[rte] annotating function job2
+[rte:annot] annotating function job2
[wp:rte] function job3: generate rte for memory access
[wp:rte] function job3: generate rte for division by zero
[wp:rte] function job3: generate rte for signed overflow
[wp:rte] function job3: generate rte for unsigned overflow
[wp:rte] function job3: generate rte for invalid bool value
-[rte] annotating function job3
+[rte:annot] annotating function job3
[wp] Goal typed_nat_job_ensures : not tried
[wp] Goal typed_nat_job_assert_rte_mem_access : not tried
[wp] Goal typed_nat_job_assert_rte_mem_access_2 : not tried
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle
index ab2f5f38105deb6dea776cc40aff3a7f66f30e1c..8dcc347a179ebd8f65416a939551a70232f28ebf 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/rte.6.res.oracle
@@ -8,15 +8,15 @@
[wp] Warning: -wp-rte and model nat require kernel to warn against signed downcast
[wp] Warning: -wp-rte and model nat require kernel to warn against unsigned downcast
[wp:rte] function job: generate rte for invalid bool value
-[rte] annotating function job
+[rte:annot] annotating function job
[wp:rte] function job2: generate rte for division by zero
[wp:rte] function job2: generate rte for signed overflow
[wp:rte] function job2: generate rte for invalid bool value
-[rte] annotating function job2
+[rte:annot] annotating function job2
[wp:rte] function job3: generate rte for division by zero
[wp:rte] function job3: generate rte for signed overflow
[wp:rte] function job3: generate rte for invalid bool value
-[rte] annotating function job3
+[rte:annot] annotating function job3
[wp] Warning: Missing RTE guards
[wp] Goal typed_nat_job_ensures : not tried
[wp] Goal typed_nat_job_assert_rte_signed_overflow : not tried
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 4378c5286a802774782011e5efcf035646661793..f002fd6fea324372319cd2b9c60bae3af26c3fdc 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
diff --git a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
index 824c33cc9629152b4a214b1138fe07c0649943d2..71cace973f704cebd22bcc5e0cdcfa3ae0655c65 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/chunk_printing.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-rte [...]
[kernel] Parsing chunk_printing.i (no preprocessing)
[wp] Running WP plugin...
-[rte] annotating function main
+[rte:annot] annotating function main
------------------------------------------------------------
Function main
------------------------------------------------------------
diff --git a/tests/rte/oracle/addsub.res.oracle b/tests/rte/oracle/addsub.res.oracle
index f0c866b0d21efe21d28ccd486d3ee704512eb4f0..b4dac4895abbfa1d9a4712046615a6237c0c7d4b 100644
--- a/tests/rte/oracle/addsub.res.oracle
+++ b/tests/rte/oracle/addsub.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing addsub.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] addsub.c:9: Warning:
guaranteed RTE:
assert signed_overflow: 0x7fffffff + 0x7fffffff ≤ 2147483647;
diff --git a/tests/rte/oracle/addsub_typedef.res.oracle b/tests/rte/oracle/addsub_typedef.res.oracle
index 55692cc6d031b8c8c5d5f351f73c688438abdf70..3c40e7028ebc3850682949bc120e4907f6867404 100644
--- a/tests/rte/oracle/addsub_typedef.res.oracle
+++ b/tests/rte/oracle/addsub_typedef.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing addsub_typedef.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] addsub_typedef.c:11: Warning:
guaranteed RTE:
assert signed_overflow: 0x7fffffff + 0x7fffffff ≤ 2147483647;
diff --git a/tests/rte/oracle/addsub_unsigned.0.res.oracle b/tests/rte/oracle/addsub_unsigned.0.res.oracle
index c99071aead7dec5ab6d13bcc935c677fdfbdf27d..4ea2c8d41feee159266b4a9e583cb5afad7de3fb 100644
--- a/tests/rte/oracle/addsub_unsigned.0.res.oracle
+++ b/tests/rte/oracle/addsub_unsigned.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing addsub_unsigned.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/rte/oracle/addsub_unsigned.1.res.oracle b/tests/rte/oracle/addsub_unsigned.1.res.oracle
index 0e2ae091f462321edf2f03b6b8c35766889bad60..8a84f4ca3ccb9721cffc8c4867a8eb4cf4e5d4e7 100644
--- a/tests/rte/oracle/addsub_unsigned.1.res.oracle
+++ b/tests/rte/oracle/addsub_unsigned.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing addsub_unsigned.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] addsub_unsigned.c:12: Warning:
guaranteed RTE:
assert unsigned_overflow: 0x80000000U + 0x80000000U ≤ 4294967295;
diff --git a/tests/rte/oracle/addsub_unsigned_typedef.0.res.oracle b/tests/rte/oracle/addsub_unsigned_typedef.0.res.oracle
index 9852fff86bbc1c9e24e4fedeebc541adde8128cb..2311039ae1d45dc573f3873273e8e98950634475 100644
--- a/tests/rte/oracle/addsub_unsigned_typedef.0.res.oracle
+++ b/tests/rte/oracle/addsub_unsigned_typedef.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing addsub_unsigned_typedef.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
typedef unsigned int uint;
int main(void)
diff --git a/tests/rte/oracle/addsub_unsigned_typedef.1.res.oracle b/tests/rte/oracle/addsub_unsigned_typedef.1.res.oracle
index 4df8f61afa49717d246cc1a177ad30f148c67d12..eff8fadf68bf0be7e364d137632c0d1f81cd4540 100644
--- a/tests/rte/oracle/addsub_unsigned_typedef.1.res.oracle
+++ b/tests/rte/oracle/addsub_unsigned_typedef.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing addsub_unsigned_typedef.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] addsub_unsigned_typedef.c:14: Warning:
guaranteed RTE:
assert unsigned_overflow: 0x80000000U + 0x80000000U ≤ 4294967295;
diff --git a/tests/rte/oracle/array_index.0.res.oracle b/tests/rte/oracle/array_index.0.res.oracle
index 8accf01a55dc343bab04ca7d4977572f0d72fd11..b4dc5ead5aa2c07c804ab5501dde97202b9e4916 100644
--- a/tests/rte/oracle/array_index.0.res.oracle
+++ b/tests/rte/oracle/array_index.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing array_index.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
struct s_arr {
int t[15] ;
@@ -70,7 +70,7 @@ void main(int i, int j, unsigned int k)
}
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
struct s_arr {
int t[15] ;
diff --git a/tests/rte/oracle/array_index.1.res.oracle b/tests/rte/oracle/array_index.1.res.oracle
index 1ed933d0895f146fe16f9dfba43f968400b6e3f1..c874d736490e80bc174c5100f82ad301be679fee 100644
--- a/tests/rte/oracle/array_index.1.res.oracle
+++ b/tests/rte/oracle/array_index.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing array_index.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
struct s_arr {
int t[15] ;
diff --git a/tests/rte/oracle/assign.res.oracle b/tests/rte/oracle/assign.res.oracle
index fcfb2be909a7a746c433e6bce806fecd6035bc50..ca5c9db5783dcdfdad1ad1410409f7b973af34c6 100644
--- a/tests/rte/oracle/assign.res.oracle
+++ b/tests/rte/oracle/assign.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing assign.c (with preprocessing)
-[rte] annotating function rte
+[rte:annot] annotating function rte
/* Generated by Frama-C */
int global_x;
int global_y;
diff --git a/tests/rte/oracle/assign2.res.oracle b/tests/rte/oracle/assign2.res.oracle
index bbe12161c39f1e1b8dbf9595f23c1930a7f9ad71..d74bcff7ce69a6d58544ac2557c0b275b40c9548 100644
--- a/tests/rte/oracle/assign2.res.oracle
+++ b/tests/rte/oracle/assign2.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing assign2.c (with preprocessing)
-[rte] annotating function f
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function main
/* Generated by Frama-C */
int i;
int t[10];
diff --git a/tests/rte/oracle/assign3.res.oracle b/tests/rte/oracle/assign3.res.oracle
index a7bd3a047b9c2d4180571ba12faa0fd3f803ae83..f8c3cc3879fab231263728a29c41504a18bd3760 100644
--- a/tests/rte/oracle/assign3.res.oracle
+++ b/tests/rte/oracle/assign3.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing assign3.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
/*@ assigns \nothing; */
int f(void);
diff --git a/tests/rte/oracle/assign4.res.oracle b/tests/rte/oracle/assign4.res.oracle
index a232f0d1d596b429c2f64b41c7c8d7c67ee2859d..60a3b9a2bc6a996182f6f6798c92a98fbc9e5ada 100644
--- a/tests/rte/oracle/assign4.res.oracle
+++ b/tests/rte/oracle/assign4.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing assign4.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
/*@ assigns \result;
assigns \result \from min, max; */
diff --git a/tests/rte/oracle/assign5.res.oracle b/tests/rte/oracle/assign5.res.oracle
index 838610a781c0c47a07f8b9de0b730ebfc36f8f09..72815caa8d8ac14e38de16589b811f7390bb55db 100644
--- a/tests/rte/oracle/assign5.res.oracle
+++ b/tests/rte/oracle/assign5.res.oracle
@@ -3,7 +3,7 @@
Drop '*p' \from at assign5.c:9 for more precise one at assign5.c:10
[kernel:annot:multi-from] Warning:
Drop '*p' \from at assign5.c:19 for more precise one at assign5.c:18
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
/*@ assigns *p;
assigns *p \from \nothing; */
diff --git a/tests/rte/oracle/assign6.res.oracle b/tests/rte/oracle/assign6.res.oracle
index cc82419239229df12a43e0121fd42d2136f2b695..b6a449d4decb9b789553e0afdb3e29c25f4e4be4 100644
--- a/tests/rte/oracle/assign6.res.oracle
+++ b/tests/rte/oracle/assign6.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing assign6.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int z;
/*@ assigns z, \result;
diff --git a/tests/rte/oracle/assign7.res.oracle b/tests/rte/oracle/assign7.res.oracle
index e7533eeb90197415ce55a38df0ab5adf087f9177..6ba453fd9abebb4bc7229fab8a8b81eb932fc973 100644
--- a/tests/rte/oracle/assign7.res.oracle
+++ b/tests/rte/oracle/assign7.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing assign7.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
/*@ assigns *p;
assigns *p \from {*((char *)p), *q}; */
diff --git a/tests/rte/oracle/bool.res.oracle b/tests/rte/oracle/bool.res.oracle
index d215b26dbeabe81d4cd19dc2bb21cc00ede795d9..a8c11132b82c84e734c9b4de007931595c68fce1 100644
--- a/tests/rte/oracle/bool.res.oracle
+++ b/tests/rte/oracle/bool.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing bool.i (no preprocessing)
-[rte] annotating function ko1
-[rte] annotating function ko2
-[rte] annotating function ok1
-[rte] annotating function ok2
+[rte:annot] annotating function ko1
+[rte:annot] annotating function ko2
+[rte:annot] annotating function ok1
+[rte:annot] annotating function ok2
/* Generated by Frama-C */
struct s_bool {
char c ;
@@ -57,10 +57,10 @@ _Bool ok2(int a, _Bool b)
}
-[rte] annotating function ko1
-[rte] annotating function ko2
-[rte] annotating function ok1
-[rte] annotating function ok2
+[rte:annot] annotating function ko1
+[rte:annot] annotating function ko2
+[rte:annot] annotating function ok1
+[rte:annot] annotating function ok2
/* Generated by Frama-C */
struct s_bool {
char c ;
diff --git a/tests/rte/oracle/bts0567.res.oracle b/tests/rte/oracle/bts0567.res.oracle
index 124606df9992905befe1bb47798331da77c86c2e..460f19e9262766b75e7eecf4c83cd134e2bc4dc2 100644
--- a/tests/rte/oracle/bts0567.res.oracle
+++ b/tests/rte/oracle/bts0567.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing bts0567.c (with preprocessing)
-[rte] annotating function g
+[rte:annot] annotating function g
/* Generated by Frama-C */
int tab[2];
/*@ requires \valid(p + 1); */
diff --git a/tests/rte/oracle/bts0576.res.oracle b/tests/rte/oracle/bts0576.res.oracle
index 301f69b8472518b1da1d6fbf5537f3747355cd3d..fe8a1ac974626ba3be47060ba2806de74b51d719 100644
--- a/tests/rte/oracle/bts0576.res.oracle
+++ b/tests/rte/oracle/bts0576.res.oracle
@@ -3,8 +3,8 @@
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[kernel] bts0576.c:6: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[rte] annotating function f4
-[rte] annotating function g4
+[rte:annot] annotating function f4
+[rte:annot] annotating function g4
/* Generated by Frama-C */
typedef double typetab[2];
/*@ requires
diff --git a/tests/rte/oracle/bts0580.res.oracle b/tests/rte/oracle/bts0580.res.oracle
index 86ffdc6a61bad80f8fd95c3af08ca20656b1a963..b2e54ea6b5d43eeb3f20ca58ff0a0f9a3d3bf5e9 100644
--- a/tests/rte/oracle/bts0580.res.oracle
+++ b/tests/rte/oracle/bts0580.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing bts0580.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
struct ArrayStruct {
int data[10] ;
diff --git a/tests/rte/oracle/bts0580_2.res.oracle b/tests/rte/oracle/bts0580_2.res.oracle
index 86213f1e2e4a0c76a88eba8f3247a8f6bf1ec127..cbd014a78b6a95d93360b8e251fc45bff4c8364b 100644
--- a/tests/rte/oracle/bts0580_2.res.oracle
+++ b/tests/rte/oracle/bts0580_2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing bts0580_2.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
struct S {
int val ;
diff --git a/tests/rte/oracle/bts1052.res.oracle b/tests/rte/oracle/bts1052.res.oracle
index 8d80a63a7885804420ae0338ed1ef2a6f33ebaac..d2a4ffff649b68e46aeef864f11adc88313148ff 100644
--- a/tests/rte/oracle/bts1052.res.oracle
+++ b/tests/rte/oracle/bts1052.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing bts1052.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
/*@ ensures \let count = \old(d); \result ≡ count;
assigns \nothing; */
diff --git a/tests/rte/oracle/bts2314.res.oracle b/tests/rte/oracle/bts2314.res.oracle
index e2078a75b5383fc4b77ab7d881f0b3155434086c..750e1ede564a90adfc376233ab09e8cf2ffadd02 100644
--- a/tests/rte/oracle/bts2314.res.oracle
+++ b/tests/rte/oracle/bts2314.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing bts2314.i (no preprocessing)
-[rte] annotating function foo
+[rte:annot] annotating function foo
/* Generated by Frama-C */
struct STR {
int num : 7 ;
diff --git a/tests/rte/oracle/bts621.res.oracle b/tests/rte/oracle/bts621.res.oracle
index d5d1f93ac89792a8ca881390a4f705dc25124782..86d3ba9505b98a0622068997d6002a56aef6cc74 100644
--- a/tests/rte/oracle/bts621.res.oracle
+++ b/tests/rte/oracle/bts621.res.oracle
@@ -10,7 +10,7 @@ void f(void) /*@ ghost (float a) */
}
-[rte] annotating function f
+[rte:annot] annotating function f
/* Generated by Frama-C */
/*@ ghost /@ assigns *p; @/
float g(float \ghost *p); */
diff --git a/tests/rte/oracle/castoncall.0.res.oracle b/tests/rte/oracle/castoncall.0.res.oracle
index e9626099a5c174f5451a72844c1101a8ca920002..2e6f716bbe1c6be7c2261cb5c4b6190e3df24492 100644
--- a/tests/rte/oracle/castoncall.0.res.oracle
+++ b/tests/rte/oracle/castoncall.0.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing castoncall.c (with preprocessing)
-[rte] annotating function g
-[rte] annotating function nondet_ptr
+[rte:annot] annotating function g
+[rte:annot] annotating function nondet_ptr
/* Generated by Frama-C */
/*@ ensures \result ≡ \old(a) ∨ \result ≡ \old(b);
assigns \result;
diff --git a/tests/rte/oracle/castoncall.1.res.oracle b/tests/rte/oracle/castoncall.1.res.oracle
index e9626099a5c174f5451a72844c1101a8ca920002..2e6f716bbe1c6be7c2261cb5c4b6190e3df24492 100644
--- a/tests/rte/oracle/castoncall.1.res.oracle
+++ b/tests/rte/oracle/castoncall.1.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing castoncall.c (with preprocessing)
-[rte] annotating function g
-[rte] annotating function nondet_ptr
+[rte:annot] annotating function g
+[rte:annot] annotating function nondet_ptr
/* Generated by Frama-C */
/*@ ensures \result ≡ \old(a) ∨ \result ≡ \old(b);
assigns \result;
diff --git a/tests/rte/oracle/divmod.res.oracle b/tests/rte/oracle/divmod.res.oracle
index f7f9626762ac19e218518238d3c8636174a0f0b9..547de8eb072a7a22a19f9248bf80dfda2672bc44 100644
--- a/tests/rte/oracle/divmod.res.oracle
+++ b/tests/rte/oracle/divmod.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing divmod.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] divmod.c:13: Warning:
guaranteed RTE:
assert
diff --git a/tests/rte/oracle/divmod_typedef.res.oracle b/tests/rte/oracle/divmod_typedef.res.oracle
index 9d2cba27982e54d9bfb1bba23de7f6ac5179cd1d..e87059926ae6ea679c3aa891622f42e1b1b96f7f 100644
--- a/tests/rte/oracle/divmod_typedef.res.oracle
+++ b/tests/rte/oracle/divmod_typedef.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing divmod_typedef.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] divmod_typedef.c:15: Warning:
guaranteed RTE:
assert
diff --git a/tests/rte/oracle/downcast.0.res.oracle b/tests/rte/oracle/downcast.0.res.oracle
index 6cad4d434e8a640d27237196e90b821777ae7798..f0eb8647a50823b0998aa831ba8959da03429ec1 100644
--- a/tests/rte/oracle/downcast.0.res.oracle
+++ b/tests/rte/oracle/downcast.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing downcast.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/rte/oracle/downcast.1.res.oracle b/tests/rte/oracle/downcast.1.res.oracle
index a99e7d028ad364f7e49c3b1188c785ee7816a273..e2c3482d90a18e6150b45080f3788e59da6ef7da 100644
--- a/tests/rte/oracle/downcast.1.res.oracle
+++ b/tests/rte/oracle/downcast.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing downcast.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/rte/oracle/downcast.2.res.oracle b/tests/rte/oracle/downcast.2.res.oracle
index 4335c6b252d14d919ab9bf70c14102d3051c8874..90eac7967f43cb758d01ee973169638affbca14a 100644
--- a/tests/rte/oracle/downcast.2.res.oracle
+++ b/tests/rte/oracle/downcast.2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing downcast.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/rte/oracle/finite_float.res.oracle b/tests/rte/oracle/finite_float.res.oracle
index 8d1f55b0872281aa5c212e7b2aba34bd41e0e4ed..9384123fbe73e75f4df1f7acc8fded59832f7e44 100644
--- a/tests/rte/oracle/finite_float.res.oracle
+++ b/tests/rte/oracle/finite_float.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing finite_float.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
#include "errno.h"
#include "math.h"
diff --git a/tests/rte/oracle/float_to_int.res.oracle b/tests/rte/oracle/float_to_int.res.oracle
index 66a24415256c21b4c9f68c51b4ae360b2191f600..85321b80f0c8473e16cf6846e56fc7a1a833c45c 100644
--- a/tests/rte/oracle/float_to_int.res.oracle
+++ b/tests/rte/oracle/float_to_int.res.oracle
@@ -2,7 +2,7 @@
[kernel:parser:decimal-float] float_to_int.c:13: Warning:
Floating-point constant 1.5e255 is not represented exactly. Will use 0x1.99309cc247f15p847.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] float_to_int.c:14: Warning:
guaranteed RTE: assert float_to_int: 258. < 128;
[rte] float_to_int.c:16: Warning:
diff --git a/tests/rte/oracle/fptr_assert.res.oracle b/tests/rte/oracle/fptr_assert.res.oracle
index 408070ad2a98b2091ddfe9be3e9a9e5ad0321565..f48df710fe1efdd1df9253038c02dc72bd40b305 100644
--- a/tests/rte/oracle/fptr_assert.res.oracle
+++ b/tests/rte/oracle/fptr_assert.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing fptr_assert.c (with preprocessing)
-[rte] annotating function f
-[rte] annotating function g
-[rte] annotating function h
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function g
+[rte:annot] annotating function h
+[rte:annot] annotating function main
/* Generated by Frama-C */
typedef int (*fptr)(int );
void g(void)
diff --git a/tests/rte/oracle/gnu_zero_length.res.oracle b/tests/rte/oracle/gnu_zero_length.res.oracle
index b5373e6738d8a7a4c9e961627b8b56a4f6cbb0e5..29ec3ac3638a2a2d2a18c44147143adca28f3e5a 100644
--- a/tests/rte/oracle/gnu_zero_length.res.oracle
+++ b/tests/rte/oracle/gnu_zero_length.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing gnu_zero_length.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
#include "stdlib.h"
struct S {
diff --git a/tests/rte/oracle/initialized-ignore-fct.0.res.oracle b/tests/rte/oracle/initialized-ignore-fct.0.res.oracle
index b5622559b367a0dd9accf67154ca8c5016f6a4e5..2d021d4b453a5087b06a36c60224ad92e9713465 100644
--- a/tests/rte/oracle/initialized-ignore-fct.0.res.oracle
+++ b/tests/rte/oracle/initialized-ignore-fct.0.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing initialized-ignore-fct.i (no preprocessing)
-[rte] annotating function f1
-[rte] annotating function f2
+[rte:annot] annotating function f1
+[rte:annot] annotating function f2
/* Generated by Frama-C */
int f1(void)
{
diff --git a/tests/rte/oracle/initialized-ignore-fct.1.res.oracle b/tests/rte/oracle/initialized-ignore-fct.1.res.oracle
index de012787ba2ce83d57137da8883486b8275823a9..bd848564e8f04c5f40bad5386074df6ef7f6ee3f 100644
--- a/tests/rte/oracle/initialized-ignore-fct.1.res.oracle
+++ b/tests/rte/oracle/initialized-ignore-fct.1.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing initialized-ignore-fct.i (no preprocessing)
-[rte] annotating function f1
-[rte] annotating function f2
+[rte:annot] annotating function f1
+[rte:annot] annotating function f2
/* Generated by Frama-C */
int f1(void)
{
diff --git a/tests/rte/oracle/initialized.res.oracle b/tests/rte/oracle/initialized.res.oracle
index b03435818eae10b0af0098e72c964e726903f2d8..e1f4052e4bdbd3aad78ce1c93c8a957870cfb15c 100644
--- a/tests/rte/oracle/initialized.res.oracle
+++ b/tests/rte/oracle/initialized.res.oracle
@@ -2,9 +2,9 @@
[kernel:parser:decimal-float] initialized.c:111: Warning:
Floating-point constant 1.1234 is not represented exactly. Will use 0x1.1f972474538efp0.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
-[rte] annotating function f
-[rte] annotating function g
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function g
+[rte:annot] annotating function main
/* Generated by Frama-C */
struct R {
int v ;
diff --git a/tests/rte/oracle/initialized_union.0.res.oracle b/tests/rte/oracle/initialized_union.0.res.oracle
index 363a06a2446bc1b0a4ce62d9e7226d8cf4e0daa9..cf3f97b0fcf44d909c8a6e6453e9e680607e2896 100644
--- a/tests/rte/oracle/initialized_union.0.res.oracle
+++ b/tests/rte/oracle/initialized_union.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing initialized_union.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
union U {
char c ;
diff --git a/tests/rte/oracle/initialized_union.1.res.oracle b/tests/rte/oracle/initialized_union.1.res.oracle
index 5123e79dcd4f96a6ece38caa61d7fa378db44c85..fac802cd4611fc15de726ea1f1ba5106057d8463 100644
--- a/tests/rte/oracle/initialized_union.1.res.oracle
+++ b/tests/rte/oracle/initialized_union.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing initialized_union.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
union U {
char c ;
diff --git a/tests/rte/oracle/invalid_fptr.res.oracle b/tests/rte/oracle/invalid_fptr.res.oracle
index 8e8c9e80b62f2f39637dacdb87bf7ebdd0d935a1..65c8cdee74afa99ef846fb5984c3701c9f45c54b 100644
--- a/tests/rte/oracle/invalid_fptr.res.oracle
+++ b/tests/rte/oracle/invalid_fptr.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing invalid_fptr.i (no preprocessing)
-[rte] annotating function f
-[rte] annotating function g
-[rte] annotating function h
+[rte:annot] annotating function f
+[rte:annot] annotating function g
+[rte:annot] annotating function h
/* Generated by Frama-C */
struct S {
void (*f)(void) ;
diff --git a/tests/rte/oracle/malloc.res.oracle b/tests/rte/oracle/malloc.res.oracle
index e5a358b1766c97a7df648de8af00cbe876abda92..d90e7d2052044627005426148f2733cdd55a27ed 100644
--- a/tests/rte/oracle/malloc.res.oracle
+++ b/tests/rte/oracle/malloc.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing malloc.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
/*@ ensures \result ≡ \null ∨ \fresh{Old, Here}(\result,10);
allocates \result;
diff --git a/tests/rte/oracle/memaccess.res.oracle b/tests/rte/oracle/memaccess.res.oracle
index 9890fa2ce1f31a803cfbbcd791c1abcfa1d510ba..570dd686f62bf8a94e681052f69fab1a84be25aa 100644
--- a/tests/rte/oracle/memaccess.res.oracle
+++ b/tests/rte/oracle/memaccess.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing memaccess.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(int x)
{
diff --git a/tests/rte/oracle/minus.0.res.oracle b/tests/rte/oracle/minus.0.res.oracle
index ea528f3492b12c29f248d07ecbe22f2ca50e6e03..77df3b0b03d4a660022539fbccd38d12177d4e60 100644
--- a/tests/rte/oracle/minus.0.res.oracle
+++ b/tests/rte/oracle/minus.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing minus.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] minus.c:11: Warning:
guaranteed RTE:
assert signed_overflow: -2147483647 ≤ (int)(-0x7fffffff) - 1;
diff --git a/tests/rte/oracle/minus.1.res.oracle b/tests/rte/oracle/minus.1.res.oracle
index 93157b6539b3417fdb709731c094222b576b234b..4680985ca143b0f3f99aa520590ed9663da49e40 100644
--- a/tests/rte/oracle/minus.1.res.oracle
+++ b/tests/rte/oracle/minus.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing minus.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/rte/oracle/mul.res.oracle b/tests/rte/oracle/mul.res.oracle
index 690b65668dccbfcebeaaf8cddd7420d81426bccd..7780b2f1df41b16655dc7a582d3f9f9bd534fabf 100644
--- a/tests/rte/oracle/mul.res.oracle
+++ b/tests/rte/oracle/mul.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing mul.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] mul.c:22: Warning:
guaranteed RTE: assert signed_overflow: 0xffff * 0xffff ≤ 2147483647;
[rte] mul.c:25: Warning:
diff --git a/tests/rte/oracle/noresult.res.oracle b/tests/rte/oracle/noresult.res.oracle
index 429612edba6d1b3d4dc6b8950415b5a39182aedc..500f819e490f4a8f8bf4ec26826bdb6ba1c80ef4 100644
--- a/tests/rte/oracle/noresult.res.oracle
+++ b/tests/rte/oracle/noresult.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing noresult.c (with preprocessing)
-[rte] annotating function job
+[rte:annot] annotating function job
/* Generated by Frama-C */
int x;
/*@ ensures \result > 0;
diff --git a/tests/rte/oracle/postcond.res.oracle b/tests/rte/oracle/postcond.res.oracle
index 44f61804593a60c4ce2e5c2f2c5c4d41a3fdd6c3..90c0eea09219fe670d7c5f6a6e3109be770fac42 100644
--- a/tests/rte/oracle/postcond.res.oracle
+++ b/tests/rte/oracle/postcond.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing postcond.c (with preprocessing)
-[rte] annotating function f
-[rte] annotating function g
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function g
+[rte:annot] annotating function main
/* Generated by Frama-C */
/*@ ensures \result ≡ -\old(x);
diff --git a/tests/rte/oracle/postcond2.res.oracle b/tests/rte/oracle/postcond2.res.oracle
index eb5282ae2d4ba91faefc3855b5d781dad82251ea..8295cfe205a8c7ef75444a26ff488d2adb3bbd6f 100644
--- a/tests/rte/oracle/postcond2.res.oracle
+++ b/tests/rte/oracle/postcond2.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing postcond2.c (with preprocessing)
[kernel] postcond2.c:7: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[rte] annotating function f
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function main
/* Generated by Frama-C */
/*@ requires \valid(x);
requires \valid(x + (0 .. 10));
diff --git a/tests/rte/oracle/precond.res.oracle b/tests/rte/oracle/precond.res.oracle
index c538407703edd8a5335ddfbf5345194b6f6001a7..edc7bde6dcd35c38afae13517f04edda40fe688e 100644
--- a/tests/rte/oracle/precond.res.oracle
+++ b/tests/rte/oracle/precond.res.oracle
@@ -1,15 +1,15 @@
[kernel] Parsing precond.c (with preprocessing)
[kernel] precond.c:27: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[rte] annotating function f
-[rte] annotating function g
-[rte] annotating function h
-[rte] annotating function main
-[rte] annotating function next_val
-[rte] annotating function set
-[rte] annotating function tabtop_set
-[rte] annotating function top_next
-[rte] annotating function top_set
+[rte:annot] annotating function f
+[rte:annot] annotating function g
+[rte:annot] annotating function h
+[rte:annot] annotating function main
+[rte:annot] annotating function next_val
+[rte:annot] annotating function set
+[rte:annot] annotating function tabtop_set
+[rte:annot] annotating function top_next
+[rte:annot] annotating function top_set
/* Generated by Frama-C */
struct cell {
int val ;
diff --git a/tests/rte/oracle/precond2.res.oracle b/tests/rte/oracle/precond2.res.oracle
index be1becab2f9f402e00bfad079a46fbad526286dc..c9a7dadda29c21d7a546122d350f9c5f637e1a2c 100644
--- a/tests/rte/oracle/precond2.res.oracle
+++ b/tests/rte/oracle/precond2.res.oracle
@@ -36,9 +36,9 @@ int main(void)
[kernel] kf = g rte_gen_status = false
[kernel] kf = main rte_gen_status = false
[kernel] computing rte-div annotations
-[rte] annotating function f
-[rte] annotating function g
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function g
+[rte:annot] annotating function main
/* Generated by Frama-C */
int global = 15;
/*@ requires x > 0;
diff --git a/tests/rte/oracle/reqlabl.res.oracle b/tests/rte/oracle/reqlabl.res.oracle
index 29a3506c575e027125136da523e2626b675e71f4..b17860e0ac4e5ec52ad9c2917aae5a2fa9da3b47 100644
--- a/tests/rte/oracle/reqlabl.res.oracle
+++ b/tests/rte/oracle/reqlabl.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing reqlabl.c (with preprocessing)
-[rte] annotating function g
+[rte:annot] annotating function g
/* Generated by Frama-C */
/*@ requires PROP_SUR_982: x > 0; */
int f(int x);
diff --git a/tests/rte/oracle/reqlabl2.res.oracle b/tests/rte/oracle/reqlabl2.res.oracle
index 78cfc2ab4932c5e941dc0594a03abefa7c5f14de..e8dcf022daf84c565db6a66afcb2385e4f626f90 100644
--- a/tests/rte/oracle/reqlabl2.res.oracle
+++ b/tests/rte/oracle/reqlabl2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing reqlabl2.c (with preprocessing)
-[rte] annotating function g
+[rte:annot] annotating function g
/* Generated by Frama-C */
/*@ requires PROP_SUR_982: x > 0;
requires PROP_SUR_982: x + 1 > 1;
diff --git a/tests/rte/oracle/s64.res.oracle b/tests/rte/oracle/s64.res.oracle
index 9962e9e0c63ae9cc7fc9591bed6047c38aedb444..e7f45a9c81c24573bddc3591bee716d8a36e6e8a 100644
--- a/tests/rte/oracle/s64.res.oracle
+++ b/tests/rte/oracle/s64.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing s64.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] s64.c:9: Warning:
guaranteed RTE: assert signed_overflow: 5LL << 63 ≤ 9223372036854775807;
/* Generated by Frama-C */
diff --git a/tests/rte/oracle/shift.0.res.oracle b/tests/rte/oracle/shift.0.res.oracle
index fac26f0c2c00feb60eb539d4ea0a98ebd2d5b403..2ef426e4e19a108a8c053488182b709d0f18261a 100644
--- a/tests/rte/oracle/shift.0.res.oracle
+++ b/tests/rte/oracle/shift.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing shift.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] shift.c:13: Warning:
guaranteed RTE: assert signed_overflow: 5 << 30 ≤ 2147483647;
[rte] shift.c:14: Warning:
diff --git a/tests/rte/oracle/shift.1.res.oracle b/tests/rte/oracle/shift.1.res.oracle
index f25446780e5b3c1f991179f9bc1abe0af95e7ad2..71293c7015d4a87f665c47f3ea07a21becad2556 100644
--- a/tests/rte/oracle/shift.1.res.oracle
+++ b/tests/rte/oracle/shift.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing shift.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] shift.c:13: Warning:
guaranteed RTE: assert signed_overflow: 5 << 30 ≤ 2147483647;
[rte] shift.c:14: Warning:
diff --git a/tests/rte/oracle/shift_machdep.0.res.oracle b/tests/rte/oracle/shift_machdep.0.res.oracle
index c684e70b621f3c2dd96eaefaa49046ae885ce19a..3bccf76f35e0eb3aa36745a0b0d124d5bc324e02 100644
--- a/tests/rte/oracle/shift_machdep.0.res.oracle
+++ b/tests/rte/oracle/shift_machdep.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing shift_machdep.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] shift_machdep.c:9: Warning:
guaranteed RTE: assert signed_overflow: 5 << 30 ≤ 2147483647;
[rte] shift_machdep.c:10: Warning:
diff --git a/tests/rte/oracle/shift_machdep.1.res.oracle b/tests/rte/oracle/shift_machdep.1.res.oracle
index 271e95d3fef9980adaf9ee1866a562742030aabe..52848785faa85dfdfee1cd126c8ac9141a3d24f7 100644
--- a/tests/rte/oracle/shift_machdep.1.res.oracle
+++ b/tests/rte/oracle/shift_machdep.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing shift_machdep.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] shift_machdep.c:9: Warning:
guaranteed RTE: assert signed_overflow: 5 << 30 ≤ 2147483647;
/* Generated by Frama-C */
diff --git a/tests/rte/oracle/shift_unsigned.0.res.oracle b/tests/rte/oracle/shift_unsigned.0.res.oracle
index 919126c899a6914ad07d052b11b12afc0ab41434..3d0738f19d8a66b24b989df75975bed9d113c887 100644
--- a/tests/rte/oracle/shift_unsigned.0.res.oracle
+++ b/tests/rte/oracle/shift_unsigned.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing shift_unsigned.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] shift_unsigned.c:11: Warning:
guaranteed RTE: assert shift: 0 ≤ (int)(-3) < 32;
[rte] shift_unsigned.c:12: Warning:
diff --git a/tests/rte/oracle/shift_unsigned.1.res.oracle b/tests/rte/oracle/shift_unsigned.1.res.oracle
index 93f591b75aec36523dc821921f0a7a35d20d4e5c..65fef595aa5dc03efcccbcbfb39f0dadf9b95930 100644
--- a/tests/rte/oracle/shift_unsigned.1.res.oracle
+++ b/tests/rte/oracle/shift_unsigned.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing shift_unsigned.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[rte] shift_unsigned.c:10: Warning:
guaranteed RTE: assert unsigned_overflow: 0x10000000U << 4 ≤ 4294967295;
[rte] shift_unsigned.c:11: Warning:
diff --git a/tests/rte/oracle/sizeof.res.oracle b/tests/rte/oracle/sizeof.res.oracle
index d9b591c01838c896c650280ade7e6c952f9aaa49..dcbe35e009cacb432a529d26caa752135859796b 100644
--- a/tests/rte/oracle/sizeof.res.oracle
+++ b/tests/rte/oracle/sizeof.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing sizeof.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/rte/oracle/tab.res.oracle b/tests/rte/oracle/tab.res.oracle
index 36efb414b362605a827c204b9763e385b60ba482..d1bf4952e047a91a77b5e3936f14538d5228b1f0 100644
--- a/tests/rte/oracle/tab.res.oracle
+++ b/tests/rte/oracle/tab.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing tab.c (with preprocessing)
-[rte] annotating function f4
-[rte] annotating function g4
-[rte] annotating function h4
-[rte] annotating function i4
+[rte:annot] annotating function f4
+[rte:annot] annotating function g4
+[rte:annot] annotating function h4
+[rte:annot] annotating function i4
/* Generated by Frama-C */
typedef double typetab[2];
double g4(typetab *t)
diff --git a/tests/rte/oracle/threefunc.res.oracle b/tests/rte/oracle/threefunc.res.oracle
index b17bc72a467afba601542f1d32359cd077f5ce8a..d503cbde3115129c5ab80014ba5376bc70d6b5a8 100644
--- a/tests/rte/oracle/threefunc.res.oracle
+++ b/tests/rte/oracle/threefunc.res.oracle
@@ -68,9 +68,9 @@ int main(void)
[kernel] ================================
-[rte] annotating function f
-[rte] annotating function g
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function g
+[rte:annot] annotating function main
/* Generated by Frama-C */
int g(int x, int y)
{
@@ -230,8 +230,8 @@ int main(void)
[kernel] kf = f rte_gen_status = true
[kernel] kf = g rte_gen_status = true
[kernel] kf = main rte_gen_status = true
-[rte] annotating function f
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function main
/* Generated by Frama-C */
int g(int x, int y)
{
diff --git a/tests/rte/oracle/twofunc.res.oracle b/tests/rte/oracle/twofunc.res.oracle
index f7a227bd6fe2f82507fba60f47407ea3d7695de0..ec2e7aa894769533265e457e6a9db29a16b5d602 100644
--- a/tests/rte/oracle/twofunc.res.oracle
+++ b/tests/rte/oracle/twofunc.res.oracle
@@ -59,8 +59,8 @@ int main(void)
[kernel] ================================
-[rte] annotating function f
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function main
/* Generated by Frama-C */
int f(int x, int y)
{
diff --git a/tests/rte/oracle/twofunc3.res.oracle b/tests/rte/oracle/twofunc3.res.oracle
index 5ba5ff7a353b3b41a67e633aa35c0bf8d9ba1204..8145b8387fff52a03d4b24b89eed580ebbda4a9e 100644
--- a/tests/rte/oracle/twofunc3.res.oracle
+++ b/tests/rte/oracle/twofunc3.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing twofunc3.c (with preprocessing)
-[rte] annotating function f
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function main
/* Generated by Frama-C */
int f(int x, int y)
{
diff --git a/tests/rte/oracle/u64.0.res.oracle b/tests/rte/oracle/u64.0.res.oracle
index 3d119314fd064d0345bff169e3690c7495aa25e9..60b5b87a4356a025caed762404445f5b37694ef2 100644
--- a/tests/rte/oracle/u64.0.res.oracle
+++ b/tests/rte/oracle/u64.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing u64.i (no preprocessing)
-[rte] annotating function f
+[rte:annot] annotating function f
/* Generated by Frama-C */
unsigned long f(unsigned int n)
{
diff --git a/tests/rte/oracle/u64.1.res.oracle b/tests/rte/oracle/u64.1.res.oracle
index 8e3f397dd47b12b29a406d45144a47ba4c9460a2..7b827cd0302e6cc5ed4317b4a41d568e9a45fdff 100644
--- a/tests/rte/oracle/u64.1.res.oracle
+++ b/tests/rte/oracle/u64.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing u64.i (no preprocessing)
-[rte] annotating function f
+[rte:annot] annotating function f
/* Generated by Frama-C */
unsigned long f(unsigned int n)
{
diff --git a/tests/rte/oracle/valid.res.oracle b/tests/rte/oracle/valid.res.oracle
index a52448f326b4e52e3c53ed2da56bb6ee101ce5ae..4ecd43c7e72339eccb8c260f022b83584c8c159c 100644
--- a/tests/rte/oracle/valid.res.oracle
+++ b/tests/rte/oracle/valid.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing valid.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
struct R {
int v ;
@@ -199,7 +199,7 @@ int main(void)
}
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
struct R {
int v ;
diff --git a/tests/rte/oracle/value_rte.res.oracle b/tests/rte/oracle/value_rte.res.oracle
index f0e668da4a4d0b4be09946158d008f6e17a47b43..929fc1551d0077b7a800819bd47b20c44a4c2620 100644
--- a/tests/rte/oracle/value_rte.res.oracle
+++ b/tests/rte/oracle/value_rte.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing value_rte.c (with preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/rte_manual/oracle/bitwise.res.oracle b/tests/rte_manual/oracle/bitwise.res.oracle
index 544815c2b1e874ee6ecb2adadf3a2f3c6c623d1d..e6760d6973280c7890daef4ac5096a102bffe519 100644
--- a/tests/rte_manual/oracle/bitwise.res.oracle
+++ b/tests/rte_manual/oracle/bitwise.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing bitwise.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/rte_manual/oracle/contract.res.oracle b/tests/rte_manual/oracle/contract.res.oracle
index 3cfac7395bf2dc93ef725b3a726e64fc69695e06..61ab777f07378b59f57796e50692e7e682e36921 100644
--- a/tests/rte_manual/oracle/contract.res.oracle
+++ b/tests/rte_manual/oracle/contract.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing contract.i (no preprocessing)
-[rte] annotating function f
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function main
/* Generated by Frama-C */
/*@ ensures \result ≡ -\old(x);
diff --git a/tests/rte_manual/oracle/div.res.oracle b/tests/rte_manual/oracle/div.res.oracle
index df7adc017f98c1e2352375018620a29de7c2a1a1..9c30f35bd7a986610bd83beb631964953fb6b389 100644
--- a/tests/rte_manual/oracle/div.res.oracle
+++ b/tests/rte_manual/oracle/div.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing div.i (no preprocessing)
-[rte] annotating function f
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function main
/* Generated by Frama-C */
void f(void)
{
diff --git a/tests/rte_manual/oracle/float.res.oracle b/tests/rte_manual/oracle/float.res.oracle
index 5737697a89396744b6c2811429a02408ccf9e8eb..0eb2d2a7244fec174f641a8a601440fd8df1b63f 100644
--- a/tests/rte_manual/oracle/float.res.oracle
+++ b/tests/rte_manual/oracle/float.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing float.i (no preprocessing)
-[rte] annotating function f
+[rte:annot] annotating function f
/* Generated by Frama-C */
int f(float v)
{
diff --git a/tests/rte_manual/oracle/machdep.0.res.oracle b/tests/rte_manual/oracle/machdep.0.res.oracle
index 3c1069aa8095bf8831926d5274f23c321bd26880..d84215d30228b99aa1db7c1bb7127083d4e0c456 100644
--- a/tests/rte_manual/oracle/machdep.0.res.oracle
+++ b/tests/rte_manual/oracle/machdep.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing machdep.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/rte_manual/oracle/machdep.1.res.oracle b/tests/rte_manual/oracle/machdep.1.res.oracle
index 74946953da3711d60266a3e191a08363df09fa52..5db9c840ed42d84e9a1028c062ef2abcca45b623 100644
--- a/tests/rte_manual/oracle/machdep.1.res.oracle
+++ b/tests/rte_manual/oracle/machdep.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing machdep.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/rte_manual/oracle/memaccess.res.oracle b/tests/rte_manual/oracle/memaccess.res.oracle
index 1ba252075fb0c7bbcebc294802915d0b563a8fa5..1ca686c508ea9e99f381f4f564fef7f23a08b92b 100644
--- a/tests/rte_manual/oracle/memaccess.res.oracle
+++ b/tests/rte_manual/oracle/memaccess.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing memaccess.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int i;
unsigned int j;
diff --git a/tests/rte_manual/oracle/safearrays.res.oracle b/tests/rte_manual/oracle/safearrays.res.oracle
index d0e564f54450238f72df9a33e55ef7eeac0eca7f..b982303c294a0067c75255af09d18737e0f28d0e 100644
--- a/tests/rte_manual/oracle/safearrays.res.oracle
+++ b/tests/rte_manual/oracle/safearrays.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing safearrays.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
struct S {
int val ;
diff --git a/tests/rte_manual/oracle/signed_downcast.0.res.oracle b/tests/rte_manual/oracle/signed_downcast.0.res.oracle
index 1b702b574aaceec554254bc80db4d4add37e4279..3f02e092cbed16d35c7888b0d15f0224312c95f5 100644
--- a/tests/rte_manual/oracle/signed_downcast.0.res.oracle
+++ b/tests/rte_manual/oracle/signed_downcast.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing signed_downcast.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/rte_manual/oracle/signed_downcast.1.res.oracle b/tests/rte_manual/oracle/signed_downcast.1.res.oracle
index f1ac2e75441bdaa1946970b2dc8c5c11e3bea979..802d1a3345d1ee0dd3580278c62f81c18c1850be 100644
--- a/tests/rte_manual/oracle/signed_downcast.1.res.oracle
+++ b/tests/rte_manual/oracle/signed_downcast.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing signed_downcast.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/rte_manual/oracle/unary_minus.res.oracle b/tests/rte_manual/oracle/unary_minus.res.oracle
index 56c6a3b2ab69186e711315890227edcd7f667498..447788fa86b93e91d22d1c0c5d593edbf072e301 100644
--- a/tests/rte_manual/oracle/unary_minus.res.oracle
+++ b/tests/rte_manual/oracle/unary_minus.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing unary_minus.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
int main(void)
{
diff --git a/tests/rte_manual/oracle/unsigned.0.res.oracle b/tests/rte_manual/oracle/unsigned.0.res.oracle
index d5516362ef8f1d8c13e4e101c3b3927db066164a..533f554133cc5501a14980a55f2b181e008689ab 100644
--- a/tests/rte_manual/oracle/unsigned.0.res.oracle
+++ b/tests/rte_manual/oracle/unsigned.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing unsigned.i (no preprocessing)
-[rte] annotating function f
+[rte:annot] annotating function f
/* Generated by Frama-C */
unsigned int f(unsigned int a, unsigned int b)
{
diff --git a/tests/rte_manual/oracle/unsigned.1.res.oracle b/tests/rte_manual/oracle/unsigned.1.res.oracle
index 1c752a84252eb6a372d5f442069f406ed9eda340..60fae9d9db15dad80b26d4298d4e43f64fd56853 100644
--- a/tests/rte_manual/oracle/unsigned.1.res.oracle
+++ b/tests/rte_manual/oracle/unsigned.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing unsigned.i (no preprocessing)
-[rte] annotating function f
+[rte:annot] annotating function f
/* Generated by Frama-C */
unsigned int f(unsigned int a, unsigned int b)
{
diff --git a/tests/rte_manual/oracle/unsigned_downcast.res.oracle b/tests/rte_manual/oracle/unsigned_downcast.res.oracle
index b8f476d5ae7de334235015af441040671c7a20e6..3b440cc2743cb396018f94441b2f8b990ebe1daf 100644
--- a/tests/rte_manual/oracle/unsigned_downcast.res.oracle
+++ b/tests/rte_manual/oracle/unsigned_downcast.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing unsigned_downcast.i (no preprocessing)
-[rte] annotating function f
+[rte:annot] annotating function f
/* Generated by Frama-C */
unsigned char f(int a, int b)
{
diff --git a/tests/syntax/oracle/char_is_unsigned.res.oracle b/tests/syntax/oracle/char_is_unsigned.res.oracle
index cda585a0ee04d21af96c30758401fdc4b7c3c4b2..5486dee5ffefeb44b565c80c0799da3021a9b204 100644
--- a/tests/syntax/oracle/char_is_unsigned.res.oracle
+++ b/tests/syntax/oracle/char_is_unsigned.res.oracle
@@ -10,7 +10,7 @@ void main(void)
[kernel] Parsing char_is_unsigned.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
/* Generated by Frama-C */
char t[10];
void main(void)
diff --git a/tests/value/oracle/div.1.res.oracle b/tests/value/oracle/div.1.res.oracle
index 0410d4b23f408be62d1b069ae28107b86c9c52b0..14acaa30f17add47b1c80dc39a18c1e6821795d5 100644
--- a/tests/value/oracle/div.1.res.oracle
+++ b/tests/value/oracle/div.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing div.i (no preprocessing)
-[rte] annotating function main
+[rte:annot] annotating function main
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/value/oracle/memexec.res.oracle b/tests/value/oracle/memexec.res.oracle
index 511142198071bebc75f405479ef9cf3727aa14b1..25be30c2f1d4750d002bdca947d2cf5702ae85e8 100644
--- a/tests/value/oracle/memexec.res.oracle
+++ b/tests/value/oracle/memexec.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing memexec.c (with preprocessing)
-[rte] annotating function fbug
+[rte:annot] annotating function fbug
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/value/oracle/precond2.0.res.oracle b/tests/value/oracle/precond2.0.res.oracle
index 6b8ad90cb927b0c71e29751dc61f0a75149e1a23..10ee7cb691c71c333a96e0b869b71de6781c3e6c 100644
--- a/tests/value/oracle/precond2.0.res.oracle
+++ b/tests/value/oracle/precond2.0.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing precond2.c (with preprocessing)
-[rte] annotating function f
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function main
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
diff --git a/tests/value/oracle/precond2.1.res.oracle b/tests/value/oracle/precond2.1.res.oracle
index 67f7eb22cc8357658ae476e157df49bc86a33825..ff415fa2c9b324a73cad48fbd8cc4917553d342a 100644
--- a/tests/value/oracle/precond2.1.res.oracle
+++ b/tests/value/oracle/precond2.1.res.oracle
@@ -35,8 +35,8 @@
x ∈ {1}
[eva:final-states] Values at end of function main:
x ∈ {0; 1}
-[rte] annotating function f
-[rte] annotating function main
+[rte:annot] annotating function f
+[rte:annot] annotating function main
[report] Computing properties status...
--------------------------------------------------------------------------------
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index 0c3ad90376e8a418941025c371f3e29537a8b190..6faede6c061bc435ba56fa292654caf779bf975c 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -1,13 +1,13 @@
[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel.
Please use -eva-slevel instead.
[kernel] Parsing summary.i (no preprocessing)
-[rte] annotating function alarms
-[rte] annotating function bottom
+[rte:annot] annotating function alarms
+[rte:annot] annotating function bottom
[rte] summary.i:15: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
-[rte] annotating function dead
-[rte] annotating function logic
-[rte] annotating function main
-[rte] annotating function minimal
+[rte:annot] annotating function dead
+[rte:annot] annotating function logic
+[rte:annot] annotating function main
+[rte:annot] annotating function minimal
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed