diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 9f341167868e2dd8410ae0732d5e535715442df5..01bc1e874089cd8f19a425740ebe452294b33951 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -7,6 +7,8 @@
- [Yannick] Logic functions
- [Nikola颹 temporal memory properties
- memory profiling
+- [Guillaume] ajouter les annotations de RTE dans la table des annotations
+ (avec une option)
#####################
# E-ACSL CONSTRUCTS #
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
index 34479ee8fd84f3691c321b0fbeb6271992095485..dc45740ff8480f1a3a9dae7c3d501cefaf32c0cb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
@@ -90,10 +90,10 @@ int main(void)
int __e_acsl_valid;
__initialize((void *)P,sizeof(int));
__e_acsl_valid_read = __valid_read((void *)P,sizeof(int));
- e_acsl_assert(__e_acsl_valid_read,(char *)"Assertion",(char *)"main",
+ e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(P)",16);
__e_acsl_valid = __valid((void *)P,sizeof(int));
- e_acsl_assert(__e_acsl_valid,(char *)"Assertion",(char *)"main",
+ e_acsl_assert(__e_acsl_valid,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid(P)",16);
(*P) ++;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
index 2b5100d6236a25d3514d173528bf4c2f1c41c363..08dae00e205b4d88c3b7ca498aa12dea4472efb7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
@@ -102,10 +102,10 @@ int main(void)
int __e_acsl_valid;
__initialize((void *)P,sizeof(int));
__e_acsl_valid_read = __valid_read((void *)P,sizeof(int));
- e_acsl_assert(__e_acsl_valid_read,(char *)"Assertion",(char *)"main",
+ e_acsl_assert(__e_acsl_valid_read,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(P)",16);
__e_acsl_valid = __valid((void *)P,sizeof(int));
- e_acsl_assert(__e_acsl_valid,(char *)"Assertion",(char *)"main",
+ e_acsl_assert(__e_acsl_valid,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid(P)",16);
(*P) ++;
}
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 50ebd5558d79cf55824362d9ee840b72a5e70a40..568bc13d485a2454aff21419c3ef4ea60f3d995a 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -637,9 +637,10 @@ and named_predicate_to_exp ?name kf ?rte env p =
let env = if rte then translate_rte kf env e else env in
e, env
-and translate_rte kf env e =
- let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
- let l = get_rte kf stmt e in
+and translate_rte_annots:
+ 'a. (Format.formatter -> 'a -> unit) -> 'a ->
+ kernel_function -> Env.t -> code_annotation list -> Env.t =
+ fun pp elt kf env l ->
let old_valid = !is_visiting_valid in
let old_kind = Env.annotation_kind env in
let env = Env.set_annotation_kind env Misc.RTE in
@@ -649,8 +650,7 @@ and translate_rte kf env e =
| AAssert(_, p) ->
handle_error
(fun env ->
- Options.feedback ~dkey ~level:4 "prevent RTE from %a"
- Printer.pp_exp e;
+ Options.feedback ~dkey ~level:4 "prevent RTE from %a" pp elt;
translate_named_predicate kf (Env.rte env false) p)
env
| _ -> assert false)
@@ -660,6 +660,11 @@ and translate_rte kf env e =
is_visiting_valid := old_valid;
Env.set_annotation_kind env old_kind
+and translate_rte kf env e =
+ let stmt = Cil.mkStmtOneInstr ~valid_sid:true (Skip e.eloc) in
+ let l = get_rte kf stmt e in
+ translate_rte_annots Printer.pp_exp e kf env l
+
and translate_named_predicate kf env p =
Options.feedback ~dkey ~level:3 "translating predicate %a"
Printer.pp_predicate_named p;
diff --git a/src/plugins/e-acsl/translate.mli b/src/plugins/e-acsl/translate.mli
index f8ac91db35f47375d88d76c9c478d87beb037fa8..dca783d90e3d7707063eb21c778ba6711ed56503 100644
--- a/src/plugins/e-acsl/translate.mli
+++ b/src/plugins/e-acsl/translate.mli
@@ -35,6 +35,14 @@ val translate_post_code_annotation:
val translate_named_predicate:
kernel_function -> Env.t -> predicate named -> Env.t
+val translate_rte_annots:
+ (Format.formatter -> 'a -> unit) ->
+ 'a ->
+ kernel_function ->
+ Env.t ->
+ code_annotation list ->
+ Env.t
+
val predicate_to_exp: kernel_function -> predicate named -> exp
val set_original_project: Project.t -> unit
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 1bb2874ea2c024a9607b47349e15984c8d333b14..3902c6e387b1cbb2b52e5aba49a4f9187502c6dd 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -460,13 +460,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
stmt.ghost <- false;
(* translate potential RTEs of ghost code *)
let rtes = get_rte_by_stmt kf stmt in
- List.fold_left
- (fun env a -> match a.annot_content with
- | AAssert(_, p) ->
- Translate.translate_named_predicate kf (Env.rte env false) p
- | _ -> assert false)
- env
- rtes
+ Translate.translate_rte_annots Printer.pp_stmt stmt kf env rtes
end else
env
in
@@ -522,11 +516,11 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
let b, env =
Env.pop_and_get env stmt ~global_clear:true Env.After
in
- if is_main && Pre_analysis.use_model () && generate then begin
+ if is_main && Pre_analysis.use_model () then begin
let stmts = b.bstmts in
let l = List.rev stmts in
match l with
- | [] -> assert false (* return is here *)
+ | [] -> assert false (* at least the 'return' stmt *)
| ret :: l ->
let loc = Stmt.loc stmt in
let delete_stmts =
@@ -548,7 +542,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
new_stmt, env
else
stmt, env
- else
+ else (* i.e. not (is_return stmt) *)
if generate then
let stmt = rename_alloc_function stmt in
(* must generate [pre_block] which includes [stmt] before generating