From 8f835658f95585eb9141a5115099187de4ed7d11 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 26 Mar 2014 15:38:41 +0100
Subject: [PATCH] handle predicates \at in the same way than terms \at
---
src/plugins/e-acsl/visit.ml | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index ea467c114ee..db138683823 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -636,10 +636,22 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(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 _ =
+ 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 ();
self#reset_env ();
--
GitLab