diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml index 3c214f3640056e138a477ad0e10b0a1a9673ca2f..84f6ff220a2f010c70318300f1f6b325b46e085a 100644 --- a/src/plugins/e-acsl/visit.ml +++ b/src/plugins/e-acsl/visit.ml @@ -322,18 +322,8 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]" if generate then Cil.JustCopy else Cil.SkipChildren | g -> let do_it = function - | GVar(vi, i, _) -> - vi.vghost <- false; - (* remove initializers on need *) - if Mmodel_analysis.old_must_model_vi self#behavior vi then begin - try - let old_vi = Cil.get_original_varinfo self#behavior vi in - match Varinfo.Hashtbl.find global_vars old_vi with - | None -> () - | Some _ -> i.init <- None - with Not_found -> - assert false - end + | GVar(vi, _, _) -> + vi.vghost <- false; () | GFun({ svar = vi } as fundec, _) -> vi.vghost <- false; (* remember that we have to remove the main later (see method