diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 32832478186a2582d8a38acfd8cee26c3b43367c..7fdecae8316b409d5dc49098688c2cf5cd52f1a9 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -763,6 +763,23 @@ src/plugins/constant_propagation/propagationParameters.ml: CEA_LGPL_OR_PROPRIETA
src/plugins/constant_propagation/propagationParameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/constant_propagation/api.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/constant_propagation/api.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/build.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/build.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/callstack.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/callstack.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/configure.ac: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/Dive.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/graph_types.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/imprecision_graph.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/imprecision_graph.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/main.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/Makefile.in: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/node_kind.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/node_kind.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/self.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/self.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/server_interface.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/server_interface.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/from/From.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/from/callwise.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/from/callwise.mli: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/dive/.gitignore b/src/plugins/dive/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..b9f44a02f3c684cc2b3080dc8d5e96a4e758cf1a
--- /dev/null
+++ b/src/plugins/dive/.gitignore
@@ -0,0 +1,3 @@
+/Makefile
+/tests/*/result
+/tests/ptests_config
diff --git a/src/plugins/dive/Dive.mli b/src/plugins/dive/Dive.mli
new file mode 100644
index 0000000000000000000000000000000000000000..182bc40a8e1af00f6d1329952d449d0f2e6808e1
--- /dev/null
+++ b/src/plugins/dive/Dive.mli
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
diff --git a/src/plugins/dive/Makefile.in b/src/plugins/dive/Makefile.in
new file mode 100644
index 0000000000000000000000000000000000000000..1609a95d3178f2a00f289b029af915220d16f2e6
--- /dev/null
+++ b/src/plugins/dive/Makefile.in
@@ -0,0 +1,71 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2020 #
+# 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). #
+# #
+##########################################################################
+
+#######################
+# Frama-C Environment #
+#######################
+
+ifndef FRAMAC_SHARE
+FRAMAC_SHARE := $(shell frama-c-config -print-share-path)
+endif
+
+ifndef FRAMAC_LIBDIR
+FRAMAC_LIBDIR := $(shell frama-c-config -print-libpath)
+endif
+
+#########################
+# Plug-in configuration #
+#########################
+
+PLUGIN_DIR ?=.
+PLUGIN_ENABLE:=@ENABLE_DIVE@
+PLUGIN_NAME := Dive
+PLUGIN_CMO := self callstack node_kind imprecision_graph build main \
+ server_interface
+PLUGIN_CMI:= graph_types
+PLUGIN_DEPENDENCIES:= Eva Studia Server
+PLUGIN_HAS_MLI:= yes
+PLUGIN_TESTS_DIRS:=dive
+PLUGIN_GENERATED:=
+PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
+PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
+
+################
+# Generic part #
+################
+
+include $(FRAMAC_SHARE)/Makefile.dynamic
+
+#####################################
+# Regenerating the Makefile on need #
+#####################################
+
+ifeq ("$(FRAMAC_INTERNAL)","yes")
+CONFIG_STATUS_DIR:=$(FRAMAC_SRC)
+CONFIG_STATUS_DIR_DEP:=
+else
+CONFIG_STATUS_DIR:=$(Dive_DIR)
+CONFIG_STATUS_DIR_DEP:=$(CONFIG_STATUS_DIR)/config.status
+endif
+
+$(Dive_DIR)/Makefile: $(Dive_DIR)/Makefile.in $(CONFIG_STATUS_DIR_DEP)
+ cd $(CONFIG_STATUS_DIR) && ./config.status --file $@
diff --git a/src/plugins/dive/README.md b/src/plugins/dive/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..b90cf22dfb9738630b201e97e25d7e6867fd170a
--- /dev/null
+++ b/src/plugins/dive/README.md
@@ -0,0 +1,17 @@
+Dive is a Frama-C plugin specialized in the visualization of data dependencies.
+It is intended to help the user find the origin of an imprecision in an Eva
+analysis.
+
+
+Dependencies
+============
+
+The front-end of Dive relies on several external tools and libraries :
+
+- Node.js: a runtime environment for javascript to run programs outside a
+ browser
+- yarn: a package manager for javascript modules written for Node.js
+- electron: a javascript framework for gui applications
+- Ivette: the future Frama-C GUI
+- Cytoscape: a javascript library to display graphs and interact with them
+- Zmq: a multilanguage framework for common simple networking patterns
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
new file mode 100644
index 0000000000000000000000000000000000000000..236582ae1ad1e06d21eac2f065347021e7c06d7e
--- /dev/null
+++ b/src/plugins/dive/build.ml
@@ -0,0 +1,645 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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
+open Graph_types
+
+let dkey = Self.register_category "build"
+
+exception Too_many_deps
+
+
+(* --- Precision evaluation --- *)
+
+let _fval_contains_maximal_bounds fkind fval =
+ let top = Fval.top_finite (Fval.kind fkind) in
+ Fval.has_greater_min_bound top fval >= 0 ||
+ Fval.has_smaller_max_bound top fval >= 0
+
+let fkind_limits =
+ let max_single = float_of_string "0x1.fffffep+127"
+ and max_double = float_of_string "0x1.fffffffffffffp+1023" in
+ let single_limits = { min = -. max_single ; max = max_single }
+ and double_limits = { min = -. max_double ; max = max_double } in
+ function
+ | FFloat -> single_limits
+ | FDouble -> double_limits
+ | FLongDouble -> assert false
+
+let float_grade_limits =
+ let single = float_of_string "0x1p+120"
+ and double = float_of_string "0x1p+960"
+ and long_double = float_of_string "0x1p+15360"
+ in function
+ | FFloat -> single
+ | FDouble -> double
+ | FLongDouble -> long_double
+
+let is_large_float_range fkind (min,max) =
+ let limit = float_grade_limits fkind in
+ if (min < 0.0) = (max < 0.0) then (* if bounds have same sign *)
+ max -. min >= limit
+ else
+ min <= -.limit || max >= limit
+
+let float_grade fkind (min,max) =
+ if min = max then
+ Singleton
+ else if is_large_float_range fkind (min,max) then
+ Wide
+ else
+ Normal
+
+let ikind_limits ikind =
+ let open Cil in
+ let bits = bitsSizeOfInt ikind in
+ if isSigned ikind then
+ { min=min_signed_number bits; max=max_signed_number bits }
+ else
+ { min=Integer.zero; max=max_unsigned_number bits }
+
+let int_grade_limits ikind =
+ let bits = Cil.bitsSizeOfInt ikind in
+ Integer.(pred (two_power_of_int (bits - bits / 8)))
+
+let is_large_int_range ikind (l,u) =
+ let limit = int_grade_limits ikind in
+ if Integer.(lt l zero) = Integer.(lt u zero) then (* if bounds have same sign *)
+ Integer.(ge (sub u l) limit)
+ else
+ Integer.(le l (neg limit)) || Integer.(ge u limit)
+
+let int_grade ikind (min,max) =
+ if min = max then
+ Singleton
+ else if is_large_int_range ikind (min,max) then
+ Wide
+ else
+ Normal
+
+
+let update_node_values node kinstr lval =
+ let typ = Cil.typeOfLval lval in
+ let state = Db.Value.get_state kinstr in
+ let _,cvalue = !Db.Value.eval_lval None state lval in
+ try
+ let ival = Cvalue.V.project_ival cvalue in
+ match typ with
+ | TInt (ikind,_) ->
+ let size = Integer.of_int (Cil.bitsSizeOfInt ikind)
+ and signed = Cil.isSigned ikind in
+ let ival = Ival.reinterpret_as_int ~size ~signed ival in
+ let min, max = match Ival.min_and_max ival with
+ | Some min, Some max -> min, max
+ | _, _ -> assert false (* ival have been reinterpreted *)
+ in
+ Imprecision_graph.update_node_int_values node {
+ values_interval = {min;max};
+ values_limits = ikind_limits ikind;
+ values_grade = int_grade ikind (min,max)
+ }
+
+ | TFloat (fkind,_) ->
+ begin match Ival.min_and_max_float ival with
+ | None, _can_be_nan -> ()
+ | Some (min, max), _can_be_nan ->
+ let min = Fval.F.to_float min and max = Fval.F.to_float max in
+ Imprecision_graph.update_node_float_values node {
+ values_interval = {min;max};
+ values_limits = fkind_limits fkind;
+ values_grade = float_grade fkind (min,max);
+ }
+ end
+ | _ -> ()
+ with Cvalue.V.Not_based_on_null -> ()
+
+
+(* --- Locations handling --- *)
+
+let get_loc_filename loc =
+ Filepath.(Normalized.to_pretty_string (fst loc).pos_path)
+
+let is_foldable_type typ =
+ match Cil.unrollType typ with
+ | TArray _ | TComp _ -> true
+ | TVoid _ | TInt _ | TEnum _ | TFloat _ | TPtr _ | TFun _
+ | TBuiltin_va_list _ -> false
+ | TNamed _ -> assert false (* the type have been unrolled *)
+
+exception NoMatchingOffset
+
+let cell_to_scalar typ vi offset =
+ (* TODO: exceptions must be shown to the user somehow *)
+ try
+ let matching = Bit_utils.MatchType typ in
+ let offset', _ = Bit_utils.find_offset vi.vtype ~offset matching in
+ Scalar (vi, typ, offset')
+ with Bit_utils.NoMatchingOffset -> raise NoMatchingOffset
+
+exception NotACell
+
+let enumerate_cells ~is_folded_base ~limit lval kinstr =
+ (* TODO: non-variable bases must be shown to the user somehow *)
+ (* TODO: exceptions must be shown to the user somehow *)
+ (* If possible, refine the lval to a non-symbolic one *)
+ let location = !Db.Value.lval_to_loc kinstr lval
+ and typ = Cil.typeOfLval lval in
+ let open Locations in
+ let add (acc,count) node_kind =
+ if count > limit then
+ raise Too_many_deps;
+ (node_kind :: acc, count+1)
+ in
+ let add_base base ival (acc,count) =
+ match base with
+ | Base.Var (vi,_) ->
+ begin
+ if is_foldable_type vi.vtype && is_folded_base vi then
+ add (acc,count) (Composite (vi))
+ else
+ let add_cells offset (acc,count) =
+ add (acc,count) (cell_to_scalar typ vi offset)
+ in
+ try
+ Ival.fold_int add_cells ival (acc,count)
+ with Abstract_interp.Error_Top -> raise NotACell
+ end
+ | _ -> raise NotACell
+ in
+ try
+ fst (Location_Bits.fold_i add_base location.loc ([],0))
+ with Abstract_interp.Error_Top | NoMatchingOffset -> raise NotACell
+
+let build_node_kind ~is_folded_base lval kinstr =
+ match enumerate_cells ~is_folded_base ~limit:1 lval kinstr with
+ | [node_kind] -> node_kind
+ | _ -> Scattered (lval, kinstr)
+ | exception NotACell -> Scattered (lval, kinstr)
+
+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 callstack node_kind =
+ match Node_kind.get_base node_kind with
+ | None -> default_node_locality callstack
+ | Some vi ->
+ 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
+ (Node_kind) (Callstack)
+ (struct let module_name = "Build.NodeRef" end)
+
+module Graph = Imprecision_graph
+module Index = Datatype.Int.Hashtbl
+module NodeTable = FCHashtbl.Make (NodeRef)
+module BaseSet = Cil_datatype.Varinfo.Set
+module FunctionMap = Kernel_function.Map
+
+type t = {
+ mutable graph: Graph.t;
+ mutable vertex_table: node Index.t;
+ mutable node_table: node NodeTable.t;
+ mutable unfolded_bases: BaseSet.t;
+ mutable hidden_bases: BaseSet.t;
+ mutable focus: bool FunctionMap.t;
+ mutable roots: node list;
+ 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 find_node context node_key =
+ Index.find context.vertex_table node_key
+
+let update_node context node =
+ if
+ not (List.exists (Graph.Node.equal node) context.graph_diff.added_nodes)
+ then
+ context.graph_diff <- {
+ context.graph_diff with
+ added_nodes = node :: context.graph_diff.added_nodes
+ }
+
+let add_node context ~node_kind ~node_locality =
+ 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 node_ref = (node.node_kind, node.node_locality.loc_callstack) in
+ Graph.remove_node context.graph node;
+ 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
+ }
+
+
+(* --- Graph building --- *)
+
+let add_or_update_node context callstack node_kind =
+ let node_locality = build_node_locality callstack node_kind in
+ add_node context ~node_kind ~node_locality
+
+let build_node context callstack lval kinstr =
+ let is_folded_base = is_folded context in
+ let node_kind = build_node_kind ~is_folded_base lval kinstr in
+ add_or_update_node context callstack node_kind
+
+let build_all_scattered_node context callstack kinstr lval =
+ let is_folded_base = is_folded context in
+ try
+ let cells = enumerate_cells ~is_folded_base ~limit:20 lval kinstr in
+ let add node_kind =
+ let node = add_or_update_node context callstack node_kind in
+ let new_lval = Extlib.the (Node_kind.to_lval node_kind) in
+ update_node_values node kinstr new_lval;
+ node
+ in
+ List.map add cells
+ with NotACell ->
+ Self.warning "Unable to enumerate cells for %a"
+ Cil_printer.pp_lval lval;
+ []
+
+let build_var context callstack varinfo =
+ let lval = Var varinfo, NoOffset in
+ build_node context callstack lval Kglobal
+
+let build_lval context callstack kinstr lval =
+ let node = build_node context callstack lval kinstr in
+ update_node_values node kinstr lval;
+ node
+
+let build_alarm context callstack stmt alarm =
+ let node_kind = Alarm (stmt,alarm) in
+ let node_locality = build_node_locality callstack node_kind in
+ add_node context ~node_kind ~node_locality
+
+let build_node_deps context node =
+ let rec build_lval_write_deps callstack kinstr lval =
+ let zone = !Db.Value.lval_to_zone kinstr lval in
+ build_write_deps callstack zone
+
+ and build_write_deps callstack zone =
+ Self.debug ~dkey "computing deps for %a" Node_kind.pretty node.node_kind;
+ let writes = Studia.Writes.compute zone
+ and add_deps (stmt,effects) =
+ match stmt.skind with
+ | Instr _ when not effects.Studia.Writes.direct -> ()
+ | Instr instr ->
+ let callstacks =
+ if callstack <> [] &&
+ Kernel_function.(equal
+ (find_englobing_kf stmt)
+ (Callstack.top_kf callstack))
+ then
+ (* slight improvement which only work when there is no recursion
+ and which is only usefull because you currently can't have
+ all callstacks due to memexec -> in this particular case
+ we are sure not to miss the only admissible callstack *)
+ [callstack]
+ else
+ (* 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 *)
+ 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;
+ if count > 20 then
+ raise Too_many_deps
+ 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},_)} as return_stmt ->
+ let callstack = Callstack.push (kf,stmt) callstack in
+ build_lval_deps callstack return_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,_) | Invalid_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 =
+ let dst = build_lval context callstack (Kstmt stmt) lval in
+ Graph.create_dependency ~allow_folding:true context.graph dst kind node
+
+ and build_scattered_deps callstack kinstr lval =
+ let nodes = build_all_scattered_node context callstack kinstr lval in
+ let kind = Composition in
+ let add_dep dst =
+ Graph.create_dependency ~allow_folding:true context.graph dst kind node
+ in
+ List.iter add_dep nodes
+
+ in
+ update_node context node;
+ let callstack = node.node_locality.loc_callstack in
+ begin match node.node_kind with
+ | Scalar (vi,_typ,offset) ->
+ let lval = (Cil_types.Var vi, offset) in
+ build_lval_write_deps callstack Kglobal lval
+ | Composite (vi) ->
+ let lval = (Cil_types.Var vi, Cil_types.NoOffset) in
+ build_lval_write_deps callstack Kglobal lval
+ | Scattered (lval,kinstr) ->
+ build_scattered_deps callstack kinstr lval
+ | Alarm (stmt,alarm) ->
+ build_alarm_deps callstack stmt alarm
+ end;
+ begin match Node_kind.get_base node.node_kind with
+ (* TODO refine formal dependency computation for non-scalar formals *)
+ | Some vi when vi.vformal -> build_arg_deps callstack vi
+ | _ -> ()
+ end
+
+
+(* --- Graph initialization --- *)
+
+let create () =
+ !Db.Value.compute ();
+ {
+ graph = Graph.create ();
+ vertex_table = Index.create 13;
+ node_table = NodeTable.create 13;
+ unfolded_bases = BaseSet.empty;
+ hidden_bases = BaseSet.empty;
+ focus = FunctionMap.empty;
+ roots = [];
+ graph_diff = { added_nodes=[] ; removed_nodes=[] };
+ }
+
+let clear context =
+ context.graph <- Graph.create ();
+ context.vertex_table <- Index.create 13;
+ context.node_table <- NodeTable.create 13;
+ context.focus <- FunctionMap.empty;
+ context.roots <- [];
+ context.graph_diff <- { added_nodes=[] ; removed_nodes=[] }
+
+
+(* --- Accessors --- *)
+
+let get_graph context =
+ context.graph
+
+let get_roots context =
+ context.roots
+
+
+(* --- Mutators --- *)
+
+let unfold_base context vi =
+ context.unfolded_bases <- BaseSet.add vi context.unfolded_bases
+
+let fold_base context vi =
+ context.unfolded_bases <- BaseSet.remove vi context.unfolded_bases
+
+let hide_base context vi =
+ context.hidden_bases <- BaseSet.add vi context.hidden_bases
+
+let unhide_base context vi =
+ context.hidden_bases <- BaseSet.add vi context.hidden_bases
+
+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 _ -> 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
+ begin try
+ build_node_deps context n;
+ with Too_many_deps ->
+ (* TODO: give a mean to explore more dependencies *)
+ Self.warning "Too many dependencies for %a ; throwing them out"
+ Node_kind.pretty n.node_kind;
+ end;
+ n.node_deps_computed <- true;
+ end;
+ Graph.iter_pred (fun n' -> Queue.add (n',d+1) queue) context.graph n
+ end;
+ done
+
+let complete_in_depth ~depth context root =
+ context.roots <- root :: context.roots;
+ explore ~depth context root
+
+let add_var ?(depth=1) context varinfo =
+ let callstack = [] in
+ let node = build_var context callstack varinfo in
+ complete_in_depth ~depth context node
+
+let add_lval ?(depth=1) context kinstr lval =
+ 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
+ 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
+ let node = build_alarm context callstack stmt alarm in
+ complete_in_depth ~depth context node
+
+let add_function_alarms ?(depth=1) context kf =
+ let add_one_alarm _emitter kf' stmt ~rank:_ alarm _code_annot =
+ if Kernel_function.equal kf' kf then
+ add_alarm ~depth context stmt alarm
+ in
+ Alarms.iter add_one_alarm
+
+let explore_from_node ~depth context node =
+ explore ~depth context node
+
+let show ?(depth=1) context node =
+ node.node_hidden <- false;
+ explore ~depth context node
+
+let hide context node =
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..990e3e6f89cf5916b7abd11f2acbb360a16cc448
--- /dev/null
+++ b/src/plugins/dive/build.mli
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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 t
+
+val create : unit -> t
+val clear : t -> unit (* reset to almost an empty context,
+ but keeps folded and hidden bases *)
+
+val get_graph : t -> Imprecision_graph.t
+val get_roots : t -> Graph_types.node list
+
+val unfold_base : t -> Cil_types.varinfo -> unit
+val fold_base : t -> Cil_types.varinfo -> unit
+val hide_base : t -> Cil_types.varinfo -> unit
+val unhide_base : t -> Cil_types.varinfo -> unit
+
+val find_node : t -> int -> Graph_types.node
+
+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 add_function_alarms : ?depth:int -> t -> Cil_types.kernel_function -> unit
+val explore_from_node : depth:int -> t -> Graph_types.node -> unit
+
+val show : ?depth:int -> t -> Graph_types.node -> unit
+val hide : t -> Graph_types.node -> unit
+
+val take_last_differences : t -> Graph_types.graph_diff
diff --git a/src/plugins/dive/callstack.ml b/src/plugins/dive/callstack.ml
new file mode 100644
index 0000000000000000000000000000000000000000..8b25837a11357d83f0dd791d749baf2e11225b77
--- /dev/null
+++ b/src/plugins/dive/callstack.ml
@@ -0,0 +1,86 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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 = Value_types.call_site
+module Callsite = Value_types.Callsite
+
+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 top_kf cs =
+ match cs with
+ | [] | (_,Kglobal) :: _ :: _ | [(_,Kstmt _)] -> assert false (* Invariant *)
+ | (kf,_) :: _ -> kf
+
+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
+
+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
new file mode 100644
index 0000000000000000000000000000000000000000..48d3a417b9614086235ce292a695fc084efd16b0
--- /dev/null
+++ b/src/plugins/dive/callstack.mli
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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 always 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 top_kf : t -> Cil_types.kernel_function
+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/configure.ac b/src/plugins/dive/configure.ac
new file mode 100644
index 0000000000000000000000000000000000000000..dddb5ed24e2092387c4c801ab35f0a3d061f8b41
--- /dev/null
+++ b/src/plugins/dive/configure.ac
@@ -0,0 +1,50 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2020 #
+# 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). #
+# #
+##########################################################################
+
+m4_define([plugin_file],Makefile.in)
+
+m4_define([FRAMAC_SHARE_ENV],
+ [m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
+
+m4_define([FRAMAC_SHARE],
+ [m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
+ [m4_esyscmd(frama-c -print-path)])])
+
+m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
+
+check_plugin(dive,PLUGIN_RELATIVE_PATH(plugin_file),
+ [support for Dive plug-in],yes)
+
+# Plug-in dependencies
+######################
+
+plugin_require(dive,eva)
+plugin_require(dive,studia)
+#plugin_use(dive,usable_plugin_but_not_mandatory)
+
+check_plugin_dependencies
+
+#######################
+# Generating Makefile #
+#######################
+
+write_plugin_config(Makefile)
diff --git a/src/plugins/dive/graph_types.mli b/src/plugins/dive/graph_types.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f1920b35026e847eaa92a1921861890d3087a590
--- /dev/null
+++ b/src/plugins/dive/graph_types.mli
@@ -0,0 +1,65 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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 node_kind =
+ | Scalar of Cil_types.varinfo * Cil_types.typ * Cil_types.offset
+ | Composite of Cil_types.varinfo
+ | Scattered of Cil_types.lval * Cil_types.kinstr
+ | Alarm of Cil_types.stmt * Alarms.alarm
+
+type node_locality = {
+ loc_file : string;
+ loc_callstack : Callstack.t;
+}
+
+type 'a interval = {min: 'a; max: 'a}
+
+type precision_grade = Singleton | Normal | Wide
+
+type 'a node_values = {
+ values_interval : 'a interval;
+ values_limits : 'a interval;
+ values_grade : precision_grade;
+}
+
+type node = {
+ node_key : int;
+ node_kind : node_kind;
+ node_locality : node_locality;
+ mutable node_hidden : bool;
+ mutable node_int_values : (Integer.t node_values) option;
+ mutable node_float_values : (float node_values) option;
+ mutable node_deps_computed : bool;
+}
+
+type dependency_kind = Callee | Data | Address | Control | Composition
+
+type dependency = {
+ dependency_key : int;
+ dependency_kind : dependency_kind;
+ mutable dependency_multiple : bool;
+}
+
+type graph_diff = {
+ added_nodes: node list;
+ removed_nodes: node list;
+}
diff --git a/src/plugins/dive/imprecision_graph.ml b/src/plugins/dive/imprecision_graph.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2ebd12cf182b051b49c551f7a1dd71d7b3b7c7b4
--- /dev/null
+++ b/src/plugins/dive/imprecision_graph.ml
@@ -0,0 +1,401 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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
+
+module Node =
+struct
+ type t = node
+ let compare v1 v2 = v1.node_key - v2.node_key
+ let hash v = v.node_key
+ let equal v1 v2 = v1.node_key = v2.node_key
+end
+
+module Dependency =
+struct
+ type t = dependency
+ let compare e1 e2 = e1.dependency_key - e2.dependency_key
+ let hash e = e.dependency_key
+ let equal e1 e2 = e1.dependency_key = e2.dependency_key
+ let default = {
+ dependency_key = -1;
+ dependency_kind = Data;
+ dependency_multiple = false;
+ }
+end
+
+module G =
+ Graph.Imperative.Digraph.ConcreteBidirectionalLabeled (Node) (Dependency)
+include G
+
+let vertices g =
+ fold_vertex (fun n acc -> n ::acc) g []
+
+let edges g =
+ fold_edges_e (fun d acc -> d ::acc) g []
+
+let next_key = ref 0
+
+let create_node ~node_kind ~node_locality g =
+ let node = {
+ node_key = !next_key;
+ node_kind;
+ node_locality;
+ node_hidden = false;
+ node_int_values = None;
+ node_float_values = None;
+ node_deps_computed = false;
+ }
+ in
+ incr next_key;
+ add_vertex g node;
+ node
+
+let remove_node = remove_vertex
+
+let union_int_interval i1 i2 =
+ { min = Integer.min i1.min i2.min ; max = Integer.max i1.max i2.max }
+
+let union_float_interval i1 i2 =
+ { min = min i1.min i2.min ; max = max i1.max i2.max }
+
+let worst_precision_grade q1 q2 =
+ match q1, q2 with
+ | Wide, _ | _, Wide -> Wide
+ | Normal, _ | _, Normal -> Normal
+ | Singleton, Singleton -> Singleton
+
+let merge_int_values p1 p2 =
+ (* TODO: prevent assertion failure *)
+ assert (Integer.equal p1.values_limits.min p2.values_limits.min);
+ assert (Integer.equal p1.values_limits.max p2.values_limits.max);
+ {
+ values_interval = union_int_interval p1.values_interval p2.values_interval;
+ values_limits = p1.values_limits;
+ values_grade = worst_precision_grade p1.values_grade p2.values_grade;
+ }
+
+let merge_float_values p1 p2 =
+ (* TODO: prevent assertion failure *)
+ assert (p1.values_limits = p2.values_limits);
+ {
+ values_interval = union_float_interval p1.values_interval p2.values_interval;
+ values_limits = p1.values_limits;
+ values_grade = worst_precision_grade p1.values_grade p2.values_grade;
+ }
+
+let update_node_int_values node new_values =
+ node.node_int_values <-
+ Some (Extlib.opt_fold merge_int_values node.node_int_values new_values)
+
+let update_node_float_values node new_values =
+ node.node_float_values <-
+ Some (Extlib.opt_fold merge_float_values node.node_float_values new_values)
+
+
+let create_dependency ~allow_folding g v1 dependency_kind v2 =
+ let same_kind (_,e,_) =
+ e.dependency_kind = dependency_kind
+ in
+ let matching_edge =
+ try
+ if allow_folding then
+ Some (List.find same_kind (G.find_all_edges g v1 v2))
+ else
+ None
+ with Not_found -> None
+ in
+ match matching_edge with
+ | Some (_,e,_) ->
+ e.dependency_multiple <- true
+ | None ->
+ let e = {
+ dependency_key = !next_key;
+ dependency_kind;
+ dependency_multiple = false;
+ }
+ in
+ 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;
+ fold_vertex (fun n acc -> if Table.mem table n then acc else n :: acc) 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
+
+ let module FileTable = Datatype.String.Hashtbl in
+ let module CallstackTable = Value_types.Callstack.Hashtbl in
+ let file_table = FileTable.create 13
+ 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;
+ {
+ sg_name = "file_" ^ (string_of_int !file_counter);
+ sg_attributes = [build_label filename];
+ sg_parent = None;
+ }
+ 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_callstack_subgraph cs =
+ CallstackTable.memo callstack_table cs build_callstack_subgraph
+ in
+
+ let module Dot = Graph.Graphviz.Dot (
+ struct
+ include G
+ let graph_attributes _g = []
+ let default_vertex_attributes _g = []
+ let vertex_name v = "cp" ^ (string_of_int v.node_key)
+ let vertex_attributes v =
+ let grade = match v.node_int_values, v.node_float_values with
+ | Some v1, Some v2 ->
+ Some (worst_precision_grade v1.values_grade v2.values_grade)
+ | Some v, _ -> Some v.values_grade
+ | _, Some v -> Some v.values_grade
+ | None, None -> None
+ in
+ let l = ref [] in
+ let text = Pretty_utils.to_string Node_kind.pretty v.node_kind in
+ if text <> "" then
+ l := build_label text :: !l;
+ let kind = match v.node_kind with
+ | Scalar _ -> [`Shape `Box]
+ | Composite _ -> [ `Shape `Box3d ]
+ | Scattered _ -> [ `Shape `Parallelogram ]
+ | Alarm _ -> [ `Shape `Doubleoctagon ;
+ `Style `Bold ; `Color 0xff0000 ;
+ `Style `Filled ; `Fillcolor 0xff0000 ]
+ and values = match grade with
+ | None -> []
+ | Some Singleton ->
+ [`Color 0x88aaff ; `Style `Filled ; `Fillcolor 0xaaccff ]
+ | Some Normal ->
+ [ `Color 0x004400 ; `Style `Filled ; `Fillcolor 0xeeffee ]
+ | Some Wide ->
+ [ `Color 0xff0000 ; `Style `Filled ; `Fillcolor 0xffbbbb ]
+ in
+ l := values @ kind @ !l;
+ if not v.node_deps_computed then
+ l := [ `Style `Dotted ] @ !l;
+ !l
+ let get_subgraph v =
+ 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
+ | Callee -> [`Color 0x00ff00 ]
+ | _ -> []
+ and folding_attribute = match e.dependency_multiple with
+ | true -> [ `Style `Bold ]
+ | false -> []
+ in kind_attribute @ folding_attribute
+ end)
+ in
+ Dot.output_graph out_channel g
+
+module JsonPrinter =
+struct
+ let output_kinstr = function
+ | Cil_types.Kglobal -> `String "global"
+ | Cil_types.Kstmt stmt -> `Int stmt.Cil_types.sid
+
+ let output_callsite (kf,kinstr) =
+ `Assoc [
+ ("fun", `String (Kernel_function.get_name kf)) ;
+ ("instr", output_kinstr kinstr) ;
+ ]
+
+ let output_callstack cs =
+ `List (List.map output_callsite cs)
+
+ let output_node_kind kind =
+ let s = match kind with
+ | Scalar _ -> "scalar"
+ | Composite _ -> "composite"
+ | Scattered _ -> "scattered"
+ | Alarm _ -> "alarm"
+ in
+ `String s
+
+ let output_node_locality { loc_file ; loc_callstack } =
+ let f1 = ("file", `String loc_file) in
+ let fields = match loc_callstack with
+ | [] -> [f1]
+ | cs -> [f1 ; ("callstack", output_callstack cs)]
+ in
+ `Assoc fields
+
+ let output_node_precision_grade grade =
+ let s = match grade with
+ | Singleton -> "singleton"
+ | Normal -> "normal"
+ | Wide -> "wide"
+ in
+ `String s
+
+ let output_dep_kind kind =
+ let s = match kind with
+ | Callee -> "callee"
+ | Data -> "data"
+ | Address -> "addr"
+ | Control -> "ctrl"
+ | Composition -> "comp"
+ in
+ `String s
+
+ let output_int_interval interval =
+ (* TODO: handle overflow *)
+ `Assoc [
+ ("min", `Int (Integer.to_int interval.min)) ;
+ ("max", `Int (Integer.to_int interval.max)) ;
+ ]
+
+ let output_float_interval interval =
+ `Assoc [
+ ("min", `Float interval.min) ;
+ ("max", `Float interval.max) ;
+ ]
+
+ let output_node_int_values values =
+ `Assoc [
+ ("computed", output_int_interval values.values_interval) ;
+ ("limits", output_int_interval values.values_limits) ;
+ ("grade", output_node_precision_grade values.values_grade) ;
+ ]
+
+ let output_node_float_values values =
+ `Assoc [
+ ("computed", output_float_interval values.values_interval) ;
+ ("limits", output_float_interval values.values_limits) ;
+ ("grade", output_node_precision_grade values.values_grade) ;
+ ]
+
+ let output_node node =
+ let label = Pretty_utils.to_string Node_kind.pretty node.node_kind in
+ `Assoc ([
+ ("id", `Int node.node_key) ;
+ ("label", `String label) ;
+ ("kind", output_node_kind node.node_kind) ;
+ ("locality", output_node_locality node.node_locality) ;
+ ("explored", `Bool node.node_deps_computed) ;
+ ] @
+ begin match node.node_int_values with
+ | None -> []
+ | Some node_values ->
+ [("int_values", output_node_int_values node_values)]
+ end @
+ begin match node.node_float_values with
+ | None -> []
+ | Some node_values ->
+ [("float_values", output_node_float_values node_values)]
+ end @
+ begin match Node_kind.to_lval node.node_kind with
+ | None -> []
+ | Some lval ->
+ let typ = Cil.typeOfLval lval in
+ let str = Pretty_utils.to_string Cil_printer.pp_typ typ in
+ [("type", `String str)]
+ end)
+
+ let output_dep (n1,dep,n2) =
+ `Assoc [
+ ("id", `Int dep.dependency_key) ;
+ ("src", `Int n1.node_key) ;
+ ("dst", `Int n2.node_key) ;
+ ("kind", output_dep_kind dep.dependency_kind) ;
+ ("multiple", `Bool dep.dependency_multiple)
+ ]
+
+ let output_graph g =
+ `Assoc [
+ ("nodes", `List (List.map output_node (vertices g))) ;
+ ("deps", `List (List.map output_dep (edges g)))
+ ]
+
+ let output_diff g diff =
+ let added_nodes = List.map output_node diff.added_nodes
+ and added_deps =
+ let module Set = Set.Make (struct
+ type t = edge
+ let compare (_,d1,_) (_,d2,_) = d1.dependency_key - d2.dependency_key
+ end)
+ in
+ let collect_deps set node =
+ let set = fold_pred_e Set.add g node set in
+ let set = fold_succ_e Set.add g node set in
+ set
+ in
+ let set = List.fold_left collect_deps Set.empty diff.added_nodes in
+ List.map output_dep (Set.elements set)
+ and removed_nodes =
+ List.map (fun node -> `Int node.node_key) diff.removed_nodes
+ in
+ `Assoc [
+ ("add", `Assoc [
+ ("nodes", `List added_nodes) ;
+ ("deps", `List added_deps)
+ ]) ;
+ ("sub", `List removed_nodes)]
+end
+
+let ouptput_to_json out_channel g =
+ let json = JsonPrinter.output_graph g in
+ Yojson.Basic.to_channel out_channel json
+
+let to_json g =
+ JsonPrinter.output_graph g
+
+let diff_to_json g diff =
+ JsonPrinter.output_diff g diff
diff --git a/src/plugins/dive/imprecision_graph.mli b/src/plugins/dive/imprecision_graph.mli
new file mode 100644
index 0000000000000000000000000000000000000000..dae5176aff12bbd6e7ead1c57dfd62394775f788
--- /dev/null
+++ b/src/plugins/dive/imprecision_graph.mli
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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 Graph.Sig.G
+ with type V.t = node
+ and type E.t = node * dependency * node
+
+module Node : Graph.Sig.COMPARABLE with type t = node
+
+module Dependency : Graph.Sig.COMPARABLE with type t = dependency
+
+val create : ?size:int -> unit -> t
+
+val create_node :
+ node_kind:node_kind ->
+ node_locality:node_locality -> t -> node
+
+val remove_node : t -> node -> unit
+
+val update_node_int_values : node -> Integer.t node_values -> unit
+val update_node_float_values : node -> float 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
+
+val to_json : t -> Json.t
+val diff_to_json : t -> graph_diff -> Json.t
diff --git a/src/plugins/dive/main.ml b/src/plugins/dive/main.ml
new file mode 100644
index 0000000000000000000000000000000000000000..7638783ac208063427b5dcbdfed54ac28913dcb4
--- /dev/null
+++ b/src/plugins/dive/main.ml
@@ -0,0 +1,61 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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 format = Dot | Json
+
+let output format context basename =
+ let filename, output_function = match format with
+ | Dot -> basename ^ ".dot", Imprecision_graph.ouptput_to_dot
+ | Json -> basename ^ ".json", Imprecision_graph.ouptput_to_json
+ in
+ Self.result "output to %s" filename;
+ let out_channel = open_out filename in
+ output_function out_channel (Build.get_graph context);
+ close_out out_channel
+
+let main () =
+ if not (Self.FromBases.is_empty () &&
+ Self.FromFunctionAlarms.is_empty ()) then begin
+ (* Create the initial graph *)
+ let context = Build.create () in
+ (* Handle parameters *)
+ Self.UnfoldedBases.iter (Build.unfold_base context);
+ Self.HiddenBases.iter (Build.hide_base context);
+ let depth = Self.DepthLimit.get () in
+ (* Add targeted vars to it *)
+ Self.FromBases.iter (Build.add_var ~depth context);
+ (* Add alarms *)
+ let add_alarm _emitter kf stmt ~rank:_ alarm _code_annot =
+ if Self.FromFunctionAlarms.mem kf then
+ Build.add_alarm ~depth context stmt alarm
+ in
+ if not (Self.FromFunctionAlarms.is_empty ()) then
+ Alarms.iter add_alarm;
+ (* Output it *)
+ if Self.OutputDot.get () <> "" then
+ output Dot context (Self.OutputDot.get ());
+ if Self.OutputJson.get () <> "" then
+ output Json context (Self.OutputJson.get ());
+ end
+
+let () =
+ Db.Main.extend main
diff --git a/src/plugins/dive/node_kind.ml b/src/plugins/dive/node_kind.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5c6b5979cf3e4eba1ddb71edcf4f073fe240ea62
--- /dev/null
+++ b/src/plugins/dive/node_kind.ml
@@ -0,0 +1,100 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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
+
+module DatatypeInput =
+struct
+ include Datatype.Undefined
+
+ open Cil_datatype
+
+ type t = node_kind
+
+ let (<?>) c (cmp,x,y) =
+ if c = 0
+ then cmp x y
+ else c
+
+ let name = "Node_kind"
+
+ let reprs = [ Scalar (
+ List.hd Varinfo.reprs,
+ List.hd Typ.reprs,
+ List.hd Offset.reprs) ]
+
+ let compare k1 k2 =
+ match k1, k2 with
+ | 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,ki1), Scattered (lv2,ki2) ->
+ LvalStructEq.compare lv1 lv2 <?> (Kinstr.compare, ki1, ki2)
+ | Scattered _, _ -> 1
+ | _, Scattered _ -> -1
+ | Alarm (stmt1, alarm1), Alarm (stmt2, alarm2) ->
+ Stmt.compare stmt1 stmt2 <?> (Alarms.compare, alarm1, alarm2)
+
+ let equal k1 k2 =
+ match k1, k2 with
+ | Scalar (vi1, _, offset1), Scalar (vi2, _, offset2) ->
+ Varinfo.equal vi1 vi2 && OffsetStructEq.equal offset1 offset2
+ | Composite vi1, Composite vi2 -> Varinfo.equal vi1 vi2
+ | Scattered (lv1, ki1), Scattered (lv2, ki2) ->
+ LvalStructEq.equal lv1 lv2 && Kinstr.equal ki1 ki2
+ | Alarm (stmt1, alarm1), Alarm (stmt2, alarm2) ->
+ Stmt.equal stmt1 stmt2 && Alarms.equal alarm1 alarm2
+ | _ -> false
+
+ let hash k =
+ match k with
+ | Scalar (vi, _, offset) ->
+ Hashtbl.hash (1, Varinfo.hash vi, OffsetStructEq.hash offset)
+ | Composite vi -> Hashtbl.hash (2, Varinfo.hash vi)
+ | Scattered (lv, ki) ->
+ Hashtbl.hash (3, LvalStructEq.hash lv, Kinstr.hash ki)
+ | 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 _ -> 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 (_,_) -> 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)
diff --git a/src/plugins/dive/node_kind.mli b/src/plugins/dive/node_kind.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a65055305c6980a5f09e07fe79305cbded635561
--- /dev/null
+++ b/src/plugins/dive/node_kind.mli
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include Datatype.S with type t = Graph_types.node_kind
+
+val get_base : t -> Cil_types.varinfo option
+val to_lval : t -> Cil_types.lval option
diff --git a/src/plugins/dive/self.ml b/src/plugins/dive/self.ml
new file mode 100644
index 0000000000000000000000000000000000000000..75bc7d1cce238aad412ea6d2bb83842f8b65b297
--- /dev/null
+++ b/src/plugins/dive/self.ml
@@ -0,0 +1,132 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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 Plugin.Register
+ (struct
+ let name = "dive"
+ let shortname = "dive"
+ let help = "An interactive imprecision graph generator for Eva."
+ end)
+
+module OutputDot = Empty_string
+ (struct
+ let option_name = "-dive-output-dot"
+ let help = "Outputs the built graph into a dot file with this basename."
+ let arg_name = "basename"
+ end)
+
+module OutputJson = Empty_string
+ (struct
+ let option_name = "-dive-output-json"
+ let help = "Outputs the built graph into a json file with this basename."
+ let arg_name = "basename"
+ end)
+
+module DepthLimit = Int
+ (struct
+ let option_name = "-dive-depth-limit"
+ let help = "Build dependencies up to a depth of N."
+ let arg_name = "N"
+ let default = 2
+ end)
+
+module FromFunctionAlarms = Kernel_function_set
+ (struct
+ let option_name = "-dive-from-alarms"
+ let help = "Build the graph from the alarms emitted in the given functions."
+ let arg_name = "f1,..."
+ end)
+
+module Varinfo =
+struct
+ include Cil_datatype.Varinfo
+
+ let of_string s =
+ let regexp = Str.regexp "^\\([_a-zA-Z0-9]+\\)::\\([_a-zA-Z0-9]+\\)$" in
+ 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 ^ "'"))
+ 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 '" ^ 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 ^ "'"));
+ match Globals.Syntactic_search.find_in_scope s Cil_types.Program with
+ | Some vi -> vi
+ | None ->
+ raise (Cannot_build ("no global variable '" ^ s ^ "'"))
+
+ let to_string vi =
+ match Kernel_function.find_defining_kf vi with
+ | None -> vi.vname
+ | Some kf -> Kernel_function.get_name kf ^ "::" ^ vi.vname
+
+ let of_singleton_string = no_element_of_string
+end
+
+module type Varinfo_set = Parameter_sig.Set
+ with type elt = Cil_types.varinfo
+ and type t = Cil_datatype.Varinfo.Set.t
+
+module Varinfo_set (X: Parameter_sig.Input_with_arg) =
+ Make_set
+ (Varinfo)
+ (struct
+ include X
+ let dependencies = []
+ let default = Cil_datatype.Varinfo.Set.empty
+ end)
+
+module FromBases = Varinfo_set
+ (struct
+ let option_name = "-dive-from-variables"
+ let help = "Build the graph from these local variables."
+ let arg_name = "f::v,..."
+ end)
+
+module UnfoldedBases = Varinfo_set
+ (struct
+ let option_name = "-dive-unfold"
+ let help = "Defines the composite variables which should be \
+ unfolded into individual cells."
+ let arg_name = "f::v,..."
+ end)
+
+module HiddenBases = Varinfo_set
+ (struct
+ let option_name = "-dive-hide"
+ let help = "Defines the variables which must not be \
+ displayed in the graph. The dependencies for these bases \
+ are not computed either."
+ let arg_name = "f::v,..."
+ end)
diff --git a/src/plugins/dive/self.mli b/src/plugins/dive/self.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f15ce3c96bd820641bf5a421de36bc8181ae046a
--- /dev/null
+++ b/src/plugins/dive/self.mli
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include Plugin.S
+
+module type Varinfo_set = Parameter_sig.Set
+ with type elt = Cil_types.varinfo
+ and type t = Cil_datatype.Varinfo.Set.t
+
+module OutputDot : Parameter_sig.String
+module OutputJson : Parameter_sig.String
+module DepthLimit : Parameter_sig.Int
+module FromFunctionAlarms : Parameter_sig.Kernel_function_set
+module FromBases : Varinfo_set
+module UnfoldedBases : Varinfo_set
+module HiddenBases : Varinfo_set
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c80a64405a8e1a0ef15b57487b4429728382618f
--- /dev/null
+++ b/src/plugins/dive/server_interface.ml
@@ -0,0 +1,219 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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 Server
+
+(* TODO: state *)
+let get_graph =
+ let graph = ref None in
+ fun () ->
+ match !graph with
+ | Some g -> g
+ | None ->
+ let g = Build.create () in
+ graph := Some g;
+ g
+
+
+let page = Doc.page (`Plugin "dive")
+ ~title:"Dive Services"
+ ~filename:"dive.md"
+
+module Graph =
+struct
+ type t = Imprecision_graph.t
+ let syntax = Syntax.any
+ let to_json = Imprecision_graph.to_json
+end
+
+module GraphDiff =
+struct
+ type t = Imprecision_graph.t * Graph_types.graph_diff
+ let syntax = Syntax.any
+ let to_json = fun (g,d) -> Imprecision_graph.diff_to_json g d
+end
+
+module Variable = Data.Collection (struct
+ let name = "dive-variable-name"
+ let descr = Markdown.plain "The name of variable of the program"
+
+ let signature = Data.Record.signature ~page ~name ~descr ()
+
+ let _fun_field = Data.Record.option signature
+ ~descr:(Markdown.plain "owner function for a local variable")
+ (module Data.Jstring)
+
+ let _var_field = Data.Record.field signature
+ ~descr:(Markdown.plain "variable name")
+ (module Data.Jstring)
+
+ type t = Cil_types.varinfo
+ module R =
+ (val (Data.Record.publish signature): Data.Record.S with type r = t)
+
+ let syntax = R.syntax
+
+ let to_json v =
+ let varname = v.Cil_types.vname in
+ let fields = [ "var", `String varname ] in
+ let fields = match Kernel_function.find_defining_kf v with
+ | Some kf -> ("fun", `String (Kernel_function.get_name kf)) :: fields
+ | None -> fields
+ in
+ `Assoc fields
+
+ let of_json json =
+ let open Yojson.Basic.Util in
+ let funname =
+ try Some (json |> member "fun" |> to_string)
+ with Not_found -> None
+ and varname = json |> member "var" |> to_string in
+ match funname with
+ | Some name ->
+ let kf =
+ try
+ Globals.Functions.find_by_name name
+ with Not_found ->
+ Data.failure "no function '%s'" name
+ in
+ let vi =
+ try Globals.Vars.find_from_astinfo varname (Cil_types.VLocal kf)
+ with Not_found ->
+ try Globals.Vars.find_from_astinfo varname (Cil_types.VFormal kf)
+ with Not_found ->
+ Data.failure "no variable '%s' in function '%s'"
+ varname name
+ in
+ vi
+ | None ->
+ match
+ Globals.Syntactic_search.find_in_scope varname Cil_types.Program
+ with
+ | Some vi -> vi
+ | None ->
+ Data.failure "no global variable '%s'" varname
+ end)
+
+module Function = Data.Collection (struct
+ type t = Cil_types.kernel_function
+
+ let syntax = Syntax.publish ~page ~name:"dive-function-name"
+ ~synopsis:Syntax.string
+ ~descr:(Markdown.plain "The name of a function of the program") ()
+
+ let to_json kf =
+ `String (Kernel_function.get_name kf)
+
+ let of_json json =
+ let open Yojson.Basic.Util in
+ let name = to_string json in
+ try
+ Globals.Functions.find_by_name name
+ with Not_found ->
+ Data.failure "no function '%s'" name
+ end)
+
+module Node = Data.Collection (struct
+ type t = Graph_types.node
+
+ let syntax = Syntax.publish ~page ~name:"dive-node"
+ ~synopsis:Syntax.int
+ ~descr:(Markdown.plain "A node identifier in the graph") ()
+
+ let to_json node =
+ `Int node.Graph_types.node_key
+
+ let of_json json =
+ let open Yojson.Basic.Util in
+ let node_key = to_int json in
+ try
+ Build.find_node (get_graph ()) node_key
+ with Not_found ->
+ Data.failure "no node '%d' in the current graph" node_key
+ end)
+
+
+let () = Request.register ~page
+ ~kind:`GET ~name:"dive.graph"
+ ~descr:(Markdown.plain "Retrieve the whole graph")
+ ~input:(module Data.Junit) ~output:(module Graph)
+ (fun () -> Build.get_graph (get_graph ()))
+
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"dive.clear"
+ ~descr:(Markdown.plain "Erase the graph and start over with an empty one")
+ ~input:(module Data.Junit) ~output:(module Data.Junit)
+ (fun () -> Build.clear (get_graph ()))
+
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"dive.add_var"
+ ~descr:(Markdown.plain "Add a variable to the graph")
+ ~input:(module Variable) ~output:(module GraphDiff)
+ begin fun var ->
+ let depth = Self.DepthLimit.get () in
+ let g = get_graph () in
+ Build.add_var ~depth g var;
+ Build.get_graph g, Build.take_last_differences g
+ end
+
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"dive.add_function_alarms"
+ ~descr:(Markdown.plain "Add all alarms of the given function")
+ ~input:(module Function) ~output:(module GraphDiff)
+ begin fun kf ->
+ let depth = Self.DepthLimit.get () in
+ let g = get_graph () in
+ Build.add_function_alarms ~depth g kf;
+ Build.get_graph g, Build.take_last_differences g
+ end
+
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"dive.explore"
+ ~descr:(Markdown.plain "Explore the graph starting from an existing vertex")
+ ~input:(module Node) ~output:(module GraphDiff)
+ begin fun node ->
+ let depth = Self.DepthLimit.get () in
+ let g = get_graph () in
+ Build.explore_from_node ~depth g node;
+ Build.get_graph g, Build.take_last_differences g
+ end
+
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"dive.show"
+ ~descr:(Markdown.plain "Show the dependencies of an existing vertex")
+ ~input:(module Node) ~output:(module GraphDiff)
+ begin fun node ->
+ let depth = Self.DepthLimit.get () in
+ let g = get_graph () in
+ Build.show ~depth g node;
+ Build.get_graph g, Build.take_last_differences g
+ end
+
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"dive.hide"
+ ~descr:(Markdown.plain "Hide the dependencies of an existing vertex")
+ ~input:(module Node) ~output:(module GraphDiff)
+ begin fun node ->
+ let g = get_graph () in
+ Build.hide g node;
+ Build.get_graph g, Build.take_last_differences g
+ end
diff --git a/src/plugins/dive/server_interface.mli b/src/plugins/dive/server_interface.mli
new file mode 100644
index 0000000000000000000000000000000000000000..6b8cd770d93ac0573027b76620aa88ab4cf0316b
--- /dev/null
+++ b/src/plugins/dive/server_interface.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module Variable : Server.Data.S_collection with type t = Cil_types.varinfo
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..fb2876d7010ba35b4a66b5c510f4c5b70cf9143f
--- /dev/null
+++ b/src/plugins/dive/tests/dive/assigned_param.i
@@ -0,0 +1,18 @@
+/* run.config
+STDOPT: +"-dive-from-variables main::w -dive-depth-limit 5"
+*/
+
+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/callstack_strategy.i b/src/plugins/dive/tests/dive/callstack_strategy.i
new file mode 100644
index 0000000000000000000000000000000000000000..b309e51cfc28261a73aedd2f06e2bf8c06668486
--- /dev/null
+++ b/src/plugins/dive/tests/dive/callstack_strategy.i
@@ -0,0 +1,31 @@
+/* run.config
+STDOPT: +"-dive-from-variables g::r -dive-depth-limit 20"
+*/
+
+float f(float z) {
+ return z;
+}
+
+float g(float y) {
+ float z = f(y);
+ float r = y + z;
+ return r;
+}
+
+float h(float x) {
+ float y = f(x);
+ float r = g(y);
+ return r;
+}
+
+float i(float x) {
+ return g(x);
+}
+
+
+void main(float a)
+{
+ h(a);
+ i(a);
+}
+
diff --git a/src/plugins/dive/tests/dive/const.i b/src/plugins/dive/tests/dive/const.i
new file mode 100644
index 0000000000000000000000000000000000000000..7001746bea33cc57f5d2f0d0a678118be3606e08
--- /dev/null
+++ b/src/plugins/dive/tests/dive/const.i
@@ -0,0 +1,16 @@
+/* run.config
+STDOPT: +"-dive-from-variables main::res -dive-depth-limit 4"
+*/
+
+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;
+}
diff --git a/src/plugins/dive/tests/dive/global.i b/src/plugins/dive/tests/dive/global.i
new file mode 100644
index 0000000000000000000000000000000000000000..ca08f89790d56aef256c8a8d67fe553d065bbb5d
--- /dev/null
+++ b/src/plugins/dive/tests/dive/global.i
@@ -0,0 +1,14 @@
+/* run.config
+STDOPT: +"-dive-from-variables main::z"
+*/
+
+float g;
+
+float main(float x)
+{
+ float y = x + 1;
+ g = y;
+ float z = g + x;
+ return z;
+}
+
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..ad2fec86899271793323922c055d7bda9074c910
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/assigned_param.dot
@@ -0,0 +1,22 @@
+digraph G {
+ cp0 [label=<w>, shape=box, ];
+ cp1 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp3 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp7 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+
+ subgraph cluster_cs_1 { label=<main>; cp7;cp5;cp0;
+ subgraph cluster_cs_2 { label=<f>; cp3;cp1;
+ };
+ };
+
+ cp1 -> cp0;
+ cp3 -> cp1;
+ cp5 -> cp1;
+ cp7 -> 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..af19ea9f6ba5fe5cb6d0774249bbb2d09eaf2b97
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/assigned_param.res.oracle
@@ -0,0 +1,20 @@
+[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:17: Warning:
+ signed overflow. assert w + 1 ≤ 2147483647;
+[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 6 statements reached (out of 6): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 integer overflow
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[dive] output to tests/dive/result/assigned_param.dot
diff --git a/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot b/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot
new file mode 100644
index 0000000000000000000000000000000000000000..2df030b641903b7f93211d1f082a334ffa6e3182
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/callstack_strategy.dot
@@ -0,0 +1,44 @@
+digraph G {
+ cp0 [label=<r>, shape=box, ];
+ cp1 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp3 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp7 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp9 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp11 [label=<a>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp13 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp16 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+
+ subgraph cluster_cs_1 { label=<g>; cp3;cp1;cp0;
+ subgraph cluster_cs_4 { label=<f>; cp9;
+ };
+ };
+ subgraph cluster_cs_2 { label=<i>; cp5;
+ };
+ subgraph cluster_cs_3 { label=<h>; cp16;cp7;
+ subgraph cluster_cs_6 { label=<f>; cp13;
+ };
+ };
+ subgraph cluster_cs_5 { label=<main>; cp11;
+ };
+
+ cp1 -> cp0;
+ cp1 -> cp9;
+ cp3 -> cp0;
+ cp5 -> cp1;
+ cp7 -> cp1;
+ cp9 -> cp3;
+ cp11 -> cp5;
+ cp11 -> cp16;
+ cp13 -> cp7;
+ cp16 -> cp13;
+
+ }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/callstack_strategy.res.oracle b/src/plugins/dive/tests/dive/oracle/callstack_strategy.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..de74d0e71cbc624ac141f2ac234818c9303e05be
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/callstack_strategy.res.oracle
@@ -0,0 +1,20 @@
+[kernel] Parsing tests/dive/callstack_strategy.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:alarm] tests/dive/callstack_strategy.i:11: Warning:
+ non-finite float value. assert \is_finite(\add_float(y, z));
+[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 5 functions analyzed (out of 5): 100% coverage.
+ In these functions, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 nan or infinite floating-point value
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[dive] output to tests/dive/result/callstack_strategy.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..db4416d80c8653914d98d9052e3e73972659c567
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/const.dot
@@ -0,0 +1,29 @@
+digraph G {
+ cp0 [label=<res>, shape=box, ];
+ cp1 [label=<__retres>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp3 [label=<c>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp5 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp7 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp9 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp11 [label=<i>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,dotted", ];
+
+ subgraph cluster_cs_1 { label=<main>; cp11;cp0;
+ subgraph cluster_cs_2 { label=<f>; cp9;cp7;cp5;cp3;cp1;
+ };
+ };
+
+ cp1 -> cp0;
+ cp3 -> cp1;
+ cp5 -> cp1;
+ cp7 -> cp3;
+ cp9 -> cp5;
+ cp11 -> cp7;
+ cp11 -> cp9;
+
+ }
\ 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..d4e8c9e857c1d7380cf4ae5576b221fb12349996
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/const.res.oracle
@@ -0,0 +1,28 @@
+[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
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 6 statements reached (out of 6): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 5 alarms generated by the analysis:
+ 5 integer overflows
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[dive] output to tests/dive/result/const.dot
diff --git a/src/plugins/dive/tests/dive/oracle/global.dot b/src/plugins/dive/tests/dive/oracle/global.dot
new file mode 100644
index 0000000000000000000000000000000000000000..b64b502f0e52418d362f35612dfdadb6b03786fe
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/global.dot
@@ -0,0 +1,19 @@
+digraph G {
+ cp0 [label=<z>, shape=box, ];
+ cp1 [label=<g>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp3 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp5 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,dotted", ];
+
+ subgraph cluster_cs_1 { label=<main>; cp5;cp3;cp0;
+ };
+ subgraph cluster_file_1 { label=<tests/dive/global.i>; cp1;
+ };
+
+ cp1 -> cp0;
+ cp3 -> cp0;
+ cp5 -> cp1;
+
+ }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/global.res.oracle b/src/plugins/dive/tests/dive/oracle/global.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d46beb72b6935e11987bfde52dfdcb6906017be3
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/global.res.oracle
@@ -0,0 +1,20 @@
+[kernel] Parsing tests/dive/global.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:alarm] tests/dive/global.i:11: Warning:
+ non-finite float value. assert \is_finite(\add_float(g, x));
+[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 1 function analyzed (out of 1): 100% coverage.
+ In this function, 4 statements reached (out of 4): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 nan or infinite floating-point value
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[dive] output to tests/dive/result/global.dot
diff --git a/src/plugins/dive/tests/dive/oracle/per_callstack.dot b/src/plugins/dive/tests/dive/oracle/per_callstack.dot
new file mode 100644
index 0000000000000000000000000000000000000000..f2c61f4f447e4496dd5764f14775ac53956e6af3
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/per_callstack.dot
@@ -0,0 +1,50 @@
+digraph G {
+ cp0 [label=<w>, shape=box, ];
+ cp1 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp3 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp5 [label=<z>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp7 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp9 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp11 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp13 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp15 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp17 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp19 [label=<a>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp21 [label=<b>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp23 [label=<c>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+
+ subgraph cluster_cs_1 { label=<main>; cp23;cp21;cp19;cp5;cp3;cp1;cp0;
+ subgraph cluster_cs_2 { label=<f>; cp13;cp7;
+ };
+ subgraph cluster_cs_3 { label=<f>; cp15;cp9;
+ };
+ subgraph cluster_cs_4 { label=<f>; cp17;cp11;
+ };
+ };
+
+ cp1 -> cp0;
+ cp3 -> cp0;
+ cp5 -> cp0;
+ cp7 -> cp1;
+ cp9 -> cp3;
+ cp11 -> cp5;
+ cp13 -> cp7;
+ cp15 -> cp9;
+ cp17 -> cp11;
+ cp19 -> cp13;
+ cp21 -> cp15;
+ cp23 -> cp17;
+
+ }
\ No newline at end of file
diff --git a/src/plugins/dive/tests/dive/oracle/per_callstack.res.oracle b/src/plugins/dive/tests/dive/oracle/per_callstack.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bd8ebb87aa38c0d1b4a7b7eef17528671dad13af
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/per_callstack.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing tests/dive/per_callstack.i (no preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:alarm] tests/dive/per_callstack.i:15: Warning:
+ non-finite float value. assert \is_finite(\add_float(x, y));
+[eva:alarm] tests/dive/per_callstack.i:15: Warning:
+ non-finite float value. assert \is_finite(\add_float(\add_float(x, y), z));
+[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 7 statements reached (out of 7): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 2 alarms generated by the analysis:
+ 2 nan or infinite floating-point values
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[dive] output to tests/dive/result/per_callstack.dot
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 0000000000000000000000000000000000000000..29d345ca69b9a03cab6c7453244add21d00feec4
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/pointed_param.dot
@@ -0,0 +1,29 @@
+digraph G {
+ cp0 [label=<y>, shape=box, ];
+ cp1 [label=<tmp>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp3 [label=<tmp>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp5 [label=<tmp>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp7 [label=<__retres>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp9 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled,dotted", ];
+
+ subgraph cluster_cs_1 { label=<main>; cp1;cp0;
+ subgraph cluster_cs_2 { label=<f>; cp9;cp3;
+ subgraph cluster_cs_3 { label=<g>; cp5;
+ subgraph cluster_cs_4 { label=<h>; cp7;
+ };
+ };
+ };
+ };
+
+ cp1 -> cp0;
+ cp3 -> cp1;
+ cp5 -> cp3;
+ cp7 -> cp5;
+ cp9 -> cp7;
+
+ }
\ 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 0000000000000000000000000000000000000000..986e0eb6f92e87e39f33cc18422b9704f7bf666f
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/pointed_param.res.oracle
@@ -0,0 +1,17 @@
+[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
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 4 functions analyzed (out of 4): 100% coverage.
+ In these functions, 9 statements reached (out of 9): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[dive] output to tests/dive/result/pointed_param.dot
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 0000000000000000000000000000000000000000..714f41eccb2a776fad23082a7d007832a0700647
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/pointers_to_local.dot
@@ -0,0 +1,20 @@
+digraph G {
+ cp0 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp1 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp4 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+
+ subgraph cluster_cs_1 { label=<main>; cp0;
+ subgraph cluster_cs_4 { label=<f2>; cp4;
+ };
+ };
+
+ cp0 -> cp0;
+ cp0 -> cp1;
+ cp0 -> cp4;
+ cp1 -> cp0;
+ cp4 -> cp0;
+
+ }
\ 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 0000000000000000000000000000000000000000..9e4f75453d868643fa70c8371194aec69ca4f72b
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/pointers_to_local.res.oracle
@@ -0,0 +1,17 @@
+[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
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 4 functions analyzed (out of 4): 100% coverage.
+ In these functions, 12 statements reached (out of 12): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 0 alarms generated by the analysis.
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[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
new file mode 100644
index 0000000000000000000000000000000000000000..1009dfdd36fcdc4c5b0c148f4f40caca4cfde142
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/unfocused_callers.dot
@@ -0,0 +1,30 @@
+digraph G {
+ cp0 [label=<x>, shape=box, ];
+ cp1 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp3 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp5 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp7 [label=<x>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+
+ subgraph cluster_cs_1 { label=<g>; cp0;
+ };
+ subgraph cluster_cs_2 { label=<f3>; cp1;
+ };
+ subgraph cluster_cs_3 { label=<f2>; cp3;
+ };
+ subgraph cluster_cs_4 { label=<f1>; cp5;
+ };
+ subgraph cluster_cs_5 { label=<main>; cp7;
+ };
+
+ cp1 -> cp0;
+ cp3 -> cp0;
+ cp5 -> cp0;
+ cp7 -> cp1;
+ cp7 -> cp3;
+ cp7 -> cp5;
+
+ }
\ 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 0000000000000000000000000000000000000000..8e9668ded4a93d97d4cd4671892ea6ad8dd14280
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/unfocused_callers.res.oracle
@@ -0,0 +1,26 @@
+[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(\add_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(\add_float(\add_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
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 5 functions analyzed (out of 5): 100% coverage.
+ In these functions, 14 statements reached (out of 14): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 2 alarms generated by the analysis:
+ 2 nan or infinite floating-point values
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[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
new file mode 100644
index 0000000000000000000000000000000000000000..14afa37a197041f2c10b38f50cf371264a6fbdd0
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/various.dot
@@ -0,0 +1,65 @@
+digraph G {
+ cp0 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp1 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp3 [label=<x>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp7 [label=<g>, shape=box, fillcolor="#AACCFF", color="#88AAFF",
+ style="filled", ];
+ cp9 [label=<z>, shape=box, ];
+ cp10 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp12 [label=<w>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp14 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp16 [label=<tmp_0>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp18 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp21 [label=<pf>, shape=box, ];
+ cp23 [label=<x2>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp26 [label=<y>, shape=box, fillcolor="#FFBBBB", color="#FF0000",
+ style="filled", ];
+ cp30 [label=<is_nan_or_infinite: \is_finite((float)\mul_double((double)y, (double)2.0))>,
+ fillcolor="#FF0000", color="#FF0000", shape=doubleoctagon,
+ style="filled,bold", ];
+ cp32 [label=<is_nan_or_infinite: \is_finite(\add_float(y, w))>,
+ fillcolor="#FF0000", color="#FF0000", shape=doubleoctagon,
+ style="filled,bold", ];
+
+ subgraph cluster_cs_1 { label=<f>; cp30;cp1;cp0;
+ };
+ subgraph cluster_cs_2 { label=<main>; cp32;cp21;cp16;cp12;cp10;cp9;cp3;
+ subgraph cluster_cs_3 { label=<f>; cp18;cp14;
+ };
+ subgraph cluster_cs_4 { label=<f>; cp26;cp23;
+ };
+ };
+ subgraph cluster_file_1 { label=<tests/dive/various.i>; cp7;
+ };
+
+ cp0 -> cp1;
+ cp1 -> cp0;
+ cp1 -> cp30;
+ cp3 -> cp0;
+ cp3 -> cp3;
+ cp3 -> cp14;
+ cp3 -> cp23;
+ cp7 -> cp3;
+ cp10 -> cp9;
+ cp10 -> cp32;
+ cp12 -> cp9;
+ cp12 -> cp32;
+ cp14 -> cp10;
+ cp14 -> cp18;
+ cp16 -> cp12;
+ cp18 -> cp14;
+ cp21 -> cp16 [color="#00FF00", ];
+ cp23 -> cp16;
+ cp23 -> cp26;
+ cp26 -> cp23;
+
+ }
\ 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..f85c474b7ad82da6ab2816618e7c8d41a65ff3e2
--- /dev/null
+++ b/src/plugins/dive/tests/dive/oracle/various.res.oracle
@@ -0,0 +1,24 @@
+[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)\mul_double((double)y, (double)2.0));
+[eva:alarm] tests/dive/various.i:27: Warning:
+ non-finite float value. assert \is_finite(\add_float(y, w));
+[eva] done for function main
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 2 functions analyzed (out of 2): 100% coverage.
+ In these functions, 18 statements reached (out of 18): 100% coverage.
+ ----------------------------------------------------------------------------
+ No errors or warnings raised during the analysis.
+ ----------------------------------------------------------------------------
+ 2 alarms generated by the analysis:
+ 2 nan or infinite floating-point values
+ ----------------------------------------------------------------------------
+ No logical properties have been reached by the analysis.
+ ----------------------------------------------------------------------------
+[dive] output to tests/dive/result/various.dot
diff --git a/src/plugins/dive/tests/dive/per_callstack.i b/src/plugins/dive/tests/dive/per_callstack.i
new file mode 100644
index 0000000000000000000000000000000000000000..5a5d81b22cc9469962a5696f6816f540a7ece1b6
--- /dev/null
+++ b/src/plugins/dive/tests/dive/per_callstack.i
@@ -0,0 +1,18 @@
+/* run.config
+STDOPT: +"-dive-from-variables main::w -dive-depth-limit 20"
+*/
+
+float f(float x) {
+ float y = x + 1;
+ return y;
+}
+
+float main(float a, float b, float c)
+{
+ float x = f(a);
+ float y = f(b);
+ float z = f(c);
+ float w = x + y + z;
+ return w;
+}
+
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 0000000000000000000000000000000000000000..e6bd4f47db024a2e99baa09be7a14905108f0fe2
--- /dev/null
+++ b/src/plugins/dive/tests/dive/pointed_param.i
@@ -0,0 +1,25 @@
+/* run.config
+STDOPT: +"-dive-from-variables 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/pointers_to_local.i b/src/plugins/dive/tests/dive/pointers_to_local.i
new file mode 100644
index 0000000000000000000000000000000000000000..a1f5c7af079921b0e106469c4d1cf09a4c4d0725
--- /dev/null
+++ b/src/plugins/dive/tests/dive/pointers_to_local.i
@@ -0,0 +1,25 @@
+/* run.config
+STDOPT: +"-dive-from-variables 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/unfocused_callers.i b/src/plugins/dive/tests/dive/unfocused_callers.i
new file mode 100644
index 0000000000000000000000000000000000000000..44723b2c92f6c930b240cf92c2e8c9e7225c7c75
--- /dev/null
+++ b/src/plugins/dive/tests/dive/unfocused_callers.i
@@ -0,0 +1,19 @@
+/* run.config
+STDOPT: +"-dive-from-variables 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/dive/various.i b/src/plugins/dive/tests/dive/various.i
new file mode 100644
index 0000000000000000000000000000000000000000..62468d375e7ffa0f73f17935d09e60d152884a81
--- /dev/null
+++ b/src/plugins/dive/tests/dive/various.i
@@ -0,0 +1,29 @@
+/* run.config
+STDOPT: +"-dive-from-variables main::z,f::x2 -dive-from-alarms f,main -dive-depth-limit 5"
+*/
+
+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);
+ x = x + 0.5f;
+ 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..9ff9387337545ed97c88920ed5c79a722351eaa8
--- /dev/null
+++ b/src/plugins/dive/tests/test_config
@@ -0,0 +1,3 @@
+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-dot @PTEST_RESULT@/@PTEST_NAME@
+FILTER: perl -0777 -pe 's/\[server[^[]*//g'