From 39984416934ae5ea30890da6a8cc90a020aa85d7 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 9 Apr 2019 18:32:18 +0200
Subject: [PATCH] [Dive] Compute dependencies per callstack
---
src/plugins/dive/Makefile.in | 2 +-
src/plugins/dive/build.ml | 360 ++++++++++--------
src/plugins/dive/callstack.ml | 50 +++
src/plugins/dive/callstack.mli | 36 ++
src/plugins/dive/graph_types.mli | 4 +-
src/plugins/dive/imprecision_graph.ml | 58 ++-
src/plugins/dive/node_kind.ml | 8 +-
src/plugins/dive/tests/dive/const.i | 2 +-
.../dive/tests/dive/oracle/assigned_param.dot | 26 +-
src/plugins/dive/tests/dive/oracle/const.dot | 35 +-
.../dive/tests/dive/oracle/pointed_param.dot | 36 ++
.../dive/oracle/pointed_param.res.oracle | 6 +
.../tests/dive/oracle/unfocused_callers.dot | 38 ++
.../dive/oracle/unfocused_callers.res.oracle | 14 +
.../dive/tests/dive/oracle/various.dot | 83 ++--
src/plugins/dive/tests/dive/pointed_param.i | 25 ++
.../dive/tests/dive/unfocused_callers.i | 19 +
src/plugins/dive/tests/test_config | 2 +-
18 files changed, 556 insertions(+), 248 deletions(-)
create mode 100644 src/plugins/dive/callstack.ml
create mode 100644 src/plugins/dive/callstack.mli
create mode 100644 src/plugins/dive/tests/dive/oracle/pointed_param.dot
create mode 100644 src/plugins/dive/tests/dive/oracle/pointed_param.res.oracle
create mode 100644 src/plugins/dive/tests/dive/oracle/unfocused_callers.dot
create mode 100644 src/plugins/dive/tests/dive/oracle/unfocused_callers.res.oracle
create mode 100644 src/plugins/dive/tests/dive/pointed_param.i
create mode 100644 src/plugins/dive/tests/dive/unfocused_callers.i
diff --git a/src/plugins/dive/Makefile.in b/src/plugins/dive/Makefile.in
index 56431372bfd..f04bc8ed084 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 := self node_kind imprecision_graph build main
+PLUGIN_CMO := callstack self 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 f8a9eee5dd8..2a6763f3fe7 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -114,55 +114,76 @@ let build_node_kind ~is_folded_base lval location =
and matching = Bit_utils.MatchType typ in
let offset', _ = Bit_utils.find_offset vi.vtype ~offset matching in
Scalar (vi, typ, offset')
- with Ival.Not_Singleton_Int ->
+ with Bit_utils.NoMatchingOffset | Ival.Not_Singleton_Int ->
+ (* TODO: handle Bit_utils.NoMatchingOffset (strict aliasing ?) *)
Scattered (lval)
end
| None ->
Scattered (lval)
-let stmt_to_node_locality stmt =
- let kf = Kernel_function.find_englobing_kf stmt in
- let file = get_loc_filename (Kernel_function.get_location kf) in
- { loc_file = file ; loc_function = Some kf }
+let default_node_locality callstack =
+ match callstack with
+ | [] ->
+ (* The empty callstack can be used for global lvalues *)
+ { loc_file="" ; loc_callstack=[] }
+ | (kf,_kinstr) :: _ ->
+ let loc_file = get_loc_filename (Kernel_function.get_location kf) in
+ { loc_file ; loc_callstack=callstack }
-let build_node_locality kinstr kind =
- match Node_kind.get_base kind with
+let build_node_locality callstack node_kind =
+ match Node_kind.get_base node_kind with
+ | None -> default_node_locality callstack
| Some vi ->
- let loc_function = Kernel_function.find_defining_kf vi in
- (* Use the location of the defining function if it exists, as some
- temporary variables do not have proper location *)
- let def_vi = Extlib.may_map Kernel_function.get_vi ~dft:vi loc_function in
- let loc_file = get_loc_filename def_vi.vdecl in
- { loc_file ; loc_function }
- | None ->
- match kinstr with
- | Kglobal -> assert false
- | Kstmt stmt -> stmt_to_node_locality stmt
+ match Kernel_function.find_defining_kf vi with
+ | Some kf ->
+ let callstack =
+ try
+ Callstack.pop_downto kf callstack
+ with Failure _ ->
+ Callstack.init kf (* TODO: complete callstack *)
+ in
+ default_node_locality callstack
+ | None ->
+ { loc_file = get_loc_filename vi.vdecl ; loc_callstack = [] }
(* --- Context object --- *)
+module NodeRef = Datatype.Pair_with_collections
+ (Locations.Location) (Callstack)
+ (struct let module_name = "Build.NodeRef" end)
+
module Graph = Imprecision_graph
-module NodeTable = FCHashtbl.Make (Locations.Location)
+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 = {
graph: Graph.t;
node_table: node NodeTable.t;
file_table: node FileTable.t;
+ callstack_table: node CallstackTable.t;
mutable unfolded_bases: BaseSet.t;
mutable hidden_bases: BaseSet.t;
+ mutable focus: bool FunctionMap.t;
mutable roots: node list;
}
-let reference_file context loc_file =
- if not (FileTable.mem context.file_table loc_file) then begin
- let node_kind = File
- and node_locality = { loc_file ; loc_function = None } in
- let node = Graph.create_node context.graph ~node_kind ~node_locality in
- FileTable.add context.file_table loc_file node
- end
+let reference_node_locality context node_locality =
+ let { loc_file ; loc_callstack } = node_locality in
+ let 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
+ in
+ ignore (FileTable.memo context.file_table loc_file add_file);
+ match loc_callstack with
+ | [] -> ()
+ | cs ->
+ ignore (CallstackTable.memo context.callstack_table cs add_callstack)
let is_folded context vi =
not (BaseSet.mem vi context.unfolded_bases)
@@ -176,15 +197,15 @@ let is_hidden context node_kind =
(* --- Graph building --- *)
(* Update or create a node *)
-let build_node context kinstr location lval =
+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 kinstr node_kind in
+ let node_locality = build_node_locality callstack node_kind in
+ reference_node_locality context node_locality;
let build_new_node _location =
- reference_file context node_locality.loc_file;
Graph.create_node context.graph ~node_kind ~node_locality
in
(* Compute the new location which might have changed after folding *)
@@ -193,19 +214,20 @@ let build_node context kinstr location lval =
| None -> location
| Some location' -> location'
in
- let node = NodeTable.memo context.node_table location' build_new_node in
+ let ref = (location', callstack) in
+ let node = NodeTable.memo context.node_table ref build_new_node in
Some node
end
-let build_var context varinfo =
+let build_var context callstack varinfo =
let location = Locations.loc_of_varinfo varinfo
and lval = Var varinfo, NoOffset in
- build_node context Kglobal location lval
+ build_node context callstack location lval
-let build_lval context kinstr lval =
+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 kinstr location lval with
+ match build_node context callstack location lval with
| None -> None
| Some node ->
(* Update the precision information *)
@@ -213,138 +235,150 @@ let build_lval context kinstr lval =
Graph.update_node_precision node node_precision;
Some node
-let build_alarm context stmt alarm =
- let node_kind = Alarm (stmt,alarm)
- and node_locality = stmt_to_node_locality stmt
+let build_alarm context callstack stmt alarm =
+ let node_kind = Alarm (stmt,alarm) in
+ let node_locality = build_node_locality callstack node_kind
and node_precision = Critical in
Graph.create_node context.graph ~node_precision ~node_kind ~node_locality
+
exception Too_many_deps of lval
-let rec build_node_deps context node =
+let build_node_deps context node =
+ let rec build_writes_deps callstack lval =
+ Self.debug ~dkey "computing deps for %a" Cil_printer.pp_lval lval;
+ let zone = !Db.Value.lval_to_zone Kglobal lval in
+ 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
+ | _ -> ()
+ in
+ let count = List.length writes in
+ Self.debug ~dkey "%d found" count;
+ if count > 20 then
+ raise (Too_many_deps lval)
+ else
+ List.iter add_deps writes
+
+ and build_arg_deps callstack vi =
+ assert vi.vformal;
+ let kf = Extlib.the (Kernel_function.find_defining_kf vi) in
+ let pos = Kernel_function.get_formal_position vi kf in
+ let callsites =
+ match Callstack.pop callstack with
+ | Some (kf',stmt,callstack) ->
+ assert (Kernel_function.equal kf' kf);
+ [(stmt,callstack)]
+ | None ->
+ let callsites = Kernel_function.find_syntactic_callsites kf in
+ List.map (fun (kf,stmt) -> (stmt,Callstack.init kf)) callsites
+ and add_deps (stmt,callstack) =
+ match stmt.skind with
+ | Instr (Call (_,_,args,_))
+ | Instr (Local_init (_, ConsInit (_, args, _), _)) ->
+ let exp = List.nth args pos in
+ build_exp_deps callstack stmt Data exp
+ | _ ->
+ assert false (* Callsites can only be Call or ConsInit *)
+ in
+ List.iter add_deps callsites
+
+ and build_return_deps callstack stmt args kf =
+ match Kernel_function.find_return kf with
+ | {skind = Return (Some {enode = Lval lval_res},_)} ->
+ let callstack = Callstack.push (kf,stmt) callstack in
+ build_lval_deps callstack stmt Data lval_res
+ | _ -> assert false (* Cil invariant *)
+ | exception Kernel_function.No_Statement ->
+ (* the function is only a prototype *)
+ (* TODO: read assigns instead *)
+ List.iter (build_exp_deps callstack stmt Data) args
+
+ and build_call_deps callstack stmt callee args =
+ begin match callee.enode with
+ | Lval (Var _vi, _offset) -> ()
+ | Lval (Mem exp, _offset) ->
+ build_exp_deps callstack stmt Callee exp
+ | _ ->
+ Self.warning "Cannot compute all callee dependencies for %a"
+ Cil_printer.pp_stmt stmt;
+ end;
+ let kinstr = Kstmt stmt in
+ let _,set = !Db.Value.expr_to_kernel_function kinstr ~deps:None callee in
+ Kernel_function.Hptset.iter (build_return_deps callstack stmt args) set
+
+ and build_alarm_deps callstack stmt alarm =
+ let for_exp e =
+ build_exp_deps callstack stmt Data e
+ in
+ let open Alarms in
+ match alarm with
+ | Division_by_zero e | Index_out_of_bound (e, _) | Invalid_shift (e,_)
+ | Overflow (_,e,_,_) | Float_to_int (e,_,_) | Is_nan_or_infinite (e,_)
+ | Is_nan (e,_) | Function_pointer (e,_) -> for_exp e
+ | Pointer_comparison (opt_e1,e2) -> Extlib.may for_exp opt_e1; for_exp e2
+ | Differing_blocks (e1,e2) -> for_exp e1; for_exp e2
+ | Memory_access _ | Not_separated _ | Overlap _
+ | Uninitialized _ | Dangling _ | Uninitialized_union _ -> ()
+ (* TODO: adress depencies inside lval *)
+ | Invalid_bool lv -> build_lval_deps callstack stmt Data lv
+
+ and build_instr_deps callstack stmt = function
+ | Set (_, exp, _) ->
+ build_exp_deps callstack stmt Data exp
+ | Call (_, callee, args, _) -> build_call_deps callstack stmt callee args
+ | Local_init (dest, ConsInit (f, args, k), loc) ->
+ let as_func _dest callee args _loc =
+ build_call_deps callstack stmt callee args
+ in
+ Cil.treat_constructor_as_func as_func dest f args k loc
+ | Local_init (_, AssignInit init, _) ->
+ build_init_deps callstack stmt init
+ | Asm _ | Skip _ | Code_annot _ -> () (* Cases not returned by Studia *)
+
+ and build_init_deps callstack stmt = function
+ | SingleInit exp ->
+ build_exp_deps callstack stmt Data exp
+ | CompoundInit (_typ, initl) ->
+ List.iter (fun (_off,init) -> build_init_deps callstack stmt init) initl
+
+ and build_exp_deps callstack stmt kind exp =
+ match exp.enode with
+ | Const _
+ | SizeOf _ | SizeOfE _ | SizeOfStr _
+ | AlignOf _ | AlignOfE _
+ | AddrOf _ | StartOf _ -> ()
+ | Lval lval ->
+ build_lval_deps callstack stmt kind lval
+ | UnOp (_,e,_) | CastE (_,e) | Info (e,_) ->
+ build_exp_deps callstack stmt kind e
+ | BinOp (_,e1,e2,_) ->
+ build_exp_deps callstack stmt kind e1;
+ 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
+
+ in
+ let callstack = node.node_locality.loc_callstack in
match node.node_kind with
| Scalar (vi,_typ,offset) ->
- build_writes_deps context node (Cil_types.Var vi, offset);
- if vi.vformal then build_arg_deps context node vi
+ build_writes_deps callstack (Cil_types.Var vi, offset);
+ if vi.vformal then build_arg_deps callstack vi
| Composite (vi) ->
- build_writes_deps context node (Cil_types.Var vi, Cil_types.NoOffset);
- if vi.vformal then build_arg_deps context node 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 *)
| Alarm (stmt,alarm) ->
- build_alarm_deps context node stmt alarm
- | File -> ()
-
-and build_writes_deps context src lval =
- Self.debug ~dkey "computing deps for %a" Cil_printer.pp_lval lval;
- let zone = !Db.Value.lval_to_zone Kglobal lval in
- 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 context src stmt instr
- | _ -> ()
- in
- let count = List.length writes in
- Self.debug ~dkey "%d found" count;
- if count > 20 then
- raise (Too_many_deps lval)
- else
- List.iter add_deps writes
-
-and build_arg_deps context src vi =
- assert vi.vformal;
- let kf = Extlib.the (Kernel_function.find_defining_kf vi) in
- let pos = Kernel_function.get_formal_position vi kf in
- let callsites = Kernel_function.find_syntactic_callsites kf
- and add_deps (_caller_kf, stmt) =
- match stmt.skind with
- | Instr (Call (_,_,args,_))
- | Instr (Local_init (_, ConsInit (_, args, _), _)) ->
- let exp = List.nth args pos in
- build_exp_deps context src stmt Data exp
- | _ ->
- assert false (* Callsites can only be Call or ConsInit *)
- in
- List.iter add_deps callsites
-
-and build_return_deps context src stmt args kf =
- match Kernel_function.find_return kf with
- | {skind = Return (Some {enode = Lval lval_res},_)} ->
- build_lval_deps context src stmt Data lval_res
- | _ -> assert false (* Cil invariant *)
- | exception Kernel_function.No_Statement ->
- (* the function is only a prototype *)
- (* TODO: read assigns instead *)
- List.iter (build_exp_deps context src stmt Data) args
-
-and build_call_deps context src stmt callee args =
- begin match callee.enode with
- | Lval (Var _vi, _offset) -> ()
- | Lval (Mem exp, _offset) ->
- build_exp_deps context src stmt Callee exp
- | _ ->
- Self.warning "Cannot compute all callee dependencies for %a"
- Cil_printer.pp_stmt stmt;
- end;
- let kinstr = Kstmt stmt in
- let _,set = !Db.Value.expr_to_kernel_function kinstr ~deps:None callee in
- Kernel_function.Hptset.iter (build_return_deps context src stmt args) set
-
-and build_alarm_deps context src stmt alarm =
- let for_exp e =
- build_exp_deps context src stmt Data e
- in
- let open Alarms in
- match alarm with
- | Division_by_zero e | Index_out_of_bound (e, _) | Invalid_shift (e,_)
- | Overflow (_,e,_,_) | Float_to_int (e,_,_) | Is_nan_or_infinite (e,_)
- | Is_nan (e,_) | Function_pointer (e,_) -> for_exp e
- | Pointer_comparison (opt_e1,e2) -> Extlib.may for_exp opt_e1; for_exp e2
- | Differing_blocks (e1,e2) -> for_exp e1; for_exp e2
- | Memory_access _ | Not_separated _ | Overlap _
- | Uninitialized _ | Dangling _ | Uninitialized_union _ -> ()
- (* TODO: adress depencies inside lval *)
- | Invalid_bool lv -> build_lval_deps context src stmt Data lv
-
-and build_instr_deps context src stmt = function
- | Set (_, exp, _) ->
- build_exp_deps context src stmt Data exp
- | Call (_, callee, args, _) -> build_call_deps context src stmt callee args
- | Local_init (dest, ConsInit (f, args, k), loc) ->
- let as_func _dest callee args _loc =
- build_call_deps context src stmt callee args
- in
- Cil.treat_constructor_as_func as_func dest f args k loc
- | Local_init (_, AssignInit init, _) ->
- build_init_deps context src stmt init
- | Asm _ | Skip _ | Code_annot _ -> () (* Cases not returned by Studia *)
-
-and build_init_deps context src stmt = function
- | SingleInit exp ->
- build_exp_deps context src stmt Data exp
- | CompoundInit (_typ, initl) ->
- List.iter (fun (_off,init) -> build_init_deps context src stmt init) initl
-
-and build_exp_deps context src stmt kind exp =
- match exp.enode with
- | Const _
- | SizeOf _ | SizeOfE _ | SizeOfStr _
- | AlignOf _ | AlignOfE _
- | AddrOf _ | StartOf _ -> ()
- | Lval lval ->
- build_lval_deps context src stmt kind lval
- | UnOp (_,e,_) | CastE (_,e) | Info (e,_) ->
- build_exp_deps context src stmt kind e
- | BinOp (_,e1,e2,_) ->
- build_exp_deps context src stmt kind e1;
- build_exp_deps context src stmt kind e2
-
-and build_lval_deps context src stmt kind lval =
- match build_lval context (Kstmt stmt) lval with
- | None -> ()
- | Some dst ->
- let allow_folding = true in
- Graph.create_dependency ~allow_folding context.graph dst kind src
+ build_alarm_deps callstack stmt alarm
+ | Cluster -> ()
+
(* --- Graph initialization --- *)
@@ -355,8 +389,10 @@ let create () =
graph = Graph.create ();
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;
roots = [];
}
@@ -387,7 +423,7 @@ let unhide_base context vi =
let should_auto_explore node =
match node.node_kind with
| Scalar _ | Composite _ | Alarm _ -> true
- | Scattered _ | File -> false
+ | Scattered _ | Cluster -> false
let complete_in_depth ~depth context root =
context.roots <- root :: context.roots;
@@ -411,13 +447,19 @@ let complete_in_depth ~depth context root =
done
let add_var ?(depth=1) context varinfo =
- let node = build_var context varinfo in
+ let callstack = [] in
+ let node = build_var context callstack varinfo in
Extlib.may (complete_in_depth ~depth context) node
let add_lval ?(depth=1) context kinstr lval =
- let node = build_lval context kinstr lval in
+ let callstack = match kinstr with
+ | Kglobal -> []
+ | 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
let add_alarm ?(depth=1) context stmt alarm =
- let node = build_alarm context stmt alarm in
+ let callstack = Callstack.init (Kernel_function.find_englobing_kf stmt) in
+ let node = build_alarm context callstack stmt alarm in
complete_in_depth ~depth context node
diff --git a/src/plugins/dive/callstack.ml b/src/plugins/dive/callstack.ml
new file mode 100644
index 00000000000..6a01ffb50e8
--- /dev/null
+++ b/src/plugins/dive/callstack.ml
@@ -0,0 +1,50 @@
+(**************************************************************************)
+(* *)
+(* 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
+
+include Value_types.Callstack
+
+type call_site = (Cil_types.kernel_function * Cil_types.kinstr)
+
+let init kf = [(kf,Kglobal)]
+
+let pop cs =
+ match cs with
+ | [] | (_,Kglobal) :: _ :: _ | [(_,Kstmt _)] -> assert false (* Invariant *)
+ | [(_,Kglobal)] -> None
+ | (kf,Kstmt stmt) :: t -> Some (kf,stmt,t)
+
+let rec pop_downto top_kf = function
+ | [] -> failwith "the callstack doesn't contain this function"
+ | ((kf,_kinstr) :: tail) as cs ->
+ if Kernel_function.equal kf top_kf
+ then cs
+ else pop_downto top_kf tail
+
+let push (kf,stmt) cs =
+ match cs with
+ (* When the callstack is truncated, we ignore the first callsite *)
+ | [] -> [(kf,Kglobal)]
+ | cs -> (kf,Kstmt stmt) :: cs
+
+
diff --git a/src/plugins/dive/callstack.mli b/src/plugins/dive/callstack.mli
new file mode 100644
index 00000000000..e5d55b8255d
--- /dev/null
+++ b/src/plugins/dive/callstack.mli
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+type call_site = (Cil_types.kernel_function * Cil_types.kinstr)
+type t = call_site list
+
+include Datatype.S_with_collections with type t := t
+
+(* The callstacks manipulated here have the following invariant:
+ - the callstack is never an empty list
+ - the last item of the list has alwas a Kglobal
+ - all elements of the list except the last have a Kstmt *)
+
+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
diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli
index cea36be39f2..e0b5eaf97b8 100644
--- a/src/plugins/dive/graph_types.mli
+++ b/src/plugins/dive/graph_types.mli
@@ -25,11 +25,11 @@ type node_kind =
| Composite of Cil_types.varinfo
| Scattered of Cil_types.lval
| Alarm of Cil_types.stmt * Alarms.alarm
- | File (* Dummy node, hack for Ocamlgraph Graphviz Dot module *)
+ | Cluster (* Dummy node, hack for Ocamlgraph Graphviz Dot module *)
type node_locality = {
loc_file : string;
- loc_function : Cil_types.kernel_function option;
+ loc_callstack : Callstack.t;
}
type node_precision = Unevaluated | Singleton | Normal | Wide | Critical
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
index ebb0ce5808c..c8685f2ea70 100644
--- a/src/plugins/dive/imprecision_graph.ml
+++ b/src/plugins/dive/imprecision_graph.ml
@@ -103,10 +103,11 @@ let ouptput_to_dot out_channel g =
let build_label s = `HtmlLabel (Extlib.html_escape s) in
let module FileTable = Datatype.String.Hashtbl in
- let module FunctionTable = Kernel_function.Hashtbl in
+ let module CallstackTable = Value_types.Callstack.Hashtbl in
let file_table = FileTable.create 13
- and function_table = FunctionTable.create 13 in
+ and callstack_table = CallstackTable.create 13 in
let file_counter = ref 0 in
+ let callstack_counter = ref 0 in
let rec build_file_subgraph filename =
incr file_counter;
{
@@ -114,16 +115,20 @@ let ouptput_to_dot out_channel g =
sg_attributes = [build_label filename];
sg_parent = None;
}
- and build_function_subgraph filename kf =
- {
- sg_name = "function_" ^ (string_of_int (Kernel_function.get_id kf));
- sg_attributes = [build_label (Kernel_function.get_name kf)];
- sg_parent = Some (get_file_subgraph filename).sg_name;
- }
+ and build_callstack_subgraph = function
+ | [] -> None
+ | (kf,_kinstr) :: stack ->
+ let parent = get_callstack_subgraph stack in
+ incr callstack_counter;
+ Some {
+ sg_name = "cs_" ^ (string_of_int !callstack_counter);
+ sg_attributes = [build_label (Kernel_function.get_name kf)];
+ sg_parent = Extlib.opt_map (fun sg -> sg.sg_name) parent;
+ }
and get_file_subgraph filename =
FileTable.memo file_table filename build_file_subgraph
- and get_function_subgraph filename kf =
- FunctionTable.memo function_table kf (build_function_subgraph filename)
+ and get_callstack_subgraph cs =
+ CallstackTable.memo callstack_table cs build_callstack_subgraph
in
let module Dot = Graph.Graphviz.Dot (
@@ -142,7 +147,7 @@ let ouptput_to_dot out_channel g =
| Composite _ -> [ `Shape `Box3d ]
| Scattered _ -> [ `Shape `Parallelogram ]
| Alarm _ -> [ `Shape `Doubleoctagon ; `Style `Bold ]
- | File -> [ `Style `Invis ]
+ | Cluster -> [ `Style `Invis ]
and precision = match v.node_precision with
| Unevaluated -> []
| Singleton -> [`Color 0x88aaff ;
@@ -159,10 +164,10 @@ let ouptput_to_dot out_channel g =
l := [ `Style `Dotted ] @ !l;
!l
let get_subgraph v =
- let {loc_file ; loc_function} = v.node_locality in
- match loc_function with
- | None -> Some (get_file_subgraph loc_file)
- | Some kf -> Some (get_function_subgraph loc_file kf)
+ let {loc_file ; loc_callstack} = v.node_locality in
+ match loc_callstack with
+ | [] -> Some (get_file_subgraph loc_file)
+ | cs -> get_callstack_subgraph cs
let default_edge_attributes _g = []
let edge_attributes (_v1,e,_v2) =
let kind_attribute = match e.dependency_kind with
@@ -177,20 +182,31 @@ let ouptput_to_dot out_channel g =
Dot.output_graph out_channel g
let ouptput_to_json out_channel g =
+ let rec output_kinstr = function
+ | Cil_types.Kglobal -> Json.of_string "global"
+ | Cil_types.Kstmt stmt -> Json.of_int stmt.Cil_types.sid
+ and output_callsite (kf,kinstr) =
+ Json.of_fields [
+ ("fun", Json.of_string (Kernel_function.get_name kf)) ;
+ ("instr", output_kinstr kinstr) ;
+ ]
+ and output_callstack cs =
+ Json.of_list (List.map output_callsite cs)
+ in
let output_node_kind kind =
let s = match kind with
| Scalar _ -> "scalar"
| Composite _ -> "composite"
| Scattered _ -> "scattered"
| Alarm _ -> "alarm"
- | File -> "dummy"
+ | Cluster -> "dummy"
in
Json.of_string s
- and output_node_locality { loc_file ; loc_function } =
+ and output_node_locality { loc_file ; loc_callstack } =
let f1 = ("file", Json.of_string loc_file) in
- let fields = match loc_function with
- | None -> [f1]
- | Some kf -> [f1 ; ("fun", Json.of_string (Kernel_function.get_name kf))]
+ let fields = match loc_callstack with
+ | [] -> [f1]
+ | cs -> [f1 ; ("fun", output_callstack cs)]
in
Json.of_fields fields
and output_node_precision precision =
@@ -212,7 +228,7 @@ let ouptput_to_json out_channel g =
Json.of_string s
in
let output_node node acc =
- if node.node_kind = File then acc
+ if node.node_kind = Cluster then acc
else
let label = Pretty_utils.to_string Node_kind.pretty node.node_kind in
Json.of_fields [
diff --git a/src/plugins/dive/node_kind.ml b/src/plugins/dive/node_kind.ml
index bbcf645bc16..2f68c93875f 100644
--- a/src/plugins/dive/node_kind.ml
+++ b/src/plugins/dive/node_kind.ml
@@ -24,7 +24,7 @@ open Graph_types
let get_base = function
| Scalar (vi,_,_) | Composite (vi) -> Some vi
- | Scattered _ | Alarm _ | File -> None
+ | Scattered _ | Alarm _ | Cluster -> None
let to_location = function
| Scalar (vi,typ,offset) ->
@@ -32,17 +32,17 @@ let to_location = function
Some (Locations.loc_of_typoffset base typ offset)
| Composite (vi) ->
Some (Locations.loc_of_varinfo vi)
- | Scattered _ | Alarm _ | File -> None
+ | Scattered _ | 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
- | Alarm (_,_) | File -> None
+ | Alarm (_,_) | Cluster -> None
let pretty fmt = function
| (Scalar _ | Composite _ | Scattered _) as kind ->
Cil_printer.pp_lval fmt (Extlib.the (to_lval kind))
| Alarm (_stmt,alarm) ->
Cil_printer.pp_predicate fmt (Alarms.create_predicate alarm)
- | File -> ()
+ | Cluster -> ()
diff --git a/src/plugins/dive/tests/dive/const.i b/src/plugins/dive/tests/dive/const.i
index 3534fa8e703..84c62df4f10 100644
--- a/src/plugins/dive/tests/dive/const.i
+++ b/src/plugins/dive/tests/dive/const.i
@@ -1,5 +1,5 @@
/* run.config
-STDOPT: +"-dive-from main::res -dive-depth-limit 5"
+STDOPT: +"-dive-from main::res -dive-depth-limit 4"
*/
int f(int x, int y)
diff --git a/src/plugins/dive/tests/dive/oracle/assigned_param.dot b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
index e988a3cdc4a..0f545f95df0 100644
--- a/src/plugins/dive/tests/dive/oracle/assigned_param.dot
+++ b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
@@ -1,25 +1,27 @@
digraph G {
cp0 [style="invis,dotted", ];
- cp1 [label=<w>, shape=box, ];
- cp2 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ cp1 [style="invis,dotted", ];
+ cp2 [label=<w>, shape=box, ];
+ cp3 [style="invis,dotted", ];
+ cp4 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
- cp3 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ cp5 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
style="filled", ];
- cp4 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ cp6 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
style="filled", ];
- cp5 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ cp7 [label=<z>, shape=box, fillcolor="#EEFFEE", color="#004400",
style="filled", ];
- 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;
+ subgraph cluster_cs_1 { label=<main>; cp7;cp6;cp2;cp1;
+ subgraph cluster_cs_2 { label=<f>; cp5;cp4;cp3;
};
};
+ subgraph cluster_file_1 { label=<tests/dive/assigned_param.i>; cp0;
+ };
- cp2 -> cp1;
- cp3 -> cp2;
cp4 -> cp2;
- cp5 -> cp3;
+ cp5 -> cp4;
+ 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 ddf007a23e7..4921853943c 100644
--- a/src/plugins/dive/tests/dive/oracle/const.dot
+++ b/src/plugins/dive/tests/dive/oracle/const.dot
@@ -1,35 +1,34 @@
digraph G {
cp0 [style="invis,dotted", ];
- cp1 [label=<res>, shape=box, ];
- cp2 [style="invis,dotted", ];
- cp3 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ cp1 [style="invis,dotted", ];
+ cp2 [label=<res>, shape=box, ];
+ cp3 [style="invis,dotted", ];
+ cp4 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
- cp4 [label=<c>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ cp5 [label=<c>, shape=box, fillcolor="#EEFFEE", color="#004400",
style="filled", ];
- cp5 [label=<w>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ cp6 [label=<w>, shape=box, fillcolor="#EEFFEE", color="#004400",
style="filled", ];
- cp6 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ cp7 [label=<x>, shape=box, fillcolor="#EEFFEE", color="#004400",
style="filled", ];
- cp7 [label=<y>, shape=box, fillcolor="#EEFFEE", color="#004400",
- style="filled", ];
- cp8 [label=<i>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ cp8 [label=<y>, shape=box, fillcolor="#EEFFEE", color="#004400",
style="filled", ];
+ cp9 [label=<i>, shape=box, fillcolor="#EEFFEE", color="#004400",
+ style="filled,dotted", ];
- subgraph cluster_file_1 { label=<tests/dive/const.i>; cp0;
- subgraph cluster_function_25 { label=<main>; cp8;cp1;
+ subgraph cluster_cs_1 { label=<main>; cp9;cp2;cp1;
+ subgraph cluster_cs_2 { label=<f>; cp8;cp7;cp6;cp5;cp4;cp3;
};
};
- subgraph cluster_file_2 { label=<>; cp2;
- subgraph cluster_function_18 { label=<f>; cp7;cp6;cp5;cp4;cp3;
- };
+ subgraph cluster_file_1 { label=<tests/dive/const.i>; cp0;
};
- cp3 -> cp1;
- cp4 -> cp3;
- cp5 -> cp3;
+ cp4 -> cp2;
+ cp5 -> cp4;
cp6 -> cp4;
cp7 -> cp5;
cp8 -> cp6;
- cp8 -> cp7;
+ cp9 -> cp7;
+ cp9 -> cp8;
}
\ 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
new file mode 100644
index 00000000000..cc0432dfdae
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/pointed_param.dot
@@ -0,0 +1,36 @@
+digraph G {
+ cp0 [style="invis,dotted", ];
+ cp1 [style="invis,dotted", ];
+ cp2 [label=<y>, shape=box, ];
+ cp3 [label=<tmp>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp4 [style="invis,dotted", ];
+ cp5 [label=<tmp>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp6 [style="invis,dotted", ];
+ cp7 [label=<tmp>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp8 [style="invis,dotted", ];
+ cp9 [label=<__retres>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp10 [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_file_1 { label=<tests/dive/pointed_param.i>; cp0;
+ };
+
+ cp3 -> cp2;
+ cp5 -> cp3;
+ cp7 -> cp5;
+ cp9 -> cp7;
+ cp10 -> cp9;
+
+ }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/pointed_param.res.oracle b/src/plugins/dive/tests/dive/oracle/pointed_param.res.oracle
new file mode 100644
index 00000000000..267eca08a19
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/pointed_param.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing tests/dive/pointed_param.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/pointed_param.dot
diff --git a/src/plugins/dive/tests/dive/oracle/unfocused_callers.dot b/src/plugins/dive/tests/dive/oracle/unfocused_callers.dot
new file mode 100644
index 00000000000..17fe2165025
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/unfocused_callers.dot
@@ -0,0 +1,38 @@
+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",
+ style="filled", ];
+ cp5 [style="invis,dotted", ];
+ cp6 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp7 [style="invis,dotted", ];
+ cp8 [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_3 { label=<f2>; cp6;cp5;
+ };
+ subgraph cluster_cs_4 { label=<f1>; cp8;cp7;
+ };
+ subgraph cluster_cs_5 { label=<main>; cp10;cp9;
+ };
+ subgraph cluster_file_1 { label=<tests/dive/unfocused_callers.i>; cp0;
+ };
+
+ cp4 -> cp2;
+ cp6 -> cp2;
+ cp8 -> cp2;
+ cp10 -> cp4;
+ cp10 -> cp6;
+ cp10 -> cp8;
+
+ }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/unfocused_callers.res.oracle b/src/plugins/dive/tests/dive/oracle/unfocused_callers.res.oracle
new file mode 100644
index 00000000000..afebc6fd738
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/unfocused_callers.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/dive/unfocused_callers.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:alarm] tests/dive/unfocused_callers.i:16: Warning:
+ non-finite float value.
+ assert \is_finite((float)(tmp + tmp_0));
+ (tmp from f1(x), tmp_0 from f2(x))
+[eva:alarm] tests/dive/unfocused_callers.i:16: Warning:
+ non-finite float value.
+ assert \is_finite((float)((float)(tmp + tmp_0) + tmp_1));
+ (tmp from f1(x), tmp_0 from f2(x), tmp_1 from f3(x))
+[eva] done for function main
+[dive] output to tests/dive/result/unfocused_callers.dot
diff --git a/src/plugins/dive/tests/dive/oracle/various.dot b/src/plugins/dive/tests/dive/oracle/various.dot
index d8595e7b16c..9ed41e39557 100644
--- a/src/plugins/dive/tests/dive/oracle/various.dot
+++ b/src/plugins/dive/tests/dive/oracle/various.dot
@@ -1,48 +1,73 @@
digraph G {
cp0 [style="invis,dotted", ];
- cp1 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ cp1 [style="invis,dotted", ];
+ cp2 [label=<x2>, shape=box, ];
+ cp3 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
- cp2 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ cp4 [style="invis,dotted", ];
+ cp5 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
- cp3 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ cp6 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
style="filled", ];
- cp4 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ cp7 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
style="filled", ];
- cp5 [label=<z>, shape=box, ];
- cp6 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ cp8 [label=<z>, shape=box, ];
+ cp9 [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", ];
- cp10 [label=<is_nan_or_infinite: \is_finite((float)((double)((double)y * 2.0)))>,
+ cp10 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp11 [style="invis,dotted", ];
+ cp12 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp13 [label=<tmp_0>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp14 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp15 [label=<pf>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp16 [style="invis,dotted", ];
+ cp17 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp18 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp19 [label=<is_nan_or_infinite: \is_finite((float)((double)((double)y * 2.0)))>,
shape=doubleoctagon, fillcolor="#FF0000", color="#FF0000",
style="bold,filled,bold", ];
- cp11 [label=<is_nan_or_infinite: \is_finite((float)(y + w))>,
+ cp20 [label=<is_nan_or_infinite: \is_finite((float)(y + w))>,
shape=doubleoctagon, fillcolor="#FF0000", color="#FF0000",
style="bold,filled,bold", ];
- subgraph cluster_file_1 { label=<tests/dive/various.i>; cp4;cp0;
- subgraph cluster_function_19 { label=<f>; cp10;cp2;cp1;
+ subgraph cluster_cs_1 { label=<f>; cp19;cp6;cp3;cp2;cp1;
+ };
+ 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_function_24 { label=<main>; cp11;cp9;cp8;cp7;cp6;cp5;cp3;
+ subgraph cluster_cs_4 { label=<f>; cp18;cp17;cp16;
};
};
+ subgraph cluster_file_1 { label=<tests/dive/various.i>; cp7;cp0;
+ };
- cp1 -> cp2;
- cp1 -> cp6;
- cp1 -> cp8;
- cp2 -> cp1;
- cp2 -> cp10;
- cp3 -> cp1;
- cp4 -> cp3;
- cp6 -> cp5;
- cp6 -> cp11;
+ cp3 -> cp2;
+ cp3 -> cp6;
+ cp3 -> cp19;
+ cp5 -> cp2;
+ cp5 -> cp6;
+ cp5 -> cp12;
+ cp5 -> cp17;
+ cp6 -> cp3;
cp7 -> cp5;
- cp7 -> cp11;
- cp8 -> cp7;
- cp9 -> cp8 [color="#00FF00", ];
+ cp9 -> cp8;
+ cp9 -> cp20;
+ cp10 -> cp8;
+ cp10 -> cp20;
+ cp12 -> cp9;
+ cp12 -> cp14;
+ cp13 -> cp10;
+ cp14 -> cp12;
+ cp15 -> cp13 [color="#00FF00", ];
+ cp17 -> cp13;
+ cp17 -> cp18;
+ cp18 -> cp17;
}
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/pointed_param.i b/src/plugins/dive/tests/dive/pointed_param.i
new file mode 100644
index 00000000000..3a47e7648f4
--- /dev/null
+++ b/src/plugins/dive/tests/dive/pointed_param.i
@@ -0,0 +1,25 @@
+/* run.config
+STDOPT: +"-dive-from main::y -dive-depth-limit 5"
+*/
+
+float h(float *p)
+{
+ return *p - 1;
+}
+
+float g(float *p)
+{
+ return h(p);
+}
+
+float f(float x)
+{
+ return g(&x);
+}
+
+float main(float x)
+{
+ float y = f(x) + 1;
+ return y;
+}
+
diff --git a/src/plugins/dive/tests/dive/unfocused_callers.i b/src/plugins/dive/tests/dive/unfocused_callers.i
new file mode 100644
index 00000000000..f61e8438737
--- /dev/null
+++ b/src/plugins/dive/tests/dive/unfocused_callers.i
@@ -0,0 +1,19 @@
+/* run.config
+STDOPT: +"-dive-from g::x -dive-depth-limit 7"
+*/
+
+float g(float x) {
+ float y = x + 1;
+ return y;
+}
+
+float f1(float x) { return g(x); }
+float f2(float x) { return g(x); }
+float f3(float x) { return g(x); }
+
+float main(float x)
+{
+ float z = f1(x) + f2(x) + f3(x);
+ return z;
+}
+
diff --git a/src/plugins/dive/tests/test_config b/src/plugins/dive/tests/test_config
index 2baab62a7d7..6a140cd0a50 100644
--- a/src/plugins/dive/tests/test_config
+++ b/src/plugins/dive/tests/test_config
@@ -1,2 +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@
+OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope,dive -check -eva-msg-key=-initial-state -eva-no-show-progress -dive-output-dot @PTEST_RESULT@/@PTEST_NAME@
--
GitLab