From 355b49dbab836b24bd51a2fbae562eb73fa24526 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 5 Jul 2018 10:33:20 +0200
Subject: [PATCH] Favor standard visitor mechanism for updating gotos
labels.ml was broken since quite some time.
---
src/plugins/e-acsl/label.ml | 21 +++++----------------
src/plugins/e-acsl/visit.ml | 8 +++++++-
2 files changed, 12 insertions(+), 17 deletions(-)
diff --git a/src/plugins/e-acsl/label.ml b/src/plugins/e-acsl/label.ml
index 73d143221fc..9887ef2a37a 100644
--- a/src/plugins/e-acsl/label.ml
+++ b/src/plugins/e-acsl/label.ml
@@ -51,22 +51,11 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
inherit Visitor.frama_c_inplace
(* 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, loc), Goto(orig_ref, _) ->
- if Cil_datatype.Stmt.equal !s_ref old then
- if s_ref == orig_ref then
- (* The memo_stmt and its origin [orig_stmt] contain a shared
- reference because [orig_stmt] has not yet been visited by [vis]
- (forward goto). Consequently, do not modify the ref directly but
- replace the corresponding stmt in the memoisation table. When
- [orig_stmt] will be visited, the visitor will automatically
- substitute it with the updated stmt. *)
- Cil.set_stmt vis#behavior
- orig_stmt
- { s with skind = Goto(ref new_stmt, loc) }
- else
- (* Backward goto: it has already been visited and there is no more
- sharing. Directly update the reference. *)
- s_ref := new_stmt;
+ | 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. *)
+ s_ref := new_stmt;
Cil.SkipChildren
| _ -> Cil.DoChildren
(* improve efficiency: skip childrens which cannot contain any label *)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 75debee5e06..c2c928a4161 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -623,6 +623,9 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
(* handle loop invariants *)
let new_stmt, env, must_mv = Loops.preserve_invariant prj env kf stmt in
+ let orig = Cil.get_original_stmt self#behavior stmt in
+ Cil.set_orig_stmt self#behavior new_stmt orig;
+ Cil.set_stmt self#behavior orig new_stmt;
let new_stmt, env =
(* Remove local variables which scopes ended via goto/break/continue. *)
let del_vars = Exit_points.delete_vars stmt in
@@ -708,13 +711,16 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Env.Before
in
let post_block =
- if post_block.blocals = [] then Cil.transient_block post_block
+ if post_block.blocals = [] && new_stmt.labels = []
+ then Cil.transient_block post_block
else post_block
in
let res = Misc.mk_block prj new_stmt post_block in
if not (Cil_datatype.Stmt.equal new_stmt res) then
E_acsl_label.move (self :> Visitor.generic_frama_c_visitor)
new_stmt res;
+ Cil.set_stmt self#behavior orig res;
+ Cil.set_orig_stmt self#behavior res orig;
res, env
end else
stmt, env
--
GitLab