From 1157b7165fe68908400cf2fe10acc3e84e31a1c7 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Thu, 5 Sep 2013 14:22:54 +0000
Subject: [PATCH] [E-ACSL] code factorisation which improves translation of
ghost stmts
---
src/plugins/e-acsl/TODO | 2 ++
.../tests/e-acsl-runtime/oracle/gen_ghost.c | 4 ++--
.../tests/e-acsl-runtime/oracle/gen_ghost2.c | 4 ++--
src/plugins/e-acsl/translate.ml | 15 ++++++++++-----
src/plugins/e-acsl/translate.mli | 8 ++++++++
src/plugins/e-acsl/visit.ml | 14 ++++----------
6 files changed, 28 insertions(+), 19 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 9f341167868..01bc1e87408 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 34479ee8fd8..dc45740ff84 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 2b5100d6236..08dae00e205 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 50ebd5558d7..568bc13d485 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 f8ac91db35f..dca783d90e3 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 1bb2874ea2c..3902c6e387b 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
--
GitLab