[Pdg_types] new plug-in

src/plugins/impact/compute_impact.ml

@@ -22,7 +22,10 @@
 
 open Cil_types
 open Cil_datatype
+
+open Pdg_types
 open PdgIndex
+
 open Reason_graph
 
 (** Computation of the PDG nodes that are impacted by the "execution"

src/plugins/impact/compute_impact.mli

@@ -22,6 +22,8 @@
 
 open Cil_types
 
+open Pdg_types
+
 type nodes = Pdg_aux.NS.t
 type result = nodes Kernel_function.Map.t
 

src/plugins/impact/gui/register_gui.ml

@@ -23,6 +23,7 @@
 open Pretty_source
 open Gtk_helper
 open Cil_types
+open Pdg_types
 
 module SelectedStmt = struct
   include State_builder.Option_ref

src/plugins/impact/pdg_aux.ml

@@ -20,12 +20,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Pdg_types
 open PdgIndex
 open Locations
 
 type node = PdgTypes.Node.t * Zone.t
 
-
 module NS = struct
   include Hptmap.Make
       (PdgTypes.Node)

src/plugins/impact/pdg_aux.mli

@@ -23,6 +23,8 @@
 open Cil_types
 open Locations
 
+open Pdg_types
+
 (** Useful functions that are not directly accessible through the other
     Pdg modules. *)
 

src/plugins/impact/reason_graph.ml

@@ -20,6 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Pdg_types
+
 module NodeSet = PdgTypes.NodeSet
 
 

src/plugins/impact/reason_graph.mli

@@ -20,6 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Pdg_types
+
 (** Why is a node impacted. The reasons will be given as [n is impacted
     by the effect of [n'], and the impact is of type reason]. *)
 type reason_type =

src/plugins/impact/register.ml

@@ -23,6 +23,8 @@
 open Cil_types
 open Cil_datatype
 
+open Pdg_types
+
 let rec pp_stmt fmt s = match s.skind with
   | Instr _ | Return _ | Goto _ | Break _ | Continue _ | TryFinally _
   | TryExcept _ | Throw _ | TryCatch _ ->

src/plugins/impact/register.mli

@@ -22,6 +22,8 @@
 
 open Cil_types
 
+open Pdg_types
+
 val compute_pragmas: (unit -> stmt list)
 (** Compute the impact analysis from the impact pragma in the program.
     Print and slice the results according to the parameters -impact-print

src/plugins/pdg/annot.ml

@@ -22,6 +22,8 @@
 
 open Cil_types
 open Cil_datatype
+
+open Pdg_types
 open PdgIndex
 
 type data_info = ((PdgTypes.Node.t * Locations.Zone.t option) list

src/plugins/pdg/annot.mli

@@ -24,6 +24,8 @@
     @raise Kernel_function.No_Definition on annotations for function declarations.
 *)
 
+open Pdg_types
+
 (** [data_info] is composed of [(node,z_part) list, undef_loc)]
  *             and correspond to data dependencies nodes.
  *             Can be None if we don't know how to compute them.

src/plugins/pdg/api.ml

@@ -22,6 +22,8 @@
 
 [@@@ warning "-32" ]
 
+open Pdg_types
+
 type t = PdgTypes.Pdg.t
 
 type t_nodes_and_undef =

src/plugins/pdg/api.mli

@@ -20,6 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Pdg_types
+
 type t = PdgTypes.Pdg.t
 (** Program Dependence Graph type *)
 

src/plugins/pdg/build.ml

@@ -31,6 +31,8 @@
     {!module: Build.Computer} below).
 *)
 
+open Pdg_types
+
 let dkey = Pdg_parameters.register_category "build"
 let debug fmt = Pdg_parameters.debug ~dkey fmt
 let debug2 fmt = Pdg_parameters.debug ~dkey fmt ~level:2

src/plugins/pdg/build.mli

@@ -20,6 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Pdg_types
+
 val compute_pdg : Cil_types.kernel_function -> PdgTypes.Pdg.t
 
 (*

src/plugins/pdg/dune

@@ -25,6 +25,7 @@
  (deps (universe))
  (action (progn
           (echo "PDG:" %{lib-available:frama-c-pdg.core} "\n")
+          (echo "  - Pdg-Types:" %{lib-available:frama-c-pdg-types.core} "\n")
           (echo "  - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
           (echo "  - Eva:" %{lib-available:frama-c-eva.core} "\n")
           (echo "  - From:" %{lib-available:frama-c-from.core} "\n")
@@ -37,7 +38,7 @@
   (optional)
   (public_name frama-c-pdg.core)
   (flags -open Frama_c_kernel :standard -w -9)
-  (libraries frama-c.kernel frama-c-callgraph.core frama-c-from.core frama-c-eva.core)
+  (libraries frama-c.kernel frama-c-pdg-types.core frama-c-callgraph.core frama-c-from.core frama-c-eva.core)
 )
 
 (plugin (optional) (name pdg) (libraries frama-c-pdg.core) (site (frama-c plugins)))

src/plugins/pdg/marks.ml

@@ -20,9 +20,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open PdgIndex
 open Cil_datatype
 
+open Pdg_types
+open PdgIndex
+
 (** compute the marks to propagate in the caller nodes from the marks of
  * a function inputs [in_marks].
 *)

src/plugins/pdg/marks.mli

@@ -20,6 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Pdg_types
+
 open PdgMarks
 
 (** [in_marks_to_caller] translate the input information part returned by

src/plugins/pdg/pdg_state.ml

@@ -29,6 +29,8 @@
 let dkey = Pdg_parameters.register_category "state"
 
 module P = Pdg_parameters
+
+open Pdg_types
 open PdgTypes
 
 exception Cannot_fold

src/plugins/pdg/pdg_state.mli

@@ -22,6 +22,8 @@
 
 exception Cannot_fold
 
+open Pdg_types
+
 open PdgTypes
 (** Types data_state and Node.t come froms this module *)