diff --git a/src/plugins/impact/compute_impact.ml b/src/plugins/impact/compute_impact.ml
index f8d9abc1c11a5502f22f06b904f88fe12eaa379e..9f1379f3ec9104f0e9c23927c726ed55e9f30ce6 100644
--- a/src/plugins/impact/compute_impact.ml
+++ b/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"
diff --git a/src/plugins/impact/compute_impact.mli b/src/plugins/impact/compute_impact.mli
index 64307dc66281a1879dd0e7332ef9748ce058813c..74831f03df77459e0b84f0b5a17f7c2154dd3c43 100644
--- a/src/plugins/impact/compute_impact.mli
+++ b/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
diff --git a/src/plugins/impact/gui/register_gui.ml b/src/plugins/impact/gui/register_gui.ml
index bdbc771e13ca78bfd779db56b46da62b269020fc..1bd988cb199607a31a287fa4df715fb8916fa52b 100644
--- a/src/plugins/impact/gui/register_gui.ml
+++ b/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
diff --git a/src/plugins/impact/pdg_aux.ml b/src/plugins/impact/pdg_aux.ml
index c36b4d651b91759a2732f62205ffa81913788098..0a3b4acb21ed47d3e6ab5e15869955fd91164b06 100644
--- a/src/plugins/impact/pdg_aux.ml
+++ b/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)
diff --git a/src/plugins/impact/pdg_aux.mli b/src/plugins/impact/pdg_aux.mli
index fa3bcde2b5f1e1b01438823d6eeb1a3ca77a071e..f07aca633a1ca26345642e911cf4567fa5d6a3fb 100644
--- a/src/plugins/impact/pdg_aux.mli
+++ b/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. *)
diff --git a/src/plugins/impact/reason_graph.ml b/src/plugins/impact/reason_graph.ml
index f3242116b751d76bd5cd4ca7f760a35434ff2623..eb8452ccdd367b01b77d582fb0b6571ea7bbb209 100644
--- a/src/plugins/impact/reason_graph.ml
+++ b/src/plugins/impact/reason_graph.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
module NodeSet = PdgTypes.NodeSet
diff --git a/src/plugins/impact/reason_graph.mli b/src/plugins/impact/reason_graph.mli
index d0f03c55694e1a5d10439b237934cd69bce29d10..ccdbd733b2207e905a3d7054b204fcea8a674433 100644
--- a/src/plugins/impact/reason_graph.mli
+++ b/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 =
diff --git a/src/plugins/impact/register.ml b/src/plugins/impact/register.ml
index 6dfc46429bd86b280c90ba5418fb0e552a2314bb..e9b09ca1784c2b9f1d8e547f27209b48f3284003 100644
--- a/src/plugins/impact/register.ml
+++ b/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 _ ->
diff --git a/src/plugins/impact/register.mli b/src/plugins/impact/register.mli
index a426a0bb2b23bc8422b0ec2a2b818d0834729721..7cdc3c047533c1b1c7e33408488ce820ba5bff83 100644
--- a/src/plugins/impact/register.mli
+++ b/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
diff --git a/src/plugins/pdg/annot.ml b/src/plugins/pdg/annot.ml
index 00b327ff190ddb2971fcb76be628f2195a400a3c..09c37fa94373490d0eb7133f4c09be10d36bccec 100644
--- a/src/plugins/pdg/annot.ml
+++ b/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
diff --git a/src/plugins/pdg/annot.mli b/src/plugins/pdg/annot.mli
index 8aa296375843ddb909c61cba30f6b76014ea6c3e..c46dd70667d8e4df934d0843732858f3694fa267 100644
--- a/src/plugins/pdg/annot.mli
+++ b/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.
diff --git a/src/plugins/pdg/api.ml b/src/plugins/pdg/api.ml
index 6f6df8d3b0a4987dd8b32a4feb3d7cd3ca020564..0024018d796890a4136e964dcbc48c9d1ee97ec7 100644
--- a/src/plugins/pdg/api.ml
+++ b/src/plugins/pdg/api.ml
@@ -22,6 +22,8 @@
[@@@ warning "-32" ]
+open Pdg_types
+
type t = PdgTypes.Pdg.t
type t_nodes_and_undef =
diff --git a/src/plugins/pdg/api.mli b/src/plugins/pdg/api.mli
index 89b6912d3f1bfa8bc154de77f8ccc33ceb35bfcf..6094779cec4e5920a5575b27b90613eae0deaf66 100644
--- a/src/plugins/pdg/api.mli
+++ b/src/plugins/pdg/api.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
type t = PdgTypes.Pdg.t
(** Program Dependence Graph type *)
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 256f3d9f9980db347853fa0fcef8ed3ab51deb27..34dfb781a9acc918cf7bbffb2cd0f28718053bbd 100644
--- a/src/plugins/pdg/build.ml
+++ b/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
diff --git a/src/plugins/pdg/build.mli b/src/plugins/pdg/build.mli
index 583fdbc47301200ea659df06ad1ba628c46044f9..6e134517409b423d3a2dab2e50cfa49f4f2a20a1 100644
--- a/src/plugins/pdg/build.mli
+++ b/src/plugins/pdg/build.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
val compute_pdg : Cil_types.kernel_function -> PdgTypes.Pdg.t
(*
diff --git a/src/plugins/pdg/dune b/src/plugins/pdg/dune
index 09b16b196070e41eb98cc7c8d813def69334e81c..1465f8006ad853303f300d99eb456d30638e8444 100644
--- a/src/plugins/pdg/dune
+++ b/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)))
diff --git a/src/plugins/pdg/marks.ml b/src/plugins/pdg/marks.ml
index 520249051f0bf6efef0a4621202bae1f901877dd..6330ce5fb40bb8dfbe87e315f1ed4c2639b905d1 100644
--- a/src/plugins/pdg/marks.ml
+++ b/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].
*)
diff --git a/src/plugins/pdg/marks.mli b/src/plugins/pdg/marks.mli
index 55a303293f931a46d482ff89bc32e84d1ad9666d..846aeae6adace9a638d1fbda719eff249dec6731 100644
--- a/src/plugins/pdg/marks.mli
+++ b/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
diff --git a/src/plugins/pdg/pdg_state.ml b/src/plugins/pdg/pdg_state.ml
index 276f231efbe10bc51e0dd8891540a12b56feb943..b5c081a3438d810f876fa6b30fe4f949be98804e 100644
--- a/src/plugins/pdg/pdg_state.ml
+++ b/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
diff --git a/src/plugins/pdg/pdg_state.mli b/src/plugins/pdg/pdg_state.mli
index a108bd99666eca31c374ce242e6a9c50e1a7134b..72f8297b41a2e8f42130aca2aed6dbe160cb99ce 100644
--- a/src/plugins/pdg/pdg_state.mli
+++ b/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 *)
diff --git a/src/plugins/pdg/pdg_tbl.ml b/src/plugins/pdg/pdg_tbl.ml
index 4961d4154bd684b566ae0f7310edd0436f5a6ce5..5603732213786a2cc7020bd13272323edd35081c 100644
--- a/src/plugins/pdg/pdg_tbl.ml
+++ b/src/plugins/pdg/pdg_tbl.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
type t = PdgTypes.Pdg.t
(**************************************************************************)
diff --git a/src/plugins/pdg/pdg_tbl.mli b/src/plugins/pdg/pdg_tbl.mli
index 73bfa5d76efbfacaebe42bf5fe69e4bab124fe33..541731a591138e8f100578e57827682b488da976 100644
--- a/src/plugins/pdg/pdg_tbl.mli
+++ b/src/plugins/pdg/pdg_tbl.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
type t = PdgTypes.Pdg.t
val self : State.t
diff --git a/src/plugins/pdg/register.ml b/src/plugins/pdg/register.ml
index 7f0f281e193f279d0d4462a75a5460e2f9f7e3ff..8217fb8ccc0794e95ec2b72c7178730c50fa990c 100644
--- a/src/plugins/pdg/register.ml
+++ b/src/plugins/pdg/register.ml
@@ -20,6 +20,9 @@
(* *)
(**************************************************************************)
+
+open Pdg_types
+
let () =
Cmdline.run_after_extended_stage
(fun () ->
diff --git a/src/plugins/pdg/sets.ml b/src/plugins/pdg/sets.ml
index 275477477b083ab80dca3d0e8df4ae8a95a30e96..846b30c2540db37082090965d0a76a07d422b553 100644
--- a/src/plugins/pdg/sets.ml
+++ b/src/plugins/pdg/sets.ml
@@ -23,6 +23,8 @@
(** Provides function to extract information from the PDG. *)
open Cil_types
+
+open Pdg_types
open PdgIndex
type nodes_and_undef =
diff --git a/src/plugins/pdg/sets.mli b/src/plugins/pdg/sets.mli
index a416d993e6975611bf9612afb1c25d71a28ee41d..27c12193321a174aad89fcd0e57f19643b355c6d 100644
--- a/src/plugins/pdg/sets.mli
+++ b/src/plugins/pdg/sets.mli
@@ -23,6 +23,7 @@
(** PDG (program dependence graph) access functions. *)
open Cil_types
+open Pdg_types
type nodes_and_undef =
(PdgTypes.Node.t * Locations.Zone.t option) list * Locations.Zone.t option
diff --git a/src/plugins/pdg_types/Pdg_types.ml b/src/plugins/pdg_types/Pdg_types.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a27209b47941a8551ffbe793be5f98d714307ea5
--- /dev/null
+++ b/src/plugins/pdg_types/Pdg_types.ml
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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 PdgIndex = PdgIndex
+module PdgMarks = PdgMarks
+module PdgTypes = PdgTypes
diff --git a/src/plugins/pdg_types/Pdg_types.mli b/src/plugins/pdg_types/Pdg_types.mli
new file mode 100644
index 0000000000000000000000000000000000000000..edc3a0fd49034f42631a26719c9338ac75e292ce
--- /dev/null
+++ b/src/plugins/pdg_types/Pdg_types.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2022 *)
+(* 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 PdgIndex: module type of PdgIndex
+module PdgMarks: module type of PdgMarks
+module PdgTypes: module type of PdgTypes
+
+(**************************************************************************)
diff --git a/src/plugins/pdg_types/dune b/src/plugins/pdg_types/dune
new file mode 100644
index 0000000000000000000000000000000000000000..08fe2686573b5510541e38b07e132b7fb6f6a2a6
--- /dev/null
+++ b/src/plugins/pdg_types/dune
@@ -0,0 +1,40 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2022 ;;
+;; 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). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Pdg-Types:" %{lib-available:frama-c-pdg-types.core} "\n")
+ )
+ )
+)
+
+( library
+ (name Pdg_types)
+ (optional)
+ (public_name frama-c-pdg-types.core)
+ (flags -open Frama_c_kernel :standard -w -9)
+ (libraries frama-c.kernel)
+)
+
+(plugin (optional) (name pdg-types) (libraries frama-c-pdg-types.core) (site (frama-c plugins)))
diff --git a/src/plugins/pdg_types/dune-project b/src/plugins/pdg_types/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..9766557fe25a5629efb30aa9da3d1019b5ba6ad7
--- /dev/null
+++ b/src/plugins/pdg_types/dune-project
@@ -0,0 +1,25 @@
+(lang dune 2.9)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2022 ;;
+;; 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). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(name frama-c-pdg_types)
+(using dune_site 0.1)
diff --git a/src/plugins/pdg_types/frama-c-pdg-types.opam b/src/plugins/pdg_types/frama-c-pdg-types.opam
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/kernel_externals/pdg_types/pdgIndex.ml b/src/plugins/pdg_types/pdgIndex.ml
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgIndex.ml
rename to src/plugins/pdg_types/pdgIndex.ml
diff --git a/src/kernel_externals/pdg_types/pdgIndex.mli b/src/plugins/pdg_types/pdgIndex.mli
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgIndex.mli
rename to src/plugins/pdg_types/pdgIndex.mli
diff --git a/src/kernel_externals/pdg_types/pdgMarks.ml b/src/plugins/pdg_types/pdgMarks.ml
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgMarks.ml
rename to src/plugins/pdg_types/pdgMarks.ml
diff --git a/src/kernel_externals/pdg_types/pdgMarks.mli b/src/plugins/pdg_types/pdgMarks.mli
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgMarks.mli
rename to src/plugins/pdg_types/pdgMarks.mli
diff --git a/src/kernel_externals/pdg_types/pdgTypes.ml b/src/plugins/pdg_types/pdgTypes.ml
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgTypes.ml
rename to src/plugins/pdg_types/pdgTypes.ml
diff --git a/src/kernel_externals/pdg_types/pdgTypes.mli b/src/plugins/pdg_types/pdgTypes.mli
similarity index 100%
rename from src/kernel_externals/pdg_types/pdgTypes.mli
rename to src/plugins/pdg_types/pdgTypes.mli
diff --git a/src/plugins/postdominators/dune b/src/plugins/postdominators/dune
index da173221feddee9605ea27c2754b1cc1f1329343..00091cf16bf4dddc404c0be88d3522041602223d 100644
--- a/src/plugins/postdominators/dune
+++ b/src/plugins/postdominators/dune
@@ -25,6 +25,7 @@
(deps (universe))
(action (progn
(echo "Postdominators:" %{lib-available:frama-c-postdominators.core} "\n")
+ (echo " - Pdg-Types:" %{lib-available:frama-c-pdg-types.core} "\n")
(echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
)
)
@@ -35,7 +36,7 @@
(optional)
(public_name frama-c-postdominators.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-eva.core)
+ (libraries frama-c.kernel frama-c-pdg-types.core frama-c-eva.core)
)
(plugin (optional) (name postdominators) (libraries frama-c-postdominators.core) (site (frama-c plugins)))
diff --git a/src/plugins/postdominators/print.ml b/src/plugins/postdominators/print.ml
index 99549e4fb683d54c1da5e3742978987cd47c6cb6..560c6965ce4f43f2a2b87e5e42cdcc93743b106e 100644
--- a/src/plugins/postdominators/print.ml
+++ b/src/plugins/postdominators/print.ml
@@ -23,7 +23,7 @@
open Cil_types
open Cil_datatype
-let pretty_stmt fmt s =
+let pretty_stmt fmt s = let open Pdg_types in
let key = PdgIndex.Key.stmt_key s in PdgIndex.Key.pretty fmt key
module Printer = struct
diff --git a/src/plugins/scope/defs.ml b/src/plugins/scope/defs.ml
index a73ef647869f8ca98983618ee9baf4c0dc36f05e..b7783e9f5e508440367136109324a5fb629805e9 100644
--- a/src/plugins/scope/defs.ml
+++ b/src/plugins/scope/defs.ml
@@ -27,6 +27,8 @@
open Cil_datatype
open Cil_types
+open Pdg_types
+
let debug1 fmt = Datascope.R.debug ~level:1 fmt
module Interproc =
diff --git a/src/plugins/scope/zones.ml b/src/plugins/scope/zones.ml
index bc98607ed3325adc948302ac3ac50aaa4cb67aa8..ba308e499fa2110d4aef18bbe2f29c18c890d9e8 100644
--- a/src/plugins/scope/zones.ml
+++ b/src/plugins/scope/zones.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
module R = Datascope.R
let debug1 fmt = R.debug ~level:1 fmt
let debug2 fmt = R.debug ~level:2 fmt
diff --git a/src/plugins/security_slicing/components.ml b/src/plugins/security_slicing/components.ml
index 1b76f3467bb45e0e6a16b60ef8314ded158967ae..e28a649eb889d5ade1e2af1bf5e0072e8607ad8b 100644
--- a/src/plugins/security_slicing/components.ml
+++ b/src/plugins/security_slicing/components.ml
@@ -23,6 +23,8 @@
open Cil_types
open Cil_datatype
+open Pdg_types
+
(* ************************************************************************* *)
(** {2 Searching security annotations} *)
(* ************************************************************************* *)
diff --git a/src/plugins/slicing/api.mli b/src/plugins/slicing/api.mli
index 2a0af61952fbb5e2b4ef8ed5550aed059a351773..c1b4b19a0d97e6391031f0fb39fb5ac64367937a 100644
--- a/src/plugins/slicing/api.mli
+++ b/src/plugins/slicing/api.mli
@@ -306,6 +306,8 @@ module Select : sig
(** {3 Pdg selectors.} *)
+ open Pdg_types
+
val select_pdg_nodes :
set -> Mark.t -> PdgTypes.Node.t list -> Cil_types.kernel_function -> set
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index 7e03ac911d06837dd2591203f26480e2fe19c278..43be72e63ec8990bfab89552dde3857cebd463e6 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -41,6 +41,7 @@
(**/**)
open Cil_types
+open Pdg_types
(**/**)
(* Look at (only once) the callers of [kf] ([kf] included). *)
diff --git a/src/plugins/slicing/fct_slice.mli b/src/plugins/slicing/fct_slice.mli
index 6ea3a114edbdc847d41731dc0d04e4ec1dd20157..a6dd86470f6aa83f972912dad981089fbfeb2468 100644
--- a/src/plugins/slicing/fct_slice.mli
+++ b/src/plugins/slicing/fct_slice.mli
@@ -23,6 +23,8 @@
open SlicingInternals
open Cil_types
+open Pdg_types
+
(** Return [true] if the source function is called
* (even indirectly via transitivity) from a [Slice.t]. *)
val is_src_fun_called :
diff --git a/src/plugins/slicing/printSlice.ml b/src/plugins/slicing/printSlice.ml
index 1775db3293c44358663853cb1d390b7a6314d28f..535e841b34be8791091c1f102f0074fafb09fa86 100644
--- a/src/plugins/slicing/printSlice.ml
+++ b/src/plugins/slicing/printSlice.ml
@@ -26,6 +26,8 @@
open Cil_types
+open Pdg_types
+
(**/**)
let find_sub_stmts st = match st.skind with
diff --git a/src/plugins/slicing/printSlice.mli b/src/plugins/slicing/printSlice.mli
index dbf55bac1d788e64a6a64727a937478b5402a153..f3ad3570b12b39cc771b39339d2277b03384d5ba 100644
--- a/src/plugins/slicing/printSlice.mli
+++ b/src/plugins/slicing/printSlice.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
val print_fct_from_pdg :
Format.formatter ->
?ff:SlicingInternals.fct_slice -> PdgTypes.Pdg.t -> unit
diff --git a/src/plugins/slicing/slicingActions.ml b/src/plugins/slicing/slicingActions.ml
index 8fd243d8a9640049a4b7b5875c5dc1d1884f5656..0f8410e0446c633e8f855b3425c5993cfa613999 100644
--- a/src/plugins/slicing/slicingActions.ml
+++ b/src/plugins/slicing/slicingActions.ml
@@ -27,6 +27,8 @@
(**/**)
+open Pdg_types
+
type select = SlicingTypes.sl_mark PdgMarks.select
type n_or_d_marks = (SlicingInternals.node_or_dpds * SlicingInternals.pdg_mark) list
diff --git a/src/plugins/slicing/slicingActions.mli b/src/plugins/slicing/slicingActions.mli
index 314a61918cb4e25f67b595d8a499d9d9940c3a8d..081e5bbb6822e1adb85919bfc86037cb7b9a62f6 100644
--- a/src/plugins/slicing/slicingActions.mli
+++ b/src/plugins/slicing/slicingActions.mli
@@ -22,6 +22,9 @@
open SlicingTypes
open Cil_types
+
+open Pdg_types
+
open SlicingInternals
type select = sl_mark PdgMarks.select
diff --git a/src/plugins/slicing/slicingCmds.mli b/src/plugins/slicing/slicingCmds.mli
index a54c67ba31adc7806433769f1d1ca5cb56d70666..693aa337f1c05aa23fbf27b9680e3a132ab2c66b 100644
--- a/src/plugins/slicing/slicingCmds.mli
+++ b/src/plugins/slicing/slicingCmds.mli
@@ -22,6 +22,8 @@
open Cil_types
+open Pdg_types
+
(* TODO: This .mli exists mainly to avoid problems with 'make -j'. This API
is too vast and must be simplified. For example, functions should not
receive variables as names (ie. strings) but directly as zones, possibly
diff --git a/src/plugins/slicing/slicingInternals.ml b/src/plugins/slicing/slicingInternals.ml
index 4169f6937d3d208c157d24e958faf9d96b4aea93..df18b5d589c2cbff6be1b02017156f92ce4478fa 100644
--- a/src/plugins/slicing/slicingInternals.ml
+++ b/src/plugins/slicing/slicingInternals.ml
@@ -27,6 +27,8 @@
open Cil_datatype
+open Pdg_types
+
(** {3 About options} *)
(** associate a level to each function in order to control how it will be
diff --git a/src/plugins/slicing/slicingInternals.mli b/src/plugins/slicing/slicingInternals.mli
index 0e6dc51a49ccfd353bbe3d0e3c6729e68a48eb96..2c7de6f72a77653826a563428b842f379e2d204c 100644
--- a/src/plugins/slicing/slicingInternals.mli
+++ b/src/plugins/slicing/slicingInternals.mli
@@ -27,6 +27,8 @@
open Cil_datatype
+open Pdg_types
+
(** {3 About options} *)
(** associate a level to each function in order to control how it will be
diff --git a/src/plugins/slicing/slicingMacros.ml b/src/plugins/slicing/slicingMacros.ml
index 05df109b3523a6e2511063a6c3159cdef05bba97..56dc2b438bd9b2024a9d642932e6aef85e96230b 100644
--- a/src/plugins/slicing/slicingMacros.ml
+++ b/src/plugins/slicing/slicingMacros.ml
@@ -28,6 +28,8 @@
open Cil_types
+open Pdg_types
+
(**/**)
(** {2 Options} *)
diff --git a/src/plugins/slicing/slicingMacros.mli b/src/plugins/slicing/slicingMacros.mli
index 183aff57436bece183f79b5ae6439e14eebde20a..427b60450b8ccffe98994cb4c62dac41866746a0 100644
--- a/src/plugins/slicing/slicingMacros.mli
+++ b/src/plugins/slicing/slicingMacros.mli
@@ -24,6 +24,8 @@
functions below should be inlined, as there is no good reason to treat
those types as semi-private *)
+open Pdg_types
+
open SlicingInternals
val str_level_option : level_option -> string
diff --git a/src/plugins/slicing/slicingMarks.ml b/src/plugins/slicing/slicingMarks.ml
index d32603122c23f6479a4139c1d7f4194016ba25ca..77e2c60002dc6e95b15e94a4df90e970610dc68b 100644
--- a/src/plugins/slicing/slicingMarks.ml
+++ b/src/plugins/slicing/slicingMarks.ml
@@ -22,6 +22,8 @@
(** Everything related with the marks. Mainly quite low level function. *)
+open Pdg_types
+
(**/**)
let debug = false
diff --git a/src/plugins/slicing/slicingMarks.mli b/src/plugins/slicing/slicingMarks.mli
index d398c3967fdaec9c47b1e2aa9a4cbd5fc79a47af..fd4505c96de75d7990f83b99007cd56f8c7f1894 100644
--- a/src/plugins/slicing/slicingMarks.mli
+++ b/src/plugins/slicing/slicingMarks.mli
@@ -22,6 +22,8 @@
open SlicingTypes
+open Pdg_types
+
val bottom_mark : sl_mark
val mk_user_mark : data:bool -> addr:bool -> ctrl:bool -> sl_mark
diff --git a/src/plugins/slicing/slicingProject.ml b/src/plugins/slicing/slicingProject.ml
index 27cca02339737ad74f510c4dfec8679ccc6b8a34..70ee325043535f43c8ae87624cf22f940addbc75 100644
--- a/src/plugins/slicing/slicingProject.ml
+++ b/src/plugins/slicing/slicingProject.ml
@@ -24,6 +24,8 @@
(**/**)
+open Pdg_types
+
module T = SlicingInternals
module M = SlicingMacros
diff --git a/src/plugins/slicing/slicingSelect.ml b/src/plugins/slicing/slicingSelect.ml
index 4b3c23c291358f60965b5e1d3f46fe69669db7a9..cf279d65247463b02cf17fc8c0155f90ea46b625 100644
--- a/src/plugins/slicing/slicingSelect.ml
+++ b/src/plugins/slicing/slicingSelect.ml
@@ -23,6 +23,8 @@
open Cil_types
open Cil_datatype
+open Pdg_types
+
(* ---------------------------------------------------------------------- *)
(** {1 For internal use} *)
diff --git a/src/plugins/slicing/slicingSelect.mli b/src/plugins/slicing/slicingSelect.mli
index 6f682ad27359f5a36480aa723f3a6375ad84db53..f68618af4ab69e2871793680ace383a3a673be89 100644
--- a/src/plugins/slicing/slicingSelect.mli
+++ b/src/plugins/slicing/slicingSelect.mli
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
val check_call : Cil_types.stmt -> bool -> Cil_types.stmt
val print_select :
diff --git a/src/plugins/slicing/slicingTransform.ml b/src/plugins/slicing/slicingTransform.ml
index f142150160d6e9cddff46dc432a841c9b8a89707..2915223eec08c36ed39b517038169b951525e899 100644
--- a/src/plugins/slicing/slicingTransform.ml
+++ b/src/plugins/slicing/slicingTransform.ml
@@ -26,6 +26,8 @@
open Cil_types
open Cil
+open Pdg_types
+
(**/**)
module Visibility (SliceName : sig
diff --git a/src/plugins/slicing/slicingTypes.ml b/src/plugins/slicing/slicingTypes.ml
index 343d08a8f13a70053957f7cbb3de2133a0394a8c..e370df2269d2401259075c7ed22268b86ea5f6a2 100644
--- a/src/plugins/slicing/slicingTypes.ml
+++ b/src/plugins/slicing/slicingTypes.ml
@@ -22,6 +22,8 @@
(** Slicing module types. *)
+open Pdg_types
+
exception Slicing_Internal_Error of string
exception ChangeCallErr of string
exception PtrCallExpr
diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml
index 314e896c6623360091597b69135ee77d16e2ac1b..bc433062ccc8929f0be579864f7878a07a6f8cee 100644
--- a/src/plugins/sparecode/spare_marks.ml
+++ b/src/plugins/sparecode/spare_marks.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Pdg_types
+
let debug n format = Sparecode_params.debug ~level:n format
let fatal fmt = Sparecode_params.fatal fmt
diff --git a/src/plugins/sparecode/spare_marks.mli b/src/plugins/sparecode/spare_marks.mli
index 92a003570b041fa3cf7509dbaa3efff0b6dae067..d6e60878d7c11c498afe8e03592bf2a2331fb8ff 100644
--- a/src/plugins/sparecode/spare_marks.mli
+++ b/src/plugins/sparecode/spare_marks.mli
@@ -21,6 +21,7 @@
(**************************************************************************)
open Cil_types
+open Pdg_types
type proj
type fct
diff --git a/src/plugins/sparecode/transform.ml b/src/plugins/sparecode/transform.ml
index b22d74c35c074d271243109f7191e4bffab99370..0e3ae5a6f1b496506585981e777937a9a7ef387a 100644
--- a/src/plugins/sparecode/transform.ml
+++ b/src/plugins/sparecode/transform.ml
@@ -23,6 +23,8 @@
open Cil_types
open Cil
+open Pdg_types
+
module BoolInfo = struct
type proj = Spare_marks.proj
type fct = Spare_marks.fct option * Kernel_function.t