From 44c995c88ab36adb93a0c114e7912ef5688995ab Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 29 Jun 2022 14:41:27 +0200
Subject: [PATCH] [Pdg_types] new plug-in
---
src/plugins/impact/compute_impact.ml | 3 ++
src/plugins/impact/compute_impact.mli | 2 +
src/plugins/impact/gui/register_gui.ml | 1 +
src/plugins/impact/pdg_aux.ml | 2 +-
src/plugins/impact/pdg_aux.mli | 2 +
src/plugins/impact/reason_graph.ml | 2 +
src/plugins/impact/reason_graph.mli | 2 +
src/plugins/impact/register.ml | 2 +
src/plugins/impact/register.mli | 2 +
src/plugins/pdg/annot.ml | 2 +
src/plugins/pdg/annot.mli | 2 +
src/plugins/pdg/api.ml | 2 +
src/plugins/pdg/api.mli | 2 +
src/plugins/pdg/build.ml | 2 +
src/plugins/pdg/build.mli | 2 +
src/plugins/pdg/dune | 3 +-
src/plugins/pdg/marks.ml | 4 +-
src/plugins/pdg/marks.mli | 2 +
src/plugins/pdg/pdg_state.ml | 2 +
src/plugins/pdg/pdg_state.mli | 2 +
src/plugins/pdg/pdg_tbl.ml | 2 +
src/plugins/pdg/pdg_tbl.mli | 2 +
src/plugins/pdg/register.ml | 3 ++
src/plugins/pdg/sets.ml | 2 +
src/plugins/pdg/sets.mli | 1 +
src/plugins/pdg_types/Pdg_types.ml | 25 ++++++++++++
src/plugins/pdg_types/Pdg_types.mli | 27 +++++++++++++
src/plugins/pdg_types/dune | 40 +++++++++++++++++++
src/plugins/pdg_types/dune-project | 25 ++++++++++++
src/plugins/pdg_types/frama-c-pdg-types.opam | 0
.../pdg_types/pdgIndex.ml | 0
.../pdg_types/pdgIndex.mli | 0
.../pdg_types/pdgMarks.ml | 0
.../pdg_types/pdgMarks.mli | 0
.../pdg_types/pdgTypes.ml | 0
.../pdg_types/pdgTypes.mli | 0
src/plugins/postdominators/dune | 3 +-
src/plugins/postdominators/print.ml | 2 +-
src/plugins/scope/defs.ml | 2 +
src/plugins/scope/zones.ml | 2 +
src/plugins/security_slicing/components.ml | 2 +
src/plugins/slicing/api.mli | 2 +
src/plugins/slicing/fct_slice.ml | 1 +
src/plugins/slicing/fct_slice.mli | 2 +
src/plugins/slicing/printSlice.ml | 2 +
src/plugins/slicing/printSlice.mli | 2 +
src/plugins/slicing/slicingActions.ml | 2 +
src/plugins/slicing/slicingActions.mli | 3 ++
src/plugins/slicing/slicingCmds.mli | 2 +
src/plugins/slicing/slicingInternals.ml | 2 +
src/plugins/slicing/slicingInternals.mli | 2 +
src/plugins/slicing/slicingMacros.ml | 2 +
src/plugins/slicing/slicingMacros.mli | 2 +
src/plugins/slicing/slicingMarks.ml | 2 +
src/plugins/slicing/slicingMarks.mli | 2 +
src/plugins/slicing/slicingProject.ml | 2 +
src/plugins/slicing/slicingSelect.ml | 2 +
src/plugins/slicing/slicingSelect.mli | 2 +
src/plugins/slicing/slicingTransform.ml | 2 +
src/plugins/slicing/slicingTypes.ml | 2 +
src/plugins/sparecode/spare_marks.ml | 2 +
src/plugins/sparecode/spare_marks.mli | 1 +
src/plugins/sparecode/transform.ml | 2 +
63 files changed, 219 insertions(+), 5 deletions(-)
create mode 100644 src/plugins/pdg_types/Pdg_types.ml
create mode 100644 src/plugins/pdg_types/Pdg_types.mli
create mode 100644 src/plugins/pdg_types/dune
create mode 100644 src/plugins/pdg_types/dune-project
create mode 100644 src/plugins/pdg_types/frama-c-pdg-types.opam
rename src/{kernel_externals => plugins}/pdg_types/pdgIndex.ml (100%)
rename src/{kernel_externals => plugins}/pdg_types/pdgIndex.mli (100%)
rename src/{kernel_externals => plugins}/pdg_types/pdgMarks.ml (100%)
rename src/{kernel_externals => plugins}/pdg_types/pdgMarks.mli (100%)
rename src/{kernel_externals => plugins}/pdg_types/pdgTypes.ml (100%)
rename src/{kernel_externals => plugins}/pdg_types/pdgTypes.mli (100%)
diff --git a/src/plugins/impact/compute_impact.ml b/src/plugins/impact/compute_impact.ml
index f8d9abc1c11..9f1379f3ec9 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 64307dc6628..74831f03df7 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 bdbc771e13c..1bd988cb199 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 c36b4d651b9..0a3b4acb21e 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 fa3bcde2b5f..f07aca633a1 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 f3242116b75..eb8452ccdd3 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 d0f03c55694..ccdbd733b22 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 6dfc46429bd..e9b09ca1784 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 a426a0bb2b2..7cdc3c04753 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 00b327ff190..09c37fa9437 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 8aa29637584..c46dd70667d 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 6f6df8d3b0a..0024018d796 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 89b6912d3f1..6094779cec4 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 256f3d9f998..34dfb781a9a 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 583fdbc4730..6e134517409 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 09b16b19607..1465f8006ad 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 520249051f0..6330ce5fb40 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 55a303293f9..846aeae6ada 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 276f231efbe..b5c081a3438 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 a108bd99666..72f8297b41a 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 4961d4154bd..56037322137 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 73bfa5d76ef..541731a5911 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 7f0f281e193..8217fb8ccc0 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 275477477b0..846b30c2540 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 a416d993e69..27c12193321 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 00000000000..a27209b4794
--- /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 00000000000..edc3a0fd490
--- /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 00000000000..08fe2686573
--- /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 00000000000..9766557fe25
--- /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 00000000000..e69de29bb2d
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 da173221fed..00091cf16bf 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 99549e4fb68..560c6965ce4 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 a73ef647869..b7783e9f5e5 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 bc98607ed33..ba308e499fa 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 1b76f3467bb..e28a649eb88 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 2a0af61952f..c1b4b19a0d9 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 7e03ac911d0..43be72e63ec 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 6ea3a114edb..a6dd86470f6 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 1775db3293c..535e841b34b 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 dbf55bac1d7..f3ad3570b12 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 8fd243d8a96..0f8410e0446 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 314a61918cb..081e5bbb682 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 a54c67ba31a..693aa337f1c 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 4169f6937d3..df18b5d589c 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 0e6dc51a49c..2c7de6f72a7 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 05df109b352..56dc2b438bd 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 183aff57436..427b60450b8 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 d32603122c2..77e2c60002d 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 d398c3967fd..fd4505c96de 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 27cca023397..70ee3250435 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 4b3c23c2913..cf279d65247 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 6f682ad2735..f68618af4ab 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 f142150160d..2915223eec0 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 343d08a8f13..e370df2269d 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 314e896c662..bc433062ccc 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 92a003570b0..d6e60878d7c 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 b22d74c35c0..0e3ae5a6f1b 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
--
GitLab