From 762ba955e5274cde5ccf690af32863df40858acf Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 4 Jul 2018 18:26:03 +0200
Subject: [PATCH] Fixes issues in updating labels and gotos during
instrumentation
Label.move must compare goto targets to the statement in the original
AST, not its copy. Furthermore moving labels must only be done if we
are about to change the target of the gotos, not if we use the
statement as generated by the plain visitor.
---
src/plugins/e-acsl/label.ml | 1 +
src/plugins/e-acsl/visit.ml | 10 ++++++----
2 files changed, 7 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/label.ml b/src/plugins/e-acsl/label.ml
index a08b50fe796..73d143221fc 100644
--- a/src/plugins/e-acsl/label.ml
+++ b/src/plugins/e-acsl/label.ml
@@ -44,6 +44,7 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
| _ :: _ ->
old.labels <- [];
new_stmt.labels <- labels @ new_stmt.labels;
+ let old = Cil.get_original_stmt vis#behavior old in
Labeled_stmts.add old new_stmt;
(* update the gotos of the function jumping to one of the labels *)
let o orig_stmt = object
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 1d570d703fd..05cf6dfdf12 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -678,10 +678,12 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
b.bstmts <- List.rev l @ delete_stmts
end;
let new_stmt = Misc.mk_block prj stmt b in
- (* move the labels of the return to the new block in order to
- evaluate the postcondition when jumping to them. *)
- E_acsl_label.move
- (self :> Visitor.generic_frama_c_visitor) stmt new_stmt;
+ if not (Cil_datatype.Stmt.equal stmt new_stmt) then begin
+ (* move the labels of the return to the new block in order to
+ evaluate the postcondition when jumping to them. *)
+ E_acsl_label.move
+ (self :> Visitor.generic_frama_c_visitor) stmt new_stmt
+ end;
new_stmt, env
else
stmt, env
--
GitLab