From 8e432fc36b32c4cea88aadfffec502f1b474b45f Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Fri, 4 Dec 2015 15:24:03 +0100
Subject: [PATCH] Disable functionality that removes initilisers from global
variables
---
src/plugins/e-acsl/visit.ml | 14 ++------------
1 file changed, 2 insertions(+), 12 deletions(-)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 3c214f36400..84f6ff220a2 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
--
GitLab