From 0aa72247b8801d2a4ada45eef76ea53339c5a003 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 15 Apr 2019 19:31:48 +0200
Subject: [PATCH] [Dive] Fix callstack computation for dependencies

---
 src/plugins/dive/Makefile.in                  |  2 +-
 src/plugins/dive/build.ml                     | 36 ++++++--
 src/plugins/dive/callstack.ml                 | 33 ++++++-
 src/plugins/dive/callstack.mli                |  3 +
 .../dive/tests/dive/oracle/assigned_param.dot | 25 +++---
 src/plugins/dive/tests/dive/oracle/const.dot  | 31 +++----
 .../dive/tests/dive/oracle/pointed_param.dot  | 41 ++++-----
 .../tests/dive/oracle/pointers_to_local.dot   | 28 ++++++
 .../dive/oracle/pointers_to_local.res.oracle  |  6 ++
 .../tests/dive/oracle/unfocused_callers.dot   | 45 +++++-----
 .../dive/tests/dive/oracle/various.dot        | 90 +++++++++----------
 .../dive/tests/dive/oracle/various.res.oracle |  2 +-
 .../dive/tests/dive/pointers_to_local.i       | 25 ++++++
 src/plugins/dive/tests/dive/various.i         |  1 +
 14 files changed, 233 insertions(+), 135 deletions(-)
 create mode 100644 src/plugins/dive/tests/dive/oracle/pointers_to_local.dot
 create mode 100644 src/plugins/dive/tests/dive/oracle/pointers_to_local.res.oracle
 create mode 100644 src/plugins/dive/tests/dive/pointers_to_local.i

diff --git a/src/plugins/dive/Makefile.in b/src/plugins/dive/Makefile.in
index f04bc8ed084..84aa9e726b3 100644
--- a/src/plugins/dive/Makefile.in
+++ b/src/plugins/dive/Makefile.in
@@ -38,7 +38,7 @@ endif
 
 PLUGIN_DIR ?=.
 PLUGIN_NAME := Dive
-PLUGIN_CMO := callstack self node_kind imprecision_graph build main
+PLUGIN_CMO := self callstack node_kind imprecision_graph build main
 PLUGIN_CMI:= graph_types
 PLUGIN_DEPENDENCIES:= Eva Studia
 PLUGIN_HAS_MLI:= yes
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 2a6763f3fe7..337a2c6cfdd 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -173,18 +173,24 @@ type t = {
 
 let reference_node_locality context node_locality =
   let { loc_file ; loc_callstack } = node_locality in
-  let add_file _ =
+  let rec add_file _ =
     let node_locality = { node_locality with loc_callstack = [] } in
     Graph.create_node context.graph ~node_kind:Cluster ~node_locality
-  and add_callstack _ =
-    Graph.create_node context.graph ~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);
+      Graph.create_node context.graph ~node_kind:Cluster ~node_locality
   in
-  ignore (FileTable.memo context.file_table loc_file add_file);
   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)
 
@@ -214,7 +220,7 @@ let build_node context callstack location lval  =
       | None -> location
       | Some location' -> location'
     in
-    let ref = (location', callstack) in
+    let ref = (location', node_locality.loc_callstack) in
     let node = NodeTable.memo context.node_table ref build_new_node in
     Some node
   end
@@ -251,9 +257,21 @@ let build_node_deps context node =
     let writes = Studia.Writes.compute zone
     and add_deps (stmt,effects) =
       match stmt.skind with
-      | Instr instr when effects.Studia.Writes.direct ->
-        build_instr_deps callstack stmt instr
-      | _ -> ()
+      | Instr _ when not effects.Studia.Writes.direct -> ()
+      | Instr instr ->
+        (* Keep only callstacks which are a compatible with the current one *)
+        let states = Db.Value.get_stmt_state_callstack ~after:false stmt in
+        let callstacks = match states with
+          | None -> assert false
+          | Some table ->
+            let module Table = Value_types.Callstack.Hashtbl in
+            Table.fold (fun cs _ acc -> cs :: acc) table []
+        in
+        (* TODO: missing callstacks filtered by memexec *)
+        let callstacks = Callstack.filter_truncate callstacks callstack in
+        (* Create a dependency for each of them *)
+        List.iter (fun cs -> build_instr_deps cs stmt instr) callstacks
+      | _ -> assert false
     in
     let count = List.length writes in
     Self.debug ~dkey "%d found" count;
diff --git a/src/plugins/dive/callstack.ml b/src/plugins/dive/callstack.ml
index 6a01ffb50e8..f9d5ae7157a 100644
--- a/src/plugins/dive/callstack.ml
+++ b/src/plugins/dive/callstack.ml
@@ -24,7 +24,8 @@ open Cil_types
 
 include Value_types.Callstack
 
-type call_site = (Cil_types.kernel_function * Cil_types.kinstr)
+type call_site = Value_types.call_site
+module Callsite = Value_types.Callsite
 
 let init kf = [(kf,Kglobal)]
 
@@ -47,4 +48,34 @@ let push (kf,stmt) cs =
   | [] -> [(kf,Kglobal)]
   | cs -> (kf,Kstmt stmt) :: cs
 
+let rec is_prefix cs1 cs2 =
+  match cs1, cs2 with
+  | [], _ -> true
+  | _, [] -> false
+  | [(kf,Kglobal)], (kf',_)::_ -> Kernel_function.equal kf kf'
+  | _, [(_,Kglobal)] -> false
+  | s1 :: t1, s2 :: t2 ->
+    if Callsite.equal s1 s2
+    then is_prefix t1 t2
+    else false
 
+let truncate_to_sub full_cs sub_cs =
+  let rec aux acc = function
+    | [] -> None
+  | (s :: t) as cs ->
+    if is_prefix sub_cs cs
+    then Some (List.rev acc @ sub_cs)
+    else aux (s :: acc) t
+  in
+  aux [] full_cs
+
+let list_filter_map f l =
+  let aux acc x =
+    match f x with
+    | None -> acc
+    | Some y -> y :: acc
+  in
+  List.rev (List.fold_left aux [] l)
+
+let filter_truncate l sub_cs =
+  list_filter_map (fun cs -> truncate_to_sub cs sub_cs) l
diff --git a/src/plugins/dive/callstack.mli b/src/plugins/dive/callstack.mli
index e5d55b8255d..7d3dce8a4b2 100644
--- a/src/plugins/dive/callstack.mli
+++ b/src/plugins/dive/callstack.mli
@@ -34,3 +34,6 @@ val init : Cil_types.kernel_function -> t
 val pop : t -> (Cil_types.kernel_function * Cil_types.stmt * t) option
 val pop_downto : Cil_types.kernel_function -> t -> t
 val push : Cil_types.kernel_function * Cil_types.stmt -> t -> t
+val is_prefix : t -> t -> bool
+val truncate_to_sub : t -> t -> t option
+val filter_truncate : t list -> t -> t list
diff --git a/src/plugins/dive/tests/dive/oracle/assigned_param.dot b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
index 0f545f95df0..f53cda98e10 100644
--- a/src/plugins/dive/tests/dive/oracle/assigned_param.dot
+++ b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
@@ -1,27 +1,24 @@
 digraph G {
   cp0 [style="invis,dotted", ];
-  cp1 [style="invis,dotted", ];
-  cp2 [label=<w>, shape=box, ];
-  cp3 [style="invis,dotted", ];
-  cp4 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp1 [label=<w>, shape=box, ];
+  cp2 [style="invis,dotted", ];
+  cp3 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp5 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp4 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
-  cp6 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp5 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
-  cp7 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp6 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
   
-  subgraph cluster_cs_1 { label=<main>; cp7;cp6;cp2;cp1;
-    subgraph cluster_cs_2 { label=<f>; cp5;cp4;cp3;
+  subgraph cluster_cs_1 { label=<main>; cp6;cp5;cp1;cp0;
+    subgraph cluster_cs_2 { label=<f>; cp4;cp3;cp2;
        };
      };
-  subgraph cluster_file_1 { label=<tests/dive/assigned_param.i>; cp0;
-     };
   
-  cp4 -> cp2;
-  cp5 -> cp4;
+  cp3 -> cp1;
+  cp4 -> cp3;
+  cp5 -> cp3;
   cp6 -> cp4;
-  cp7 -> cp5;
   
   }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/const.dot b/src/plugins/dive/tests/dive/oracle/const.dot
index 4921853943c..61ddfb59c4a 100644
--- a/src/plugins/dive/tests/dive/oracle/const.dot
+++ b/src/plugins/dive/tests/dive/oracle/const.dot
@@ -1,34 +1,31 @@
 digraph G {
   cp0 [style="invis,dotted", ];
-  cp1 [style="invis,dotted", ];
-  cp2 [label=<res>, shape=box, ];
-  cp3 [style="invis,dotted", ];
-  cp4 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp1 [label=<res>, shape=box, ];
+  cp2 [style="invis,dotted", ];
+  cp3 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp5 [label=<c>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp4 [label=<c>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
-  cp6 [label=<w>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp5 [label=<w>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
-  cp7 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp6 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
-  cp8 [label=<y>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp7 [label=<y>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled", ];
-  cp9 [label=<i>, shape=box, fillcolor="#EEFFEE", color="#004400",
+  cp8 [label=<i>, shape=box, fillcolor="#EEFFEE", color="#004400",
        style="filled,dotted", ];
   
-  subgraph cluster_cs_1 { label=<main>; cp9;cp2;cp1;
-    subgraph cluster_cs_2 { label=<f>; cp8;cp7;cp6;cp5;cp4;cp3;
+  subgraph cluster_cs_1 { label=<main>; cp8;cp1;cp0;
+    subgraph cluster_cs_2 { label=<f>; cp7;cp6;cp5;cp4;cp3;cp2;
        };
      };
-  subgraph cluster_file_1 { label=<tests/dive/const.i>; cp0;
-     };
   
-  cp4 -> cp2;
-  cp5 -> cp4;
+  cp3 -> cp1;
+  cp4 -> cp3;
+  cp5 -> cp3;
   cp6 -> cp4;
   cp7 -> cp5;
   cp8 -> cp6;
-  cp9 -> cp7;
-  cp9 -> cp8;
+  cp8 -> cp7;
   
   }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/pointed_param.dot b/src/plugins/dive/tests/dive/oracle/pointed_param.dot
index cc0432dfdae..4975eca71d4 100644
--- a/src/plugins/dive/tests/dive/oracle/pointed_param.dot
+++ b/src/plugins/dive/tests/dive/oracle/pointed_param.dot
@@ -1,36 +1,33 @@
 digraph G {
   cp0 [style="invis,dotted", ];
-  cp1 [style="invis,dotted", ];
-  cp2 [label=<y>, shape=box, ];
-  cp3 [label=<tmp>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp1 [label=<y>, shape=box, ];
+  cp2 [label=<tmp>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp4 [style="invis,dotted", ];
-  cp5 [label=<tmp>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp3 [style="invis,dotted", ];
+  cp4 [label=<tmp>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp6 [style="invis,dotted", ];
-  cp7 [label=<tmp>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp5 [style="invis,dotted", ];
+  cp6 [label=<tmp>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp8 [style="invis,dotted", ];
-  cp9 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp7 [style="invis,dotted", ];
+  cp8 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp10 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
-        style="filled,dotted", ];
+  cp9 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled,dotted", ];
   
-  subgraph cluster_cs_1 { label=<main>; cp3;cp2;cp1;
-    subgraph cluster_cs_2 { label=<f>; cp10;cp5;cp4;
-      subgraph cluster_cs_3 { label=<g>; cp7;cp6;
-        subgraph cluster_cs_4 { label=<h>; cp9;cp8;
+  subgraph cluster_cs_1 { label=<main>; cp2;cp1;cp0;
+    subgraph cluster_cs_2 { label=<f>; cp9;cp4;cp3;
+      subgraph cluster_cs_3 { label=<g>; cp6;cp5;
+        subgraph cluster_cs_4 { label=<h>; cp8;cp7;
            };
          };
        };
      };
-  subgraph cluster_file_1 { label=<tests/dive/pointed_param.i>; cp0;
-     };
   
-  cp3 -> cp2;
-  cp5 -> cp3;
-  cp7 -> cp5;
-  cp9 -> cp7;
-  cp10 -> cp9;
+  cp2 -> cp1;
+  cp4 -> cp2;
+  cp6 -> cp4;
+  cp8 -> cp6;
+  cp9 -> cp8;
   
   }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/pointers_to_local.dot b/src/plugins/dive/tests/dive/oracle/pointers_to_local.dot
new file mode 100644
index 00000000000..4977207ae32
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/pointers_to_local.dot
@@ -0,0 +1,28 @@
+digraph G {
+  cp0 [style="invis,dotted", ];
+  cp1 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  cp2 [style="invis,dotted", ];
+  cp3 [style="invis,dotted", ];
+  cp4 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  cp5 [style="invis,dotted", ];
+  cp6 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  
+  subgraph cluster_cs_1 { label=<main>; cp1;cp0;
+    subgraph cluster_cs_2 { label=<f1>; cp2;
+      subgraph cluster_cs_3 { label=<g>; cp4;cp3;
+         };
+       };
+    subgraph cluster_cs_4 { label=<f2>; cp6;cp5;
+       };
+     };
+  
+  cp1 -> cp1;
+  cp1 -> cp4;
+  cp1 -> cp6;
+  cp4 -> cp1;
+  cp6 -> cp1;
+  
+  }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/pointers_to_local.res.oracle b/src/plugins/dive/tests/dive/oracle/pointers_to_local.res.oracle
new file mode 100644
index 00000000000..5d460ce772b
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/pointers_to_local.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing tests/dive/pointers_to_local.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva] done for function main
+[dive] output to tests/dive/result/pointers_to_local.dot
diff --git a/src/plugins/dive/tests/dive/oracle/unfocused_callers.dot b/src/plugins/dive/tests/dive/oracle/unfocused_callers.dot
index 17fe2165025..873a1fc6479 100644
--- a/src/plugins/dive/tests/dive/oracle/unfocused_callers.dot
+++ b/src/plugins/dive/tests/dive/oracle/unfocused_callers.dot
@@ -1,38 +1,35 @@
 digraph G {
   cp0 [style="invis,dotted", ];
-  cp1 [style="invis,dotted", ];
-  cp2 [label=<x>, shape=box, ];
-  cp3 [style="invis,dotted", ];
-  cp4 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp1 [label=<x>, shape=box, ];
+  cp2 [style="invis,dotted", ];
+  cp3 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp5 [style="invis,dotted", ];
-  cp6 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp4 [style="invis,dotted", ];
+  cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp7 [style="invis,dotted", ];
-  cp8 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp6 [style="invis,dotted", ];
+  cp7 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled", ];
+  cp8 [style="invis,dotted", ];
+  cp9 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp9 [style="invis,dotted", ];
-  cp10 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
-        style="filled", ];
   
-  subgraph cluster_cs_1 { label=<g>; cp2;cp1;
-     };
-  subgraph cluster_cs_2 { label=<f3>; cp4;cp3;
+  subgraph cluster_cs_1 { label=<g>; cp1;cp0;
      };
-  subgraph cluster_cs_3 { label=<f2>; cp6;cp5;
+  subgraph cluster_cs_2 { label=<f3>; cp3;cp2;
      };
-  subgraph cluster_cs_4 { label=<f1>; cp8;cp7;
+  subgraph cluster_cs_3 { label=<f2>; cp5;cp4;
      };
-  subgraph cluster_cs_5 { label=<main>; cp10;cp9;
+  subgraph cluster_cs_4 { label=<f1>; cp7;cp6;
      };
-  subgraph cluster_file_1 { label=<tests/dive/unfocused_callers.i>; cp0;
+  subgraph cluster_cs_5 { label=<main>; cp9;cp8;
      };
   
-  cp4 -> cp2;
-  cp6 -> cp2;
-  cp8 -> cp2;
-  cp10 -> cp4;
-  cp10 -> cp6;
-  cp10 -> cp8;
+  cp3 -> cp1;
+  cp5 -> cp1;
+  cp7 -> cp1;
+  cp9 -> cp3;
+  cp9 -> cp5;
+  cp9 -> cp7;
   
   }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot
index 9ed41e39557..500799fd2fa 100644
--- a/src/plugins/dive/tests/dive/oracle/various.dot
+++ b/src/plugins/dive/tests/dive/oracle/various.dot
@@ -1,73 +1,71 @@
 digraph G {
   cp0 [style="invis,dotted", ];
-  cp1 [style="invis,dotted", ];
-  cp2 [label=<x2>, shape=box, ];
-  cp3 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp1 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp4 [style="invis,dotted", ];
-  cp5 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp2 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp6 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp3 [style="invis,dotted", ];
+  cp4 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp7 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp5 [style="invis,dotted", ];
+  cp6 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
        style="filled", ];
-  cp8 [label=<z>, shape=box, ];
-  cp9 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp7 [label=<z>, shape=box, ];
+  cp8 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
        style="filled", ];
-  cp10 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
-        style="filled", ];
-  cp11 [style="invis,dotted", ];
-  cp12 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp9 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled", ];
+  cp10 [style="invis,dotted", ];
+  cp11 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
         style="filled", ];
-  cp13 [label=<tmp_0>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp12 [label=<tmp_0>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
         style="filled", ];
-  cp14 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp13 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
         style="filled", ];
-  cp15 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+  cp14 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
         style="filled", ];
-  cp16 [style="invis,dotted", ];
-  cp17 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp15 [style="invis,dotted", ];
+  cp16 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
         style="filled", ];
-  cp18 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+  cp17 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
         style="filled", ];
-  cp19 [label=<is_nan_or_infinite: \is_finite((float)((double)((double)y * 2.0)))>,
+  cp18 [label=<is_nan_or_infinite: \is_finite((float)((double)((double)y * 2.0)))>,
         shape=doubleoctagon, fillcolor="#FF0000", color="#FF0000",
         style="bold,filled,bold", ];
-  cp20 [label=<is_nan_or_infinite: \is_finite((float)(y + w))>,
+  cp19 [label=<is_nan_or_infinite: \is_finite((float)(y + w))>,
         shape=doubleoctagon, fillcolor="#FF0000", color="#FF0000",
         style="bold,filled,bold", ];
   
-  subgraph cluster_cs_1 { label=<f>; cp19;cp6;cp3;cp2;cp1;
+  subgraph cluster_cs_1 { label=<f>; cp18;cp2;cp1;cp0;
      };
-  subgraph cluster_cs_2 { label=<main>; cp20;cp15;cp13;cp10;cp9;cp8;cp5;cp4;
-    subgraph cluster_cs_3 { label=<f>; cp14;cp12;cp11;
+  subgraph cluster_cs_2 { label=<main>; cp19;cp14;cp12;cp9;cp8;cp7;cp4;cp3;
+    subgraph cluster_cs_3 { label=<f>; cp13;cp11;cp10;
        };
-    subgraph cluster_cs_4 { label=<f>; cp18;cp17;cp16;
+    subgraph cluster_cs_4 { label=<f>; cp17;cp16;cp15;
        };
      };
-  subgraph cluster_file_1 { label=<tests/dive/various.i>; cp7;cp0;
+  subgraph cluster_file_1 { label=<tests/dive/various.i>; cp6;cp5;
      };
   
-  cp3 -> cp2;
-  cp3 -> cp6;
-  cp3 -> cp19;
-  cp5 -> cp2;
-  cp5 -> cp6;
-  cp5 -> cp12;
-  cp5 -> cp17;
-  cp6 -> cp3;
-  cp7 -> cp5;
-  cp9 -> cp8;
-  cp9 -> cp20;
-  cp10 -> cp8;
-  cp10 -> cp20;
+  cp1 -> cp2 [style="bold", ];
+  cp2 -> cp1 [style="bold", ];
+  cp2 -> cp18;
+  cp4 -> cp1;
+  cp4 -> cp4;
+  cp4 -> cp11;
+  cp4 -> cp16;
+  cp6 -> cp4;
+  cp8 -> cp7;
+  cp8 -> cp19;
+  cp9 -> cp7;
+  cp9 -> cp19;
+  cp11 -> cp8;
+  cp11 -> cp13;
   cp12 -> cp9;
-  cp12 -> cp14;
-  cp13 -> cp10;
-  cp14 -> cp12;
-  cp15 -> cp13 [color="#00FF00", ];
-  cp17 -> cp13;
-  cp17 -> cp18;
-  cp18 -> cp17;
+  cp13 -> cp11;
+  cp14 -> cp12 [color="#00FF00", ];
+  cp16 -> cp12;
+  cp16 -> cp17;
+  cp17 -> cp16;
   
   }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/various.res.oracle b/src/plugins/dive/tests/dive/oracle/various.res.oracle
index fc941299b06..8dbdfbde803 100644
--- a/src/plugins/dive/tests/dive/oracle/various.res.oracle
+++ b/src/plugins/dive/tests/dive/oracle/various.res.oracle
@@ -6,7 +6,7 @@
 [eva:alarm] tests/dive/various.i:13: Warning: 
   non-finite float value.
   assert \is_finite((float)((double)((double)y * 2.0)));
-[eva:alarm] tests/dive/various.i:26: Warning: 
+[eva:alarm] tests/dive/various.i:27: Warning: 
   non-finite float value. assert \is_finite((float)(y + w));
 [eva] done for function main
 [dive] output to tests/dive/result/various.dot
diff --git a/src/plugins/dive/tests/dive/pointers_to_local.i b/src/plugins/dive/tests/dive/pointers_to_local.i
new file mode 100644
index 00000000000..832b282261a
--- /dev/null
+++ b/src/plugins/dive/tests/dive/pointers_to_local.i
@@ -0,0 +1,25 @@
+/* run.config
+STDOPT: +"-dive-from main::x -dive-depth-limit 5"
+*/
+
+void g(float *p) {
+  float x = *p;
+  *p = x + 1.0f;
+}
+
+void f1(float *p) {
+  g(p);
+}
+
+void f2(float *p) {
+  float x = *p;
+  *p += x + 2.0f;
+}
+
+float main()
+{
+  float x = 0.0f;
+  f1(&x);
+  f2(&x);
+  return x;
+}
diff --git a/src/plugins/dive/tests/dive/various.i b/src/plugins/dive/tests/dive/various.i
index f89d87ed5c8..f4008ace228 100644
--- a/src/plugins/dive/tests/dive/various.i
+++ b/src/plugins/dive/tests/dive/various.i
@@ -22,6 +22,7 @@ void main()
 
   float x = 3.0 + g;
   float y = f(x);
+  x = x + 0.5f;
   float w = (*pf)(x);
   float z = y + w + 1.0;
 }
-- 
GitLab