diff --git a/src/plugins/dive/main.ml b/src/plugins/dive/main.ml
index e7f7f3ffa0b6a9f86260b22b0d4d2c194e3eccaf..51c905e88abcbdf72fce521c3da6510ad85cb7e0 100644
--- a/src/plugins/dive/main.ml
+++ b/src/plugins/dive/main.ml
@@ -31,9 +31,14 @@ let main () =
     let depth_limit = Self.DepthLimit.get () in
     Self.FromBases.iter (Build.add_var ~depth_limit context);
     (* Output it *)
-    let out_channel = open_out "imprecisions.dot" in
-    Imprecision_graph.ouptput_to_dot out_channel (Build.get_graph context);
-    close_out out_channel
+    let output_basename = Self.OutputBasename.get () in
+    if output_basename <> "" then begin
+      let filename = output_basename ^ ".dot" in
+      Self.result "output to %s" filename;
+      let out_channel = open_out filename in
+      Imprecision_graph.ouptput_to_dot out_channel (Build.get_graph context);
+      close_out out_channel
+    end;
   end
 
 let () =
diff --git a/src/plugins/dive/self.ml b/src/plugins/dive/self.ml
index 60d794eff335c5b08b65fe3be7f706bef06eab00..09a9616fd6b434887c5923366888bf22b55ce40f 100644
--- a/src/plugins/dive/self.ml
+++ b/src/plugins/dive/self.ml
@@ -29,12 +29,19 @@ include Plugin.Register
       let help = "An interactive imprecision graph generator."
     end)
 
+module OutputBasename = Empty_string
+    (struct
+      let option_name = "-dive-output"
+      let help = "Outputs the built graph into a file with this basename."
+      let arg_name = "basename"
+    end)
+
 module DepthLimit = Int
     (struct
-      let default = 5
       let option_name = "-dive-depth-limit"
       let help = "Build dependencies up to a depth of N."
       let arg_name = "N"
+      let default = 3
     end)
 
 module FromAlarms = True
@@ -49,26 +56,27 @@ struct
 
   let of_string s =
     let regexp = Str.regexp "^\\([_a-zA-Z0-9]+\\)::\\([_a-zA-Z0-9]+\\)$" in
-    let name, localisation, error_suffix =
-      if Str.string_match regexp s 0 then
-        let function_name = Str.matched_group 1 s
-        and variable_name = Str.matched_group 2 s in
-        try
-          let kf = Globals.Functions.find_by_name function_name in
-          variable_name, VLocal kf, " in function " ^ function_name
+    if Str.string_match regexp s 0 then
+      let function_name = Str.matched_group 1 s
+      and variable_name = Str.matched_group 2 s in
+      let kf = try Globals.Functions.find_by_name function_name
         with Not_found -> 
           raise (Cannot_build ("no function '" ^ function_name ^ "'"))
-      else
-        let regexp = Str.regexp "^[_a-zA-Z0-9]+$" in
-        if Str.string_match regexp s 0 then
-          s, VGlobal, ""
-        else
-          raise (Cannot_build ("wrong syntax: '" ^ s ^ "'"))
-    in
-    try
-      Globals.Vars.find_from_astinfo name localisation
-    with Not_found ->
-      raise (Cannot_build ("no variable '" ^ name ^ "'" ^ error_suffix))
+      in
+      try Globals.Vars.find_from_astinfo variable_name (VLocal kf)
+      with Not_found ->
+      try Globals.Vars.find_from_astinfo variable_name (VFormal kf)
+      with Not_found ->
+        raise (Cannot_build ("no variable '" ^ name ^ "' in function"
+                             ^ function_name))
+    else
+      let regexp = Str.regexp "^[_a-zA-Z0-9]+$" in
+      if not (Str.string_match regexp s 0) then
+        raise (Cannot_build ("wrong syntax: '" ^ s ^ "'"));
+      try
+        Globals.Vars.find_from_astinfo name VGlobal
+      with Not_found ->
+        raise (Cannot_build ("no global variable '" ^ name ^ "'"))
 
   let to_string vi =
     match Kernel_function.find_defining_kf vi with
diff --git a/src/plugins/dive/self.mli b/src/plugins/dive/self.mli
index f56de61ab58205ca8d215ef15733236f2af39763..8d9f9f8b0ecc93461af482b30ea5ba520d1c02da 100644
--- a/src/plugins/dive/self.mli
+++ b/src/plugins/dive/self.mli
@@ -26,6 +26,7 @@ module type Varinfo_set = Parameter_sig.Set
   with type elt = Cil_types.varinfo
    and type t = Cil_datatype.Varinfo.Set.t
 
+module OutputBasename : Parameter_sig.String
 module DepthLimit : Parameter_sig.Int
 module FromAlarms : Parameter_sig.Bool
 module FromBases : Varinfo_set
diff --git a/src/plugins/dive/tests/dive/assigned_param.i b/src/plugins/dive/tests/dive/assigned_param.i
new file mode 100644
index 0000000000000000000000000000000000000000..322aa200478933843561c32efa025212c260607e
--- /dev/null
+++ b/src/plugins/dive/tests/dive/assigned_param.i
@@ -0,0 +1,18 @@
+/* run.config
+STDOPT: +"-dive-from main::w"
+*/
+
+volatile int nondet;
+
+int f(int x, int z)
+{
+  if (nondet)
+    x = z;
+  return x;
+}
+
+int main(int x, int z)
+{
+  int w = f(x,z);
+  return w + 1;
+}
diff --git a/src/plugins/dive/tests/dive/const.i b/src/plugins/dive/tests/dive/const.i
new file mode 100644
index 0000000000000000000000000000000000000000..adc5365c8c65e97e4fb497cc0ff8c1119ac420dc
--- /dev/null
+++ b/src/plugins/dive/tests/dive/const.i
@@ -0,0 +1,16 @@
+/* run.config
+STDOPT: +"-dive-from main::res"
+*/
+
+int f(int x, int y)
+{
+  const c = x + 1;
+  int w = y + 1;
+  return c + w;
+}
+
+int main(int i)
+{
+  int res = f(i, 2*i);
+  return res;
+}
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/assigned_param.dot b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
new file mode 100644
index 0000000000000000000000000000000000000000..460be6d9d7299106e74d0f4c06e6ddb4b90058d3
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
@@ -0,0 +1,23 @@
+digraph G {
+  cp0 [fillcolor="#AACCFF", color="#88AAFF", style="invis,filled,dotted", ];
+  cp1 [label=<w>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  cp2 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  cp3 [label=<z>, shape=box, ];
+  cp4 [label=<x>, shape=box, ];
+  cp5 [label=<z>, shape=box, style="dotted", ];
+  
+  subgraph cluster_file_1 { label=<tests/dive/assigned_param.i>; cp0;
+    subgraph cluster_function_19 { label=<f>; cp3;cp2;
+       };
+    subgraph cluster_function_24 { label=<main>; cp5;cp4;cp1;
+       };
+     };
+  
+  cp2 -> cp1;
+  cp3 -> cp2;
+  cp4 -> cp2;
+  cp5 -> cp3;
+  
+  }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/assigned_param.res.oracle b/src/plugins/dive/tests/dive/oracle/assigned_param.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..01978d954708330fd10ff862b91570b8bcca166a
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/assigned_param.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing tests/dive/assigned_param.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:alarm] tests/dive/assigned_param.i:18: Warning: 
+  signed overflow. assert w + 1 ≤ 2147483647;
+[eva] done for function main
+[dive] output to tests/dive/result/assigned_param.dot
diff --git a/src/plugins/dive/tests/dive/oracle/const.dot b/src/plugins/dive/tests/dive/oracle/const.dot
new file mode 100644
index 0000000000000000000000000000000000000000..cce0e10e5aa4ee290c68002c57da8703017528c2
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/const.dot
@@ -0,0 +1,28 @@
+digraph G {
+  cp0 [fillcolor="#AACCFF", color="#88AAFF", style="invis,filled,dotted", ];
+  cp1 [label=<res>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  cp2 [fillcolor="#AACCFF", color="#88AAFF", style="invis,filled,dotted", ];
+  cp3 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  cp4 [label=<c>, shape=box, ];
+  cp5 [label=<w>, shape=box, ];
+  cp6 [label=<x>, shape=box, style="dotted", ];
+  cp7 [label=<y>, shape=box, style="dotted", ];
+  
+  subgraph cluster_file_1 { label=<tests/dive/const.i>; cp0;
+    subgraph cluster_function_25 { label=<main>; cp1;
+       };
+     };
+  subgraph cluster_file_2 { label=<>; cp2;
+    subgraph cluster_function_18 { label=<f>; cp7;cp6;cp5;cp4;cp3;
+       };
+     };
+  
+  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.res.oracle b/src/plugins/dive/tests/dive/oracle/const.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7b0b90606588cc92149b6875e5915423cc3092eb
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/const.res.oracle
@@ -0,0 +1,16 @@
+[kernel] Parsing tests/dive/const.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:alarm] tests/dive/const.i:14: Warning: 
+  signed overflow. assert -2147483648 ≤ 2 * i;
+[eva:alarm] tests/dive/const.i:14: Warning: 
+  signed overflow. assert 2 * i ≤ 2147483647;
+[eva:alarm] tests/dive/const.i:7: Warning: 
+  signed overflow. assert x + 1 ≤ 2147483647;
+[eva:alarm] tests/dive/const.i:9: Warning: 
+  signed overflow. assert -2147483648 ≤ c + w;
+[eva:alarm] tests/dive/const.i:9: Warning: 
+  signed overflow. assert c + w ≤ 2147483647;
+[eva] done for function main
+[dive] output to tests/dive/result/const.dot
diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot
new file mode 100644
index 0000000000000000000000000000000000000000..e9d2bb149eab62bafa3b10b122cd8d96fba0eea3
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/various.dot
@@ -0,0 +1,40 @@
+digraph G {
+  cp0 [fillcolor="#AACCFF", color="#88AAFF", style="invis,filled,dotted", ];
+  cp1 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled", ];
+  cp2 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled", ];
+  cp3 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  cp4 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  cp5 [label=<z>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled", ];
+  cp6 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled", ];
+  cp7 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled", ];
+  cp8 [label=<tmp_0>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+       style="filled", ];
+  cp9 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+       style="filled,dotted", ];
+  
+  subgraph cluster_file_1 { label=<tests/dive/various.i>; cp4;cp0;
+    subgraph cluster_function_19 { label=<f>; cp2;cp1;
+       };
+    subgraph cluster_function_24 { label=<main>; cp9;cp8;cp7;cp6;cp5;cp3;
+       };
+     };
+  
+  cp1 -> cp2;
+  cp1 -> cp6;
+  cp1 -> cp8;
+  cp2 -> cp1;
+  cp3 -> cp1;
+  cp4 -> cp3;
+  cp6 -> cp5;
+  cp7 -> cp5;
+  cp8 -> cp7;
+  cp9 -> cp8 [color="#00FF00", ];
+  
+  }
\ 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
new file mode 100644
index 0000000000000000000000000000000000000000..fc941299b063f39c78a3f841e4cd999087d35574
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/various.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/dive/various.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva] tests/dive/various.i:10: starting to merge loop iterations
+[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: 
+  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/various.i b/src/plugins/dive/tests/dive/various.i
new file mode 100644
index 0000000000000000000000000000000000000000..84c0f7788f763b62c42dc7a4918c6c160c94b6cd
--- /dev/null
+++ b/src/plugins/dive/tests/dive/various.i
@@ -0,0 +1,28 @@
+/* run.config
+STDOPT: +"-dive-from main::z,f::x2"
+*/
+
+float g;
+
+float f(float x2)
+{
+  float y;
+  for (int i = 0 ; i < 10 ; i++)
+  {
+    y = x2 + 1.0;
+    x2 = y * 2.0;
+  }
+
+  return x2;
+}
+
+void main()
+{
+  float (*pf)(float) = &f;
+
+  float x = 3.0 + g;
+  float y = f(x);
+  float w = (*pf)(x);
+  float z = y + w + 1.0;
+}
+
diff --git a/src/plugins/dive/tests/test_config b/src/plugins/dive/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..2baab62a7d788431a99459bec75bc3004ea1e724
--- /dev/null
+++ b/src/plugins/dive/tests/test_config
@@ -0,0 +1,2 @@
+LOG: @PTEST_NAME@.dot
+OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope,dive -check -eva-msg-key=-initial-state -eva-no-show-progress -dive-output @PTEST_RESULT@/@PTEST_NAME@