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