diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index fa8bd1e797a12f25e05eda59fe46d2c0c9947551..5a5f88fc82d42bddef0c71ad0bd83df0a3ec5a93 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -137,10 +137,10 @@ let build_node_kind ~is_folded_base lval location =
Scalar (vi, typ, offset')
with Bit_utils.NoMatchingOffset | Ival.Not_Singleton_Int ->
(* TODO: handle Bit_utils.NoMatchingOffset (strict aliasing ?) *)
- Scattered (lval)
+ Scattered (lval, location)
end
| None ->
- Scattered (lval)
+ Scattered (lval, location)
let default_node_locality callstack =
match callstack with
@@ -171,23 +171,19 @@ let build_node_locality callstack node_kind =
(* --- Context object --- *)
module NodeRef = Datatype.Pair_with_collections
- (Locations.Location) (Callstack)
+ (Node_kind) (Callstack)
(struct let module_name = "Build.NodeRef" end)
module Graph = Imprecision_graph
-module VertexTable = Datatype.Int.Hashtbl
+module Index = Datatype.Int.Hashtbl
module NodeTable = FCHashtbl.Make (NodeRef)
-module FileTable = Datatype.String.Hashtbl
-module CallstackTable = Value_types.Callstack.Hashtbl
module BaseSet = Cil_datatype.Varinfo.Set
module FunctionMap = Kernel_function.Map
type t = {
mutable graph: Graph.t;
- mutable vertex_table: node VertexTable.t;
+ mutable vertex_table: node Index.t;
mutable node_table: node NodeTable.t;
- mutable file_table: node FileTable.t;
- mutable callstack_table: node CallstackTable.t;
mutable unfolded_bases: BaseSet.t;
mutable hidden_bases: BaseSet.t;
mutable focus: bool FunctionMap.t;
@@ -195,10 +191,18 @@ type t = {
mutable graph_diff: graph_diff;
}
+let is_folded context vi =
+ not (BaseSet.mem vi context.unfolded_bases)
+
+let is_hidden context node_kind =
+ match Node_kind.get_base node_kind with
+ | Some vi when BaseSet.mem vi context.hidden_bases -> true
+ | _ -> false
+
let get_node context node_key =
- VertexTable.find context.vertex_table node_key
+ Index.find context.vertex_table node_key
-let update_node context node =
+let update_node context node =
if
not (List.exists (Graph.Node.equal node) context.graph_diff.added_nodes)
then
@@ -208,47 +212,26 @@ let update_node context node =
}
let add_node context ~node_kind ~node_locality =
- let node = Graph.create_node context.graph ~node_kind ~node_locality in
- VertexTable.add context.vertex_table node.node_key node;
- update_node context node;
- node
+ let node_ref = (node_kind, node_locality.loc_callstack) in
+ let add_new _ =
+ let node = Graph.create_node context.graph ~node_kind ~node_locality in
+ node.node_hidden <- is_hidden context node.node_kind;
+ Index.add context.vertex_table node.node_key node;
+ update_node context node;
+ node
+ in
+ NodeTable.memo context.node_table node_ref add_new
-let _remove_node context node =
+let remove_node context node =
+ let node_ref = (node.node_kind, node.node_locality.loc_callstack) in
Graph.remove_node context.graph node;
- VertexTable.remove context.vertex_table node.node_key;
+ Index.remove context.vertex_table node.node_key;
+ NodeTable.remove context.node_table node_ref;
context.graph_diff <- {
context.graph_diff with
removed_nodes = node :: context.graph_diff.removed_nodes
}
-let reference_node_locality context node_locality =
- let { loc_file ; loc_callstack } = node_locality in
- let rec add_file _ =
- let node_locality = { node_locality with loc_callstack = [] } in
- add_node context ~node_kind:Cluster ~node_locality
- and add_callstack = function
- | [] -> assert false
- | _ :: t as loc_callstack ->
- let node_locality = { node_locality with loc_callstack } in
- if t <> [] then
- ignore (CallstackTable.memo context.callstack_table t add_callstack);
- add_node context ~node_kind:Cluster ~node_locality
- in
- match loc_callstack with
- | [] ->
- ignore (FileTable.memo context.file_table loc_file add_file)
- | cs ->
- ignore (CallstackTable.memo context.callstack_table cs add_callstack)
-
-
-let is_folded context vi =
- not (BaseSet.mem vi context.unfolded_bases)
-
-let is_hidden context node_kind =
- match Node_kind.get_base node_kind with
- | Some vi when BaseSet.mem vi context.hidden_bases -> true
- | _ -> false
-
(* --- Graph building --- *)
@@ -256,24 +239,8 @@ let is_hidden context node_kind =
let build_node context callstack location lval =
let is_folded_base = is_folded context in
let node_kind = build_node_kind ~is_folded_base lval location in
- if is_hidden context node_kind then
- None
- else begin
- let node_locality = build_node_locality callstack node_kind in
- reference_node_locality context node_locality;
- let build_new_node _location =
- add_node context ~node_kind ~node_locality
- in
- (* Compute the new location which might have changed after folding *)
- let location' =
- match Node_kind.to_location node_kind with
- | None -> location
- | Some location' -> location'
- in
- let ref = (location', node_locality.loc_callstack) in
- let node = NodeTable.memo context.node_table ref build_new_node in
- Some node
- end
+ let node_locality = build_node_locality callstack node_kind in
+ add_node context ~node_kind ~node_locality
let build_var context callstack varinfo =
let location = Locations.loc_of_varinfo varinfo
@@ -283,11 +250,9 @@ let build_var context callstack varinfo =
let build_lval context callstack kinstr lval =
(* If possible, refine the lval to a non-symbolic one *)
let location = !Db.Value.lval_to_loc kinstr lval in
- match build_node context callstack location lval with
- | None -> None
- | Some node ->
- update_node_values node kinstr lval;
- Some node
+ let node = build_node context callstack location lval in
+ update_node_values node kinstr lval;
+ node
let build_alarm context callstack stmt alarm =
let node_kind = Alarm (stmt,alarm) in
@@ -437,11 +402,9 @@ let build_node_deps context node =
build_exp_deps callstack stmt kind e2
and build_lval_deps callstack stmt kind lval =
- match build_lval context callstack (Kstmt stmt) lval with
- | None -> ()
- | Some dst ->
- let allow_folding = true in
- Graph.create_dependency ~allow_folding context.graph dst kind node
+ let dst = build_lval context callstack (Kstmt stmt) lval in
+ let allow_folding = true in
+ Graph.create_dependency ~allow_folding context.graph dst kind node
in
update_node context node;
@@ -453,7 +416,7 @@ let build_node_deps context node =
| Composite (vi) ->
build_writes_deps callstack (Cil_types.Var vi, Cil_types.NoOffset);
if vi.vformal then build_arg_deps callstack vi
- | Scattered (_lval) -> () (* TODO: implements *)
+ | Scattered (_lval, _location) -> () (* TODO: implements *)
| Alarm (stmt,alarm) ->
build_alarm_deps callstack stmt alarm
| Cluster -> ()
@@ -465,10 +428,8 @@ let create () =
!Db.Value.compute ();
{
graph = Graph.create ();
- vertex_table = VertexTable.create 13;
+ vertex_table = Index.create 13;
node_table = NodeTable.create 13;
- file_table = FileTable.create 13;
- callstack_table = CallstackTable.create 13;
unfolded_bases = BaseSet.empty;
hidden_bases = BaseSet.empty;
focus = FunctionMap.empty;
@@ -478,10 +439,8 @@ let create () =
let clear context =
context.graph <- Graph.create ();
- context.vertex_table <- VertexTable.create 13;
+ context.vertex_table <- Index.create 13;
context.node_table <- NodeTable.create 13;
- context.file_table <- FileTable.create 13;
- context.callstack_table <- CallstackTable.create 13;
context.focus <- FunctionMap.empty;
context.roots <- [];
context.graph_diff <- { added_nodes=[] ; removed_nodes=[] }
@@ -510,22 +469,27 @@ let hide_base context vi =
let unhide_base context vi =
context.hidden_bases <- BaseSet.add vi context.hidden_bases
-let should_auto_explore node =
- match node.node_kind with
- | Scalar _ | Composite _ | Alarm _ -> true
- | Scattered _ | Cluster -> false
-
let explore ~depth context root =
+ let should_auto_explore node =
+ let is_root = Graph.Node.equal node root (* the root is always explored *)
+ and is_intersting_kind = match node.node_kind with
+ | Scalar _ | Composite _ | Alarm _ -> true
+ | Scattered _ | Cluster -> false
+ in
+ is_root || (not node.node_hidden && is_intersting_kind)
+ in
(* Breadth first search *)
let queue : (node * int) Queue.t = Queue.create () in
Queue.add (root,0) queue;
while not (Queue.is_empty queue) do
let (n,d) = Queue.take queue in
if d < depth then begin
- if not (n.node_deps_computed) && should_auto_explore n then begin
+ if not (n.node_deps_computed) && should_auto_explore n then
+ begin
begin try
build_node_deps context n;
with Too_many_deps lval ->
+ (* TODO: give a mean to explore more dependencies *)
Self.warning "Too many dependencies for %a ; throwing them out"
Cil_printer.pp_lval lval;
end;
@@ -542,7 +506,7 @@ let complete_in_depth ~depth context root =
let add_var ?(depth=1) context varinfo =
let callstack = [] in
let node = build_var context callstack varinfo in
- Extlib.may (complete_in_depth ~depth context) node
+ complete_in_depth ~depth context node
let add_lval ?(depth=1) context kinstr lval =
let callstack = match kinstr with
@@ -550,7 +514,7 @@ let add_lval ?(depth=1) context kinstr lval =
| Kstmt stmt -> Callstack.init (Kernel_function.find_englobing_kf stmt)
in
let node = build_lval context callstack kinstr lval in
- Extlib.may (complete_in_depth ~depth context) node
+ complete_in_depth ~depth context node
let add_alarm ?(depth=1) context stmt alarm =
let callstack = Callstack.init (Kernel_function.find_englobing_kf stmt) in
@@ -560,7 +524,36 @@ let add_alarm ?(depth=1) context stmt alarm =
let explore_from_vertex ~depth context node_key =
explore ~depth context (get_node context node_key)
+let show ?(depth=1) context node_key =
+ let node = get_node context node_key in
+ node.node_hidden <- false;
+ explore ~depth context node
+
+let hide context node_key =
+ let node = get_node context node_key in
+ if not node.node_hidden then
+ begin
+ let g = get_graph context in
+ (* Set the node as hidden *)
+ node.node_hidden <- true;
+ (* Remove incomming edges *)
+ let incomming_edges = Graph.pred_e g node in
+ List.iter (Graph.remove_dependency g) incomming_edges;
+ (* Remove disconnected vertices *)
+ let disconnected_nodes = Graph.find_independant_nodes g context.roots in
+ List.iter (remove_node context) disconnected_nodes;
+ (* Dependencies are not there anymore *)
+ node.node_deps_computed <- false;
+ (* Notify node update *)
+ update_node context node
+ end
+
let take_last_differences context =
+ let pp_node fmt n = Format.pp_print_int fmt n.node_key in
+ let pp_node_list = Pretty_utils.pp_list ~sep:",@, " pp_node in
let diff = context.graph_diff in
+ Self.debug ~dkey "added: %a,@, subbed: %a"
+ pp_node_list diff.added_nodes
+ pp_node_list diff.removed_nodes;
context.graph_diff <- { added_nodes=[] ; removed_nodes=[] };
diff
diff --git a/src/plugins/dive/build.mli b/src/plugins/dive/build.mli
index 961dec8856363dcafaa76fa59df6e7cb591e9f05..e3e345a3e8209bf634dbf0dc076e2e82b1f4d165 100644
--- a/src/plugins/dive/build.mli
+++ b/src/plugins/dive/build.mli
@@ -38,4 +38,8 @@ val add_lval : ?depth:int -> t -> Cil_types.kinstr -> Cil_types.lval -> unit
val add_var : ?depth:int -> t -> Cil_types.varinfo -> unit
val add_alarm : ?depth:int -> t -> Cil_types.stmt -> Alarms.alarm -> unit
val explore_from_vertex : depth:int -> t -> int -> unit
+
+val show : ?depth:int -> t -> int -> unit
+val hide : t -> int -> unit
+
val take_last_differences : t -> Graph_types.graph_diff
diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli
index 515bf05c6a45be70b228ed46f2e4b41964575fd8..e8f4943518996149c7bb6a0118e7b0565876892d 100644
--- a/src/plugins/dive/graph_types.mli
+++ b/src/plugins/dive/graph_types.mli
@@ -23,7 +23,7 @@
type node_kind =
| Scalar of Cil_types.varinfo * Cil_types.typ * Cil_types.offset
| Composite of Cil_types.varinfo
- | Scattered of Cil_types.lval
+ | Scattered of Cil_types.lval * Locations.location
| Alarm of Cil_types.stmt * Alarms.alarm
| Cluster (* Dummy node, hack for Ocamlgraph Graphviz Dot module *)
@@ -46,6 +46,7 @@ type node = {
node_key : int;
node_kind : node_kind;
node_locality : node_locality;
+ mutable node_hidden : bool;
mutable node_values : node_values option;
mutable node_deps_computed : bool;
}
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
index 6fee241289eb5e78ebb491057196e26059a8156d..4816eb263b0d48e782f29e9ddab03ab2df0b5f04 100644
--- a/src/plugins/dive/imprecision_graph.ml
+++ b/src/plugins/dive/imprecision_graph.ml
@@ -54,6 +54,7 @@ let create_node ?node_values ~node_kind ~node_locality g =
node_key = !next_key;
node_kind;
node_locality;
+ node_hidden = false;
node_values;
node_deps_computed = false;
}
@@ -112,9 +113,59 @@ let create_dependency ~allow_folding g v1 dependency_kind v2 =
incr next_key;
add_edge_e g (v1,e,v2)
+let remove_dependency g edge =
+ remove_edge_e g edge
+
+
+let find_independant_nodes g roots =
+ let module Dfs = Graph.Traverse.Dfs (struct
+ include G
+ let iter_succ = G.iter_pred
+ let fold_succ = G.fold_pred
+ end)
+ in
+ let module Table = Hashtbl.Make (Node) in
+ let table = Table.create 13 in
+ List.iter (Dfs.prefix_component (fun n -> Table.add table n true) g) roots;
+ let keep_node n =
+ Table.mem table n || n.node_kind = Cluster
+ in
+ fold_vertex (fun n acc -> if keep_node n then acc else n :: acc) g []
+
+
+let add_dummy_nodes g =
+ let module FileTable = Datatype.String.Hashtbl in
+ let module CallstackTable = Value_types.Callstack.Hashtbl in
+ let file_table = FileTable.create 13 in
+ let callstack_table = CallstackTable.create 13 in
+ let g = copy g in
+
+ let create_locality_vertex { node_locality } =
+ let { loc_file ; loc_callstack } = node_locality in
+ let rec add_file _ =
+ let node_locality = { node_locality with loc_callstack = [] } in
+ create_node g ~node_kind:Cluster ~node_locality
+ and add_callstack = function
+ | [] -> assert false
+ | _ :: t as loc_callstack ->
+ let node_locality = { node_locality with loc_callstack } in
+ if t <> [] then
+ ignore (CallstackTable.memo callstack_table t add_callstack);
+ create_node g ~node_kind:Cluster ~node_locality
+ in
+ match loc_callstack with
+ | [] ->
+ ignore (FileTable.memo file_table loc_file add_file)
+ | cs ->
+ ignore (CallstackTable.memo callstack_table cs add_callstack)
+ in
+ iter_vertex create_locality_vertex g;
+ g
+
let ouptput_to_dot out_channel g =
let open Graph.Graphviz.DotAttributes in
+ let g = add_dummy_nodes g in
let build_label s = `HtmlLabel (Extlib.html_escape s) in
diff --git a/src/plugins/dive/imprecision_graph.mli b/src/plugins/dive/imprecision_graph.mli
index 7e1162beb32be99d45313d65ff8c0928be5d7433..890cee867a98922eb840d1927623cd2a020ea6f7 100644
--- a/src/plugins/dive/imprecision_graph.mli
+++ b/src/plugins/dive/imprecision_graph.mli
@@ -44,6 +44,10 @@ val update_node_values : node -> node_values -> unit
val create_dependency : allow_folding:bool -> t -> node -> dependency_kind ->
node -> unit
+val remove_dependency : t -> node * dependency * node -> unit
+
+val find_independant_nodes : t -> node list -> node list
+
val ouptput_to_dot : out_channel -> t -> unit
val ouptput_to_json : out_channel -> t -> unit
diff --git a/src/plugins/dive/node_kind.ml b/src/plugins/dive/node_kind.ml
index 73e3ec50a30b3da17a0f6d02bc8d178b3402c767..396119c63e5ccf6b3a782ffbafe49531f5c646de 100644
--- a/src/plugins/dive/node_kind.ml
+++ b/src/plugins/dive/node_kind.ml
@@ -22,6 +22,70 @@
open Graph_types
+module DatatypeInput =
+struct
+ include Datatype.Undefined
+
+ type t = node_kind
+
+ let (<?>) c (cmp,x,y) =
+ if c = 0
+ then cmp x y
+ else c
+
+ let name = "Node_kind"
+
+ let reprs = [ Cluster ]
+
+ let compare k1 k2 =
+ let open Cil_datatype in
+ match k1, k2 with
+ | Cluster, Cluster -> 0
+ | Cluster, _ -> 1
+ | _, Cluster -> -1
+ | Scalar (vi1, _, offset1), Scalar (vi2, _, offset2) ->
+ Varinfo.compare vi1 vi2 <?> (OffsetStructEq.compare, offset1, offset2)
+ | Scalar _, _ -> 1
+ | _, Scalar _ -> -1
+ | Composite vi1, Composite vi2 -> Varinfo.compare vi1 vi2
+ | Composite _, _ -> 1
+ | _, Composite _ -> -1
+ | Scattered (lv1,loc1), Scattered (lv2,loc2) ->
+ LvalStructEq.compare lv1 lv2 <?> (Locations.Location.compare, loc1, loc2)
+ | Scattered _, _ -> 1
+ | _, Scattered _ -> -1
+ | Alarm (stmt1, alarm1), Alarm (stmt2, alarm2) ->
+ Stmt.compare stmt1 stmt2 <?> (Alarms.compare, alarm1, alarm2)
+
+ let equal k1 k2 =
+ let open Cil_datatype in
+ match k1, k2 with
+ | Cluster, Cluster -> true
+ | Scalar (vi1, _, offset1), Scalar (vi2, _, offset2) ->
+ Varinfo.equal vi1 vi2 && OffsetStructEq.equal offset1 offset2
+ | Composite vi1, Composite vi2 -> Varinfo.equal vi1 vi2
+ | Scattered (lv1, loc1), Scattered (lv2, loc2) ->
+ LvalStructEq.equal lv1 lv2 && Locations.Location.equal loc1 loc2
+ | Alarm (stmt1, alarm1), Alarm (stmt2, alarm2) ->
+ Stmt.equal stmt1 stmt2 && Alarms.equal alarm1 alarm2
+ | _ -> false
+
+ let hash k =
+ let open Cil_datatype in
+ match k with
+ | Cluster -> Hashtbl.hash 0
+ | Scalar (vi, _, offset) ->
+ Hashtbl.hash (1, Varinfo.hash vi, OffsetStructEq.hash offset)
+ | Composite vi -> Hashtbl.hash (2, Varinfo.hash vi)
+ | Scattered (lv, loc) ->
+ Hashtbl.hash (3, LvalStructEq.hash lv, Locations.Location.hash loc)
+ | Alarm (stmt, alarm) ->
+ Hashtbl.hash (4, Stmt.hash stmt, Alarms.hash alarm)
+end
+
+include Datatype.Make (DatatypeInput)
+
+
let get_base = function
| Scalar (vi,_,_) | Composite (vi) -> Some vi
| Scattered _ | Alarm _ | Cluster -> None
@@ -32,12 +96,14 @@ let to_location = function
Some (Locations.loc_of_typoffset base typ offset)
| Composite (vi) ->
Some (Locations.loc_of_varinfo vi)
- | Scattered _ | Alarm _ | Cluster -> None
+ | Scattered (_,loc) ->
+ Some loc
+ | Alarm _ | Cluster -> None
let to_lval = function
| Scalar (vi,_typ,offset) -> Some (Cil_types.Var vi, offset)
| Composite (vi) -> Some (Cil_types.Var vi, Cil_types.NoOffset)
- | Scattered (lval) -> Some lval
+ | Scattered (lval,_) -> Some lval
| Alarm (_,_) | Cluster -> None
let pretty fmt = function
diff --git a/src/plugins/dive/node_kind.mli b/src/plugins/dive/node_kind.mli
new file mode 100644
index 0000000000000000000000000000000000000000..923348cf197c809bcd41688ca4b970fe71e54014
--- /dev/null
+++ b/src/plugins/dive/node_kind.mli
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C plug-in `Dive'. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Graph_types
+
+include Datatype.S with type t = Graph_types.node_kind
+
+val get_base : t -> Cil_types.varinfo option
+val to_location : t -> Locations.location option
+val to_lval : t -> Cil_types.lval option
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index b8038457f16050e2bd217e3f008ec80d86fb6dac..9c4a175c2b11d884170a806da9459d852255f49e 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -137,3 +137,24 @@ let () = Request.register ~page
Build.explore_from_vertex ~depth g node_key;
Build.get_graph g, Build.take_last_differences g
end
+
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"dive.show"
+ ~descr:(Markdown.rm "Show the dependencies of an existing vertex")
+ ~input:(module Data.Jint) ~output:(module GraphDiff)
+ begin fun node_key ->
+ let depth = Self.DepthLimit.get () in
+ let g = get_graph () in
+ Build.show ~depth g node_key;
+ Build.get_graph g, Build.take_last_differences g
+ end
+
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"dive.hide"
+ ~descr:(Markdown.rm "Hide the dependencies of an existing vertex")
+ ~input:(module Data.Jint) ~output:(module GraphDiff)
+ begin fun node_key ->
+ let g = get_graph () in
+ Build.hide g node_key;
+ Build.get_graph g, Build.take_last_differences g
+ end
\ No newline at end of file
diff --git a/src/plugins/dive/simple_deps.ml b/src/plugins/dive/simple_deps.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8baa89672fc3b8e173529be322bedb121200facf
--- /dev/null
+++ b/src/plugins/dive/simple_deps.ml
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C plug-in `Dive'. *)
+(* *)
+(* Copyright (C) 2018 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+class find_write target_vi = object (self)
+ inherit Visitor.frama_c_inplace
+
+ val mutable res = ([] : stmt list)
+
+ method add_current_stmt () =
+ res <- Extlib.the self#current_stmt :: res
+
+ method! vinst i =
+ begin match i with
+ | Call (None,_,_,_) | Asm _ | Skip _ | Code_annot _ -> () (* No effect *)
+ | Local_init(vi,_,_) ->
+ if Cil_datatype.Varinfo.equal vi target_vi then
+ self#add_current_stmt ()
+ | Call (Some dest,_,_,_)
+ | Set (dest,_,_) ->
+ match dest with
+ | Var vi, _ when vi = target_vi -> self#add_current_stmt ()
+ | _ -> ()
+ end;
+ Cil.SkipChildren
+
+ method result = res
+end
+
+let find_assignments kf vi =
+ let fundec = Kernel_function.get_definition kf
+ and vis = new find_write vi in
+ ignore (Visitor.visitFramacFunction (vis :> Visitor.frama_c_visitor) fundec);
+ vis#result
+
+let compute lval =
+ match lval with
+ | Var vi, NoOffset when not vi.vaddrof ->
+ Self.feedback "%a %B" Cil_printer.pp_varinfo vi vi.vaddrof;
+ begin try
+ let kf = Kernel_function.find_defining_kf vi in
+ Extlib.opt_map (fun kf -> find_assignments kf vi) kf
+ with Not_found -> None
+ end
+ | _ -> None