diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml index 35abd18a12bd9a6b316df95e98835ddb919024ff..5af377d2bf8484231e8e6de63643b8087b27b2e7 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 ();