From 0561a0350828fe5e8becb6d74eefe4b7572c81d2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 5 Jul 2018 16:34:41 +0200
Subject: [PATCH] Avoid messing up with visitor correspondance tables
---
src/plugins/e-acsl/label.ml | 6 +++---
src/plugins/e-acsl/translate.ml | 3 +--
src/plugins/e-acsl/visit.ml | 25 +------------------------
3 files changed, 5 insertions(+), 29 deletions(-)
diff --git a/src/plugins/e-acsl/label.ml b/src/plugins/e-acsl/label.ml
index 9887ef2a37a..89949e3c727 100644
--- a/src/plugins/e-acsl/label.ml
+++ b/src/plugins/e-acsl/label.ml
@@ -52,9 +52,9 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
(* invariant of this method: [s = Cil.memo_stmt vis#behavior orig_stmt] *)
method !vstmt_aux s = match s.skind, orig_stmt.skind with
| Goto(s_ref, _), Goto(orig_ref, _) ->
- if Cil_datatype.Stmt.equal !s_ref old && s_ref != orig_ref then
- (* Forward goto: it has already been visited and there is no more
- sharing. Must update the reference. *)
+ if Cil_datatype.Stmt.equal !orig_ref old && s_ref != orig_ref then
+ (* Forward goto: it has already been visited.
+ We must update the reference. *)
s_ref := new_stmt;
Cil.SkipChildren
| _ -> Cil.DoChildren
diff --git a/src/plugins/e-acsl/translate.ml b/src/plugins/e-acsl/translate.ml
index 9726a521bee..db194ddf24c 100644
--- a/src/plugins/e-acsl/translate.ml
+++ b/src/plugins/e-acsl/translate.ml
@@ -663,8 +663,7 @@ and at_to_exp env t_opt label e =
end
in
let bhv = Env.get_behavior new_env in
- let new_stmt = Visitor.visitFramacStmt o (Cil.get_stmt bhv stmt) in
- Cil.set_stmt bhv stmt new_stmt;
+ ignore( Visitor.visitFramacStmt o (Cil.get_stmt bhv stmt));
res, !env_ref, false
and env_of_li li kf env loc =
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index c2c928a4161..a65afdce47a 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -742,15 +742,13 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
let must_model = Mmodel_analysis.must_model_lval ~stmt ~kf lv in
if not (may_safely_ignore lv) && must_model then
- let before = Cil.memo_stmt self#behavior stmt in
+ let before = Cil.mkStmt stmt.skind in
let new_stmt = Project.on prj (Misc.mk_initialize ~loc) lv in
- let new_stmt = Cil.memo_stmt self#behavior new_stmt in
let env = Env.add_stmt ~post ~before env new_stmt in
let env = match vi with
| None -> env
| Some vi ->
let new_stmt = Project.on prj Misc.mk_store_stmt vi in
- let new_stmt = Cil.memo_stmt self#behavior new_stmt in
Env.add_stmt ~post ~before env new_stmt
in
env
@@ -891,27 +889,6 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
end else
Cil.SkipChildren
- method !vterm _ =
- Cil.DoChildrenPost
- (fun t ->
- (match t.term_node with
- | Tat(_, StmtLabel s_ref) ->
- (* the label may have been moved,
- so move the corresponding reference *)
- s_ref := E_acsl_label.new_labeled_stmt !s_ref
- | _ -> ());
- t)
-
- method !vpredicate_node _ =
- Cil.DoChildrenPost
- (function
- | Pat(_, StmtLabel s_ref) as p ->
- (* the label may have been moved,
- so move the corresponding reference *)
- s_ref := E_acsl_label.new_labeled_stmt !s_ref;
- p
- | p -> p);
-
initializer
Misc.reset ();
Literal_strings.reset ();
--
GitLab