From 6b73d17c99e03501c8deb23fc5b2cc0728b42b51 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Mon, 15 May 2017 16:21:07 +0200
Subject: [PATCH] Track offset in global vars (prereq. to temporal analysis)
---
src/plugins/e-acsl/visit.ml | 23 +++++++++++++++--------
1 file changed, 15 insertions(+), 8 deletions(-)
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 2bfb8b9f0af..046ee11ff6f 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -111,7 +111,8 @@ class e_acsl_visitor prj generate = object (self)
(* Global flag set to [true] if a currently visited node
belongs to a global initializer and set to [false] otherwise *)
- val global_vars: init option Varinfo.Hashtbl.t = Varinfo.Hashtbl.create 7
+ val global_vars: (offset * init option) Varinfo.Hashtbl.t =
+ Varinfo.Hashtbl.create 7
(* Hashtable mapping global variables (as Cil_type.varinfo) to their
initializers aiming to capture memory allocated by global variable
declarations and initialization. At runtime the memory blocks
@@ -150,7 +151,7 @@ class e_acsl_visitor prj generate = object (self)
||
try
Varinfo.Hashtbl.iter
- (fun old_vi i -> match i with None | Some _ ->
+ (fun old_vi (_, i) -> match i with None | Some _ ->
if Mmodel_analysis.must_model_vi old_vi then raise Exit)
global_vars;
false
@@ -166,7 +167,7 @@ class e_acsl_visitor prj generate = object (self)
let env = Env.push !function_env in
let stmts, env =
Varinfo.Hashtbl.fold_sorted
- (fun old_vi i (stmts, env) ->
+ (fun old_vi (_, i) (stmts, env) ->
let new_vi = Cil.get_varinfo self#behavior old_vi in
(* [model] creates an initialization statement
of the form [__e_acsl_full_init(...)] for every global
@@ -375,15 +376,16 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(* Make a unique mapping for each global variable omitting initializers.
Initializers (used to capture literal strings) are added to
[global_vars] via the [vinit] visitor method (see comments below). *)
- Varinfo.Hashtbl.replace global_vars vi None
+ Varinfo.Hashtbl.replace global_vars vi (NoOffset, None)
| _ -> ());
if generate then Cil.DoChildrenPost(fun g -> List.iter do_it g; g)
else Cil.DoChildren
(* Add mappings from global variables to their initializers in [global_vars].
Note that the below function captures only [SingleInit]s. All compound
- initializers (which contain single ones) are unrapped and thrown away. *)
- method !vinit vi _off _i =
+ initializers containing SingleInits (except for empty compound
+ initializers) are unrapped and thrown away. *)
+ method !vinit vi off _ =
if generate then
if Mmodel_analysis.must_model_vi vi then begin
is_initializer <- vi.vglob;
@@ -393,7 +395,12 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(* Note the use of [add] instead of [replace]. This is because a
single variable can be associated with multiple initializers
and all of them need to be captured. *)
- | true -> Varinfo.Hashtbl.add global_vars vi (Some i)
+ | true ->
+ (match i with
+ (* Case of an empty CompoundInit, treat it as if there were
+ * no initializer at all *)
+ | CompoundInit(_,[]) -> ()
+ | _ -> Varinfo.Hashtbl.add global_vars vi (off, (Some i)))
| false-> ());
is_initializer <- false;
i)
@@ -637,7 +644,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
let loc = Stmt.loc stmt in
let delete_stmts =
Varinfo.Hashtbl.fold_sorted
- (fun old_vi i acc ->
+ (fun old_vi (_, i) acc ->
if Mmodel_analysis.must_model_vi old_vi then
let new_vi = Cil.get_varinfo self#behavior old_vi in
(* Since there are multiple entries for same variables
--
GitLab