From 1b9588f9ff44e15d2d866db44052152467acba70 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Fri, 4 Dec 2015 16:13:34 +0100
Subject: [PATCH] Replace keep_initialiser mutable variable (which used to
decide to keep global initialisers or not) with a boolean switch called
is_initialiser used to detect and filter out compound initialisers and update
[global_vars] mapping
---
src/plugins/e-acsl/visit.ml | 44 ++++++++++++++++++-------------------
1 file changed, 21 insertions(+), 23 deletions(-)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 8bb5b69801a..88e175ee105 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -83,7 +83,9 @@ class e_acsl_visitor prj generate = object (self)
[None] while the global corresponding to this fundec has not been
visited *)
- val mutable keep_initializer = None
+ val mutable is_initializer = false
+ (* Global flag set to a [true] value if a currently visited node
+ belongs to a global initialiser and set to [false] otherwise *)
val global_vars: init option Varinfo.Hashtbl.t = Varinfo.Hashtbl.create 7
(* A hashtable mapping global variables (as Cil_type.varinfo) to their
@@ -335,22 +337,29 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
(match g with
| GVar(vi, _, _) | GVarDecl(vi, _) ->
- Varinfo.Hashtbl.replace global_vars vi None
+ Varinfo.Hashtbl.add global_vars vi None
| _ -> ());
if generate then Cil.DoChildrenPost(fun g -> List.iter do_it g; g)
else Cil.DoChildren
- method !vinit vi _off _i =
+ (* Process global variable initialisers and add mappings from global
+ variables to their initialisers to [global_vars]. Note that [add] method
+ should be used instead [replace]. This is because a single variable can
+ be assicoated with multiple initialisers and all of them need to be
+ captured. Also note that the below function captures only [SingleInit]s.
+ All compound initialisers (which contain single ones) are unrapped and
+ thrown away. *)
+ method !vinit vi _off _i =
if generate then
if Mmodel_analysis.must_model_vi vi then begin
- keep_initializer <- Some true;
+ is_initializer <- true;
Cil.DoChildrenPost
- (fun i ->
- (match keep_initializer with
- | Some false -> Varinfo.Hashtbl.replace global_vars vi (Some i)
- | Some true | None -> ());
- keep_initializer <- None;
- i)
+ (fun i ->
+ (match is_initializer with
+ | true -> Varinfo.Hashtbl.add global_vars vi (Some i)
+ | false-> ());
+ is_initializer <- false;
+ i)
end else
Cil.JustCopy
else
@@ -704,20 +713,9 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
if generate then Cil.DoChildrenPost handle_memory else Cil.DoChildren
- method !vexpr exp =
+ method !vexpr _ =
if generate then
- match keep_initializer with
- | Some false -> Cil.JustCopy
- | Some true ->
- let keep = match exp.enode with Const(CStr _) -> false | _ -> true in
- keep_initializer <- Some keep;
- if keep then Cil.DoChildren else Cil.JustCopy
- | None ->
- Cil.DoChildrenPost
- (fun e ->
- let e, env = self#literal_string !function_env e in
- function_env := env;
- e)
+ Cil.DoChildren
else
Cil.SkipChildren
--
GitLab