diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 76c8222d724d27a819828530e4510964c0f8bd99..f323723913ff81e47e916b9d3de563ff5198df9a 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -47,116 +47,6 @@ module Toplevel = struct
end
-(* ************************************************************************* *)
-(** {2 Inouts} *)
-(* ************************************************************************* *)
-
-module type INOUTKF = sig
- type t
- val self_internal: State.t ref
- val self_external: State.t ref
- val compute : (kernel_function -> unit) ref
-
- val get_internal : (kernel_function -> t) ref
- val get_external : (kernel_function -> t) ref
-
- val display : (Format.formatter -> kernel_function -> unit) ref
- val pretty : Format.formatter -> t -> unit
-end
-module type INOUT = sig
- include INOUTKF
- val statement : (stmt -> t) ref
- val kinstr : kinstr -> t option
-end
-
-(** State_builder.of outputs
- - over-approximation of zones written by each function. *)
-module Outputs = struct
- type t = Locations.Zone.t
- let self_internal = ref State.dummy
- let self_external = ref State.dummy
- let compute = mk_fun "Out.compute"
- let display = mk_fun "Out.display"
- let display_external = mk_fun "Out.display_external"
- let get_internal = mk_fun "Out.get_internal"
- let get_external = mk_fun "Out.get_external"
- let statement = mk_fun "Out.statement"
- let kinstr ki = match ki with
- | Kstmt s -> Some (!statement s)
- | Kglobal -> None
-
- let pretty = Locations.Zone.pretty
-end
-
-(** State_builder.of read inputs
- - over-approximation of locations read by each function. *)
-module Inputs = struct
- (* What about [Inputs.statement] ? *)
- type t = Locations.Zone.t
- let self_internal = ref State.dummy
- let self_external = ref State.dummy
- let self_with_formals = ref State.dummy
- let compute = mk_fun "Inputs.compute"
- let display = mk_fun "Inputs.display"
- let display_with_formals = mk_fun "Inputs.display_with_formals"
- let get_internal = mk_fun "Inputs.get_internal"
- let get_external = mk_fun "Inputs.get_external"
- let get_with_formals = mk_fun "Inputs.get_with_formals"
- let statement = mk_fun "Inputs.statement"
- let expr = mk_fun "Inputs.expr"
- let kinstr ki = match ki with
- | Kstmt s -> Some (!statement s)
- | Kglobal -> None
-
- let pretty = Locations.Zone.pretty
-end
-
-(** State_builder.of operational inputs
- - over-approximation of zones whose input values are read by each function,
- State_builder.of sure outputs
- - under-approximation of zones written by each function. *)
-module Operational_inputs = struct
- type t = Inout_type.t
- let self_internal = ref State.dummy
- let self_external = ref State.dummy
- let compute = mk_fun "Operational_inputs.compute"
- let display = mk_fun "Operational_inputs.display"
- let get_internal = mk_fun "Operational_inputs.get_internal"
- let get_internal_precise = ref (fun ?stmt:_ _ ->
- failwith ("Db.Operational_inputs.get_internal_precise not implemented"))
- let get_external = mk_fun "Operational_inputs.get_external"
-
- module Record_Inout_Callbacks = Hook.Build (struct type t = Inout_type.t end)
-
- let pretty fmt x =
- Format.fprintf fmt "@[<v>";
- Format.fprintf fmt "@[<v 2>Operational inputs:@ @[<hov>%a@]@]@ "
- Locations.Zone.pretty (x.Inout_type.over_inputs);
- Format.fprintf fmt "@[<v 2>Operational inputs on termination:@ @[<hov>%a@]@]@ "
- Locations.Zone.pretty (x.Inout_type.over_inputs_if_termination);
- Format.fprintf fmt "@[<v 2>Sure outputs:@ @[<hov>%a@]@]"
- Locations.Zone.pretty (x.Inout_type.under_outputs_if_termination);
- Format.fprintf fmt "@]";
-
-end
-
-(** Derefs computations *)
-module Derefs = struct
- type t = Locations.Zone.t
- let self_internal = ref State.dummy
- let self_external = ref State.dummy
- let compute = mk_fun "Derefs.compute"
- let display = mk_fun "Derefs.display"
- let get_internal = mk_fun "Derefs.get_internal"
- let get_external = mk_fun "Derefs.get_external"
- let statement = mk_fun "Derefs.statement"
- let kinstr ki = match ki with
- | Kstmt s -> Some (!statement s)
- | Kglobal -> None
-
- let pretty = Locations.Zone.pretty
-end
-
(* ************************************************************************* *)
(** {2 Others plugins} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index e191d7d2f3a86fb7c5051f3a12871de0d30e42c5..65434ec1c10b30865c561fd3cc07268907b105e4 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -145,91 +145,6 @@ module Security : sig
end
-(** Signature common to some Inout plugin options. The results of
- the computations are available on a per function basis. *)
-module type INOUTKF = sig
-
- type t
-
- val self_internal: State.t ref
- val self_external: State.t ref
-
- val compute : (kernel_function -> unit) ref
-
- val get_internal : (kernel_function -> t) ref
- (** Inputs/Outputs with local and formal variables *)
-
- val get_external : (kernel_function -> t) ref
- (** Inputs/Outputs without either local or formal variables *)
-
- (** {3 Pretty printing} *)
-
- val display : (Format.formatter -> kernel_function -> unit) ref
- val pretty : Format.formatter -> t -> unit
-
-end
-
-(** Signature common to inputs and outputs computations. The results
- are also available on a per-statement basis. *)
-module type INOUT = sig
- include INOUTKF
-
- val statement : (stmt -> t) ref
- val kinstr : kinstr -> t option
-end
-
-(** State_builder.of read inputs.
- That is over-approximation of zones read by each function.
- @see <../inout/Inputs.html> internal documentation. *)
-module Inputs : sig
-
- include INOUT with type t = Locations.Zone.t
-
- val expr : (stmt -> exp -> t) ref
-
- val self_with_formals: State.t ref
-
- val get_with_formals : (kernel_function -> t) ref
- (** Inputs with formals and without local variables *)
-
- val display_with_formals: (Format.formatter -> kernel_function -> unit) ref
-
-end
-
-(** State_builder.of outputs.
- That is over-approximation of zones written by each function.
- @see <../inout/Outputs.html> internal documentation. *)
-module Outputs : sig
- include INOUT with type t = Locations.Zone.t
- val display_external : (Format.formatter -> kernel_function -> unit) ref
-end
-
-(** State_builder.of operational inputs.
- That is:
- - over-approximation of zones whose input values are read by each function,
- State_builder.of sure outputs
- - under-approximation of zones written by each function.
- @see <../inout/Context.html> internal documentation. *)
-module Operational_inputs : sig
- include INOUTKF with type t = Inout_type.t
- val get_internal_precise: (?stmt:stmt -> kernel_function -> Inout_type.t) ref
- (** More precise version of [get_internal] function. If [stmt] is
- specified, and is a possible call to the given kernel_function,
- returns the operational inputs for this call. *)
-
- (**/**)
- (* Internal use *)
- module Record_Inout_Callbacks: Hook.Iter_hook with type param = Inout_type.t
- (**/**)
-end
-
-
-(**/**)
-(** Do not use yet.
- @see <../inout/Derefs.html> internal documentation. *)
-module Derefs : INOUT with type t = Locations.Zone.t
-(**/**)
-
(** {3 GUI} *)
(** This function should be called from time to time by all analysers taking
diff --git a/src/plugins/eva/domains/cvalue/cvalue_domain.ml b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
index 132a3c72d5f5331e826d9407e0225e7a990e5c53..39ec5355a64d49e3646f7721c831d14d4650ae2c 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_domain.ml
@@ -411,7 +411,7 @@ module State = struct
then Cvalue.Model.cardinal_estimate values
else Cvalue.CardinalEstimate.one
in
- let outs = !Db.Outputs.get_internal kf in
+ let outs = Inout.Outputs.get_internal kf in
let outs = Locations.Zone.filter_base filter_generated_and_locals outs in
let header fmt =
Format.fprintf fmt "Values at end of function %a:%t"
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 165dbf57cdd5ec0b314d7c4b61ebebdcce064906..710cda5a2cff886b794f754bfd9b4bd5cb6e5cea 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -56,7 +56,7 @@ module InOutCallback =
end)
let register_callback () =
- Db.Operational_inputs.Record_Inout_Callbacks.extend_once InOutCallback.set
+ Inout.Operational_inputs.Record_Inout_Callbacks.extend_once InOutCallback.set
let () = Cmdline.run_after_configuring_stage register_callback
diff --git a/src/plugins/eva/gui/register_gui.ml b/src/plugins/eva/gui/register_gui.ml
index a24c62d362d1fe156c12b79bb0e41a63ae847d5b..66a19c086f5bce7e14e29d87dd0e65df57f189d1 100644
--- a/src/plugins/eva/gui/register_gui.ml
+++ b/src/plugins/eva/gui/register_gui.ml
@@ -46,8 +46,8 @@ let used_var = UsedVarState.memo
Function_calls.partial_results () ||
try
let f = fst (Globals.entry_point ()) in
- let inputs = !Db.Inputs.get_external f in
- let outputs = !Db.Outputs.get_external f in
+ let inputs = Inout.Inputs.get_external f in
+ let outputs = Inout.Outputs.get_external f in
let b = Base.of_varinfo var in
Locations.Zone.mem_base b inputs || Locations.Zone.mem_base b outputs
with e ->
@@ -227,7 +227,7 @@ let gui_compute_values (main_ui:main_ui) =
then main_ui#launcher ()
let cleaned_outputs kf s =
- let outs = Db.Outputs.kinstr (Kstmt s) in
+ let outs = Inout.Outputs.kinstr (Kstmt s) in
let accept = Logic_inout.accept_base ~formals:true ~locals:true kf in
let filter = Locations.Zone.filter_base accept in
Option.map filter outs
@@ -251,7 +251,7 @@ let pretty_stmt_info (main_ui:main_ui) kf stmt =
match outs with
| Some outs ->
main_ui#pretty_information
- "Modifies @[<hov>%a@]@." Db.Outputs.pretty outs
+ "Modifies @[<hov>%a@]@." Locations.Zone.pretty outs
| _ -> ()
end
else main_ui#pretty_information "This code is dead@."
diff --git a/src/plugins/eva/utils/inout.ml b/src/plugins/eva/utils/inout.ml
new file mode 100644
index 0000000000000000000000000000000000000000..399e26b1c5cf3ffacbeed0afd2e85141e344edb0
--- /dev/null
+++ b/src/plugins/eva/utils/inout.ml
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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 Outputs = struct
+ let ref_statement = ref (fun _ -> assert false)
+ let ref_get_external = ref (fun _ -> assert false)
+ let ref_get_internal = ref (fun _ -> assert false)
+
+ let kinstr = function
+ | Cil_types.Kstmt s -> Some (!ref_statement s)
+ | Kglobal -> None
+
+ let get_external kf = !ref_get_external kf
+ let get_internal kf = !ref_get_internal kf
+end
+
+module Inputs = struct
+ let ref_get_external = ref (fun _ -> assert false)
+
+ let get_external kf = !ref_get_external kf
+end
+
+(** State_builder.of operational inputs
+ - over-approximation of zones whose input values are read by each function,
+ State_builder.of sure outputs
+ - under-approximation of zones written by each function. *)
+module Operational_inputs = struct
+ module Record_Inout_Callbacks = Hook.Build (struct type t = Inout_type.t end)
+end
diff --git a/src/plugins/eva/utils/inout.mli b/src/plugins/eva/utils/inout.mli
new file mode 100644
index 0000000000000000000000000000000000000000..087dd3643418154c6b489976d9b1f6c53b6635f4
--- /dev/null
+++ b/src/plugins/eva/utils/inout.mli
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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 Outputs :
+sig
+ val ref_statement : (Cil_types.stmt -> Locations.Zone.t) ref
+ val ref_get_external : (Cil_types.kernel_function -> Locations.Zone.t) ref
+ val ref_get_internal : (Cil_types.kernel_function -> Locations.Zone.t) ref
+
+ val kinstr : Cil_types.kinstr -> Locations.Zone.t option
+ val get_external : Cil_types.kernel_function -> Locations.Zone.t
+ val get_internal : Cil_types.kernel_function -> Locations.Zone.t
+end
+
+module Inputs :
+sig
+ val ref_get_external : (Cil_types.kernel_function -> Locations.Zone.t) ref
+ val get_external : Cil_types.kernel_function -> Locations.Zone.t
+end
+
+(** State_builder.of operational inputs.
+ That is:
+ - over-approximation of zones whose input values are read by each function,
+ State_builder.of sure outputs
+ - under-approximation of zones written by each function.
+ @see <../inout/Context.html> internal documentation. *)
+module Operational_inputs : sig
+ (**/**)
+ (* Internal use *)
+ module Record_Inout_Callbacks: Hook.Iter_hook with type param = Inout_type.t
+ (**/**)
+end
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index e4a368655a9c996dcafcb0369e4ba346cfa6549b..15a046d096a85208e713ed065e62ad2fe4321ba0 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -41,6 +41,7 @@ module Eval_op = Eval_op
module Eval_terms = Eval_terms
module Eval_typ = Eval_typ
module Function_calls = Function_calls
+module Inout = Inout
module Logic_inout = Logic_inout
module Main_locations = Main_locations
module Main_values = Main_values
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index f70377152869169e4763bef80aca6d553384f555..6386a914cd85aeff495d910622c80846b4651cb1 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -45,6 +45,7 @@ module Eval_op = Eval_op
module Eval_terms = Eval_terms
module Eval_typ = Eval_typ
module Function_calls = Function_calls
+module Inout = Inout
module Logic_inout = Logic_inout
module Main_locations = Main_locations
module Main_values = Main_values
diff --git a/src/plugins/impact/pdg_aux.ml b/src/plugins/impact/pdg_aux.ml
index c6ecfcf8c6e1793e3940436dbdd537fd26820fcf..a486d6adbac42a5d101fc50b2341caddd9689fbb 100644
--- a/src/plugins/impact/pdg_aux.ml
+++ b/src/plugins/impact/pdg_aux.ml
@@ -167,7 +167,7 @@ let find_call_input_nodes pdg_caller call_stmt ?(z=Locations.Zone.top) in_key =
let all_call_input_nodes ~caller:pdg_caller ~callee:(kf_callee, pdg_callee) call_stmt =
let real_inputs =
let inout =
- !Db.Operational_inputs.get_internal_precise ~stmt:call_stmt kf_callee
+ Inout.Operational_inputs.get_internal_precise ~stmt:call_stmt kf_callee
in
inout.Inout_type.over_inputs_if_termination
in
diff --git a/src/plugins/inout/derefs.ml b/src/plugins/inout/derefs.ml
index f7115d4022ae2503fef641665d006bc87f515814..0a1d04589e82846f82e0d9d2ca291eb77bb0f564 100644
--- a/src/plugins/inout/derefs.ml
+++ b/src/plugins/inout/derefs.ml
@@ -108,12 +108,3 @@ let pretty_external fmt kf =
Format.fprintf fmt "@[Derefs for function %a:@\n@[<hov 2> %a@]@]@\n"
Kernel_function.pretty kf
Zone.pretty (get_external kf)
-
-let () =
- Db.Derefs.self_internal := Analysis.Memo.self;
- Db.Derefs.self_external := Externals.self;
- Db.Derefs.get_internal := get_internal;
- Db.Derefs.get_external := get_external;
- Db.Derefs.compute := compute_external;
- Db.Derefs.display := pretty_external;
- Db.Derefs.statement := Analysis.statement
diff --git a/src/plugins/inout/inputs.ml b/src/plugins/inout/inputs.ml
index 1de8961fa3ebe407c16537cbf034c4663c99b7cc..b99014f2018a46882efb4164e9aa710cd3ffd528 100644
--- a/src/plugins/inout/inputs.ml
+++ b/src/plugins/inout/inputs.ml
@@ -163,7 +163,7 @@ let get_with_formals kf =
(Eva.Logic_inout.accept_base ~formals:true ~locals:false kf)
(get_internal kf)
-let compute_external kf = ignore (get_external kf)
+let compute kf = ignore (get_external kf)
let pretty_external fmt kf =
Format.fprintf fmt "@[Inputs for function %a:@\n@[<hov 2> %a@]@]@\n"
@@ -175,18 +175,12 @@ let pretty_with_formals fmt kf =
Kernel_function.pretty kf
Zone.pretty (get_with_formals kf)
+let self = Externals.self
+let statement = Analysis.statement
+let expr = Analysis.expr
+
let () =
- Db.Inputs.self_internal := Analysis.Memo.self;
- Db.Inputs.self_external := Externals.self;
- Db.Inputs.self_with_formals := Analysis.Memo.self;
- Db.Inputs.get_internal := get_internal;
- Db.Inputs.get_external := get_external;
- Db.Inputs.get_with_formals := get_with_formals;
- Db.Inputs.compute := compute_external;
- Db.Inputs.display := pretty_external;
- Db.Inputs.display_with_formals := pretty_with_formals;
- Db.Inputs.statement := Analysis.statement;
- Db.Inputs.expr := Analysis.expr
+ Eva__Private.Inout.Inputs.ref_get_external := get_external
(*
Local Variables:
diff --git a/src/plugins/inout/inputs.mli b/src/plugins/inout/inputs.mli
index 593785adddf69a80bc119b45334780faae2e4596..93148f6a94ee91ca176417a29789b30b1ac6f591 100644
--- a/src/plugins/inout/inputs.mli
+++ b/src/plugins/inout/inputs.mli
@@ -20,5 +20,13 @@
(* *)
(**************************************************************************)
+val self: State.t
+
+val compute: Cil_types.kernel_function -> unit
+val get_external: Cil_types.kernel_function -> Locations.Zone.t
+val get_internal: Cil_types.kernel_function -> Locations.Zone.t
+val statement: Cil_types.stmt -> Locations.Zone.t
+val expr: Cil_types.stmt -> Cil_types.exp -> Locations.Zone.t
+
val pretty_external: Format.formatter -> Cil_types.kernel_function -> unit
val pretty_with_formals: Format.formatter -> Cil_types.kernel_function -> unit
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 8f658d124e1c51fbe723c13c3b731e1920b93332..227ac8101ebf27b3136417287d9e63f0389156cb 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -486,19 +486,23 @@ let compute_externals_using_prototype ?stmt kf =
let internals = compute_using_prototype ?stmt kf in
externalize ~with_formals:false kf internals
+let ref_get_internal = ref (fun _kf : t -> assert false)
+
let get_internal_aux ?stmt kf =
match stmt with
- | None -> !Db.Operational_inputs.get_internal kf
+ | None -> !ref_get_internal kf
| Some stmt ->
try CallwiseResults.find (kf, Kstmt stmt)
with Not_found ->
if Eva.Analysis.use_spec_instead_of_definition kf then
compute_using_prototype ~stmt kf
- else !Db.Operational_inputs.get_internal kf
+ else !ref_get_internal kf
+
+let ref_get_external = ref (fun _kf : t -> assert false)
let get_external_aux ?stmt kf =
match stmt with
- | None -> !Db.Operational_inputs.get_external kf
+ | None -> !ref_get_external kf
| Some stmt ->
try
let internals = CallwiseResults.find (kf, Kstmt stmt) in
@@ -508,7 +512,7 @@ let get_external_aux ?stmt kf =
let r = compute_externals_using_prototype ~stmt kf in
CallwiseResults.add (kf, Kstmt stmt) r;
r
- else !Db.Operational_inputs.get_external kf
+ else !ref_get_external kf
let extract_inout_from_froms froms =
let open Function_Froms in
@@ -580,7 +584,7 @@ module Callwise = struct
| [] -> Inout_parameters.fatal "callwise: internal stack is empty"
let end_record callstack kf inout =
- Db.Operational_inputs.Record_Inout_Callbacks.apply inout;
+ Eva__Private.Inout.Operational_inputs.Record_Inout_Callbacks.apply inout;
let callsite = Eva.Callstack.top_callsite callstack in
match callsite, !call_inout_stack with
| Kstmt _, (_caller, table) :: _ ->
@@ -765,7 +769,7 @@ module Externals =
let size = 17
end)
let get_external = Externals.memo (raw_externals ~with_formals:false)
-let compute_external kf = ignore (get_external kf)
+let compute kf = ignore (get_external kf)
@@ -795,17 +799,22 @@ let pretty_operational_inputs_external_with_formals fmt kf =
Kernel_function.pretty kf
Inout_type.pretty_operational_inputs (get_external_with_formals kf)
+let pretty fmt x =
+ Format.fprintf fmt "@[<v>";
+ Format.fprintf fmt "@[<v 2>Operational inputs:@ @[<hov>%a@]@]@ "
+ Locations.Zone.pretty (x.Inout_type.over_inputs);
+ Format.fprintf fmt "@[<v 2>Operational inputs on termination:@ @[<hov>%a@]@]@ "
+ Locations.Zone.pretty (x.Inout_type.over_inputs_if_termination);
+ Format.fprintf fmt "@[<v 2>Sure outputs:@ @[<hov>%a@]@]"
+ Locations.Zone.pretty (x.Inout_type.under_outputs_if_termination);
+ Format.fprintf fmt "@]"
+let get_internal_precise = get_internal_aux
-let () =
- Db.Operational_inputs.self_internal := Internals.self;
- Db.Operational_inputs.self_external := Externals.self;
- Db.Operational_inputs.get_internal := get_internal;
- Db.Operational_inputs.get_external := get_external;
- Db.Operational_inputs.get_internal_precise := get_internal_aux;
- Db.Operational_inputs.compute := compute_external;
- Db.Operational_inputs.display := pretty_operational_inputs_internal
+let () =
+ ref_get_internal := get_internal;
+ ref_get_external := get_external
(*
Local Variables:
diff --git a/src/plugins/inout/operational_inputs.mli b/src/plugins/inout/operational_inputs.mli
index 3c54c51db8c231f92cf834b09ab4a4a8805fe23b..2a545e374ea6d2b90328be4d2f8496802a788de4 100644
--- a/src/plugins/inout/operational_inputs.mli
+++ b/src/plugins/inout/operational_inputs.mli
@@ -22,12 +22,18 @@
open Cil_types
+val compute: kernel_function -> unit
+
val get_external: kernel_function -> Inout_type.t
val get_external_aux: ?stmt:stmt -> kernel_function -> Inout_type.t
+val get_internal_precise: ?stmt:stmt -> kernel_function -> Inout_type.t
+
val pretty_operational_inputs_internal:
Format.formatter -> kernel_function -> unit
val pretty_operational_inputs_external:
Format.formatter -> kernel_function -> unit
val pretty_operational_inputs_external_with_formals:
Format.formatter -> kernel_function -> unit
+
+val pretty: Format.formatter -> Inout_type.t -> unit
diff --git a/src/plugins/inout/outputs.ml b/src/plugins/inout/outputs.ml
index 14c8ee4b6bf404a0c0a29ffafcbf4f8681474dd9..1caf9f4d01bb406cae90880983a7a470799f5668 100644
--- a/src/plugins/inout/outputs.ml
+++ b/src/plugins/inout/outputs.ml
@@ -171,15 +171,14 @@ let pretty_external fmt kf =
with Not_found ->
()
+let self = Externals.self
+let compute kf = ignore (get_internal kf)
+let statement = Analysis.statement
+
let () =
- Db.Outputs.self_internal := Analysis.Memo.self;
- Db.Outputs.self_external := Externals.self;
- Db.Outputs.get_internal := get_internal;
- Db.Outputs.get_external := get_external;
- Db.Outputs.compute := (fun kf -> ignore (get_internal kf));
- Db.Outputs.display := pretty_internal;
- Db.Outputs.display_external := pretty_external;
- Db.Outputs.statement := Analysis.statement
+ Eva__Private.Inout.Outputs.ref_statement := Analysis.statement ;
+ Eva__Private.Inout.Outputs.ref_get_external := get_external ;
+ Eva__Private.Inout.Outputs.ref_get_internal := get_internal
(*
Local Variables:
diff --git a/src/plugins/inout/outputs.mli b/src/plugins/inout/outputs.mli
index 4fe03b173c6d15d9adbd66ee340b720e7d7be3ec..006d55cae5cef6654afe40115ab8fda08419ff86 100644
--- a/src/plugins/inout/outputs.mli
+++ b/src/plugins/inout/outputs.mli
@@ -20,5 +20,11 @@
(* *)
(**************************************************************************)
+val self: State.t
+
+val compute: Cil_types.kernel_function -> unit
+val get_external: Cil_types.kernel_function -> Locations.Zone.t
+val statement: Cil_types.stmt -> Locations.Zone.t
+
val pretty_external: Format.formatter -> Cil_types.kernel_function -> unit
val pretty_internal: Format.formatter -> Cil_types.kernel_function -> unit
diff --git a/src/plugins/reduc/collect.ml b/src/plugins/reduc/collect.ml
index ad7b55351d3d22f035aea30f27aeb57c0e30f706..d19635aa3cd8a9245687dc777d1064fe9a88e6b9 100644
--- a/src/plugins/reduc/collect.ml
+++ b/src/plugins/reduc/collect.ml
@@ -122,7 +122,7 @@ class inout_vis
with Kernel_function.No_Statement -> assert false
method !vstmt stmt =
- let out = !Db.Outputs.statement stmt in
+ let out = Inout.Outputs.statement stmt in
let filter_out vi =
let open Locations in
let zone = enumerate_bits (loc_of_varinfo vi) in
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index f992fda8da2b72a2dc2d59a582b7fa832b201391..23c2421b339068bbcd61c7f2c139a106a79477e2 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -87,7 +87,7 @@ let get_writes stmt lval =
let register_modified_zones lmap stmt =
let register lmap zone = InitSid.add_zone lmap zone stmt in
let aux_out out kf =
- let inout= !Db.Operational_inputs.get_internal_precise ~stmt kf in
+ let inout= Inout.Operational_inputs.get_internal_precise ~stmt kf in
Locations.Zone.join out inout.Inout_type.over_outputs
in
match stmt.skind with
diff --git a/src/plugins/slicing/dune b/src/plugins/slicing/dune
index 23df7d7c78f22a6323af17e578fa353b4e35501a..fda67cdea22236078676792d469515d6aad8b479 100644
--- a/src/plugins/slicing/dune
+++ b/src/plugins/slicing/dune
@@ -27,6 +27,7 @@
(echo "Slicing:" %{lib-available:frama-c-slicing.core} "\n")
(echo " - Pdg:" %{lib-available:frama-c-pdg.core} "\n")
(echo " - Sparecode:" %{lib-available:frama-c-sparecode.core} "\n")
+ (echo " - Inout" %{lib-available:frama-c-inout.core} "\n")
)
)
)
@@ -36,7 +37,7 @@
(optional)
(public_name frama-c-slicing.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-pdg.core frama-c-sparecode.core)
+ (libraries frama-c.kernel frama-c-inout.core frama-c-pdg.core frama-c-sparecode.core)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))
)
diff --git a/src/plugins/slicing/fct_slice.ml b/src/plugins/slicing/fct_slice.ml
index 7611cece658420628c00a2e0bdada706d4849587..6d09aef97e71bd9f684dff384cad6c92e0760a36 100644
--- a/src/plugins/slicing/fct_slice.ml
+++ b/src/plugins/slicing/fct_slice.ml
@@ -424,7 +424,7 @@ end = struct
let add_mark =
let kf = fi_to_call.SlicingInternals.fi_kf in
let op_inputs =
- !Db.Operational_inputs.get_internal_precise ~stmt:call kf in
+ Inout.Operational_inputs.get_internal_precise ~stmt:call kf in
let z = op_inputs.Inout_type.over_inputs in
match s with
| PdgMarks.SelNode (_, None) -> true
@@ -1308,7 +1308,7 @@ let apply_change_call ff call f_to_call =
try
let kf = ff_to_call.SlicingInternals.ff_fct.SlicingInternals.fi_kf in
let op_inputs =
- !Db.Operational_inputs.get_internal_precise ~stmt:call kf in
+ Inout.Operational_inputs.get_internal_precise ~stmt:call kf in
let z = op_inputs.Inout_type.over_inputs in
(*Format.printf "##Call at %a,@ kf %a,@ @[Z %a@]@."
Cil.d_loc (Cil_datatype.Stmt.loc call)
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index 38c151c53b064ded45c97d78b906b167b35125f3..637319e1b3db053e3286a93110e3e7fbf7ff7b2a 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -247,7 +247,7 @@ let select_func_calls_to set ~spare kf =
SlicingMarks.mk_user_mark ~data:nspare ~addr:nspare ~ctrl:nspare
in
assert (Eva.Analysis.is_computed ());
- let outputs = !Db.Outputs.get_external kf in
+ let outputs = Inout.Outputs.get_external kf in
select_entry_point_and_some_inputs_outputs set ~mark kf
~return:true
~outputs
@@ -407,8 +407,8 @@ let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
in
assert (Eva.Results.is_called kf) ; (* otherwise [!Db.Outputs.get_external kf] gives weird results *)
- select_inter_zone select_wr zone_wr_opt (!Db.Outputs.get_external kf) ;
- select_inter_zone select_rd zone_rd_opt (!Db.Inputs.get_external kf)
+ select_inter_zone select_wr zone_wr_opt (Inout.Outputs.get_external kf) ;
+ select_inter_zone select_rd zone_rd_opt (Inout.Inputs.get_external kf)
end
));
!ac
diff --git a/src/plugins/slicing/slicingState.ml b/src/plugins/slicing/slicingState.ml
index 082deff81942d5b5e121ea5b286489cf2cb6f097..bd8abdff6869f58d99864aa2080523371fb6ba2c 100644
--- a/src/plugins/slicing/slicingState.ml
+++ b/src/plugins/slicing/slicingState.ml
@@ -34,7 +34,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:self
- [ Pdg.Api.self; !Db.Inputs.self_external; !Db.Outputs.self_external ])
+ [ Pdg.Api.self; Inout.Inputs.self ; Inout.Outputs.self ])
let get () =
try P.get ()
diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index 08f1df99b3bc1c67cdd3d4146c9696e87f3ea0da..dafe82987f4666ef9e8829016410f867de06f21c 100644
--- a/src/plugins/sparecode/globs.ml
+++ b/src/plugins/sparecode/globs.ml
@@ -160,7 +160,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:Result.self
- [ Pdg.Api.self; !Db.Outputs.self_external ])
+ [ Pdg.Api.self; Inout.Outputs.self ])
let rm_unused_decl =
Result.memo
diff --git a/src/plugins/sparecode/register.ml b/src/plugins/sparecode/register.ml
index 0a90bf35987769c1531ad3adc5d98d1d2f9ea59c..8e2d7af9f7e6727d1bff2bf9bdb99a2dd676847e 100644
--- a/src/plugins/sparecode/register.ml
+++ b/src/plugins/sparecode/register.ml
@@ -43,7 +43,7 @@ let () =
(fun () ->
State_dependency_graph.add_codependencies
~onto:Result.self
- [ Pdg.Api.self; !Db.Outputs.self_external ])
+ [ Pdg.Api.self; Inout.Outputs.self ])
module P = Sparecode_params
diff --git a/src/plugins/sparecode/spare_marks.ml b/src/plugins/sparecode/spare_marks.ml
index e41b498caea524d60468b020600a53a06825f329..48d1f2884d9b2896a01efe29993f55a05e9eb48f 100644
--- a/src/plugins/sparecode/spare_marks.ml
+++ b/src/plugins/sparecode/spare_marks.ml
@@ -280,7 +280,7 @@ let select_entry_point proj _kf pdg =
select_pdg_elements proj pdg to_select
let select_all_outputs proj kf pdg =
- let outputs = !Db.Outputs.get_external kf in
+ let outputs = Inout.Outputs.get_external kf in
debug 1 "@[selecting output zones %a@]" Locations.Zone.pretty outputs;
try
let nodes, undef = Pdg.Api.find_location_nodes_at_end pdg outputs in
diff --git a/src/plugins/studia/dune b/src/plugins/studia/dune
index cb4cc468ce98a2b7a1559a7a72c75b9eebbaa98d..daf095129ec7c1fea7828907d703631b3cc8fac5 100644
--- a/src/plugins/studia/dune
+++ b/src/plugins/studia/dune
@@ -26,6 +26,7 @@
(action (progn
(echo "Studia:" %{lib-available:frama-c-studia.core} "\n")
(echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ (echo " - Inout:" %{lib-available:frama-c-inout.core} "\n")
)
)
)
@@ -35,7 +36,7 @@
(optional)
(public_name frama-c-studia.core)
(flags -open Frama_c_kernel :standard)
- (libraries frama-c.kernel frama-c-eva.core)
+ (libraries frama-c.kernel frama-c-eva.core frama-c-inout.core)
(instrumentation (backend landmarks))
(instrumentation (backend bisect_ppx))
)
diff --git a/src/plugins/studia/reads.ml b/src/plugins/studia/reads.ml
index 3bebf797fa3bda62c11cf80191be51eec1a06226..457a6a17da99f7fc84dc79d0d45ade880205669e 100644
--- a/src/plugins/studia/reads.ml
+++ b/src/plugins/studia/reads.ml
@@ -37,11 +37,11 @@ class find_read zlval = object
method! vstmt_aux stmt =
let aux_call lvopt _kf args _loc =
- let z = !Db.Inputs.statement stmt in
+ let z = Inout.Inputs.statement stmt in
if Zone.intersects z zlval then begin
(* Computes what is read to evaluate [args] and [lvopt] *)
let deps =
- List.map (!Db.Inputs.expr stmt) args
+ List.map (Inout.Inputs.expr stmt) args
in
let deps = List.fold_left Zone.join Zone.bottom deps in
let deps = match lvopt with
@@ -54,7 +54,7 @@ class find_read zlval = object
(* now determine if the functions called at [stmt] read directly or
indirectly [zlval] *)
let aux_kf (direct, indirect) kf =
- let inputs = !Db.Inputs.get_internal kf in
+ let inputs = Inout.Inputs.get_internal kf in
(* TODO: change to this once we can get "full" inputs through Inout.
Currently, non operational inputs disappear, and this function
is not suitable.
@@ -85,13 +85,13 @@ class find_read zlval = object
Cil.treat_constructor_as_func aux_call v f args k l;
Cil.SkipChildren
| Instr _ ->
- let z = !Db.Inputs.statement stmt in
+ let z = Inout.Inputs.statement stmt in
if Zone.intersects z zlval then begin
res <- Direct stmt :: res
end;
Cil.SkipChildren
| If (e, _, _, _) | Switch (e, _, _, _) | Return (Some e, _) ->
- let z = !Db.Inputs.expr stmt e in
+ let z = Inout.Inputs.expr stmt e in
if Zone.intersects z zlval then begin
res <- Direct stmt :: res
end;
@@ -104,7 +104,7 @@ end
let compute z =
let vis = new find_read z in
let aux_kf_fundec kf =
- let all_in = !Db.Inputs.get_internal kf in
+ let all_in = Inout.Inputs.get_internal kf in
if Zone.intersects all_in z then begin
let fundec = Kernel_function.get_definition kf in
ignore
diff --git a/src/plugins/studia/writes.ml b/src/plugins/studia/writes.ml
index d5a2f6b0584af1ebbf9e74565b1580c54437dfe6..65a670198c4f290a7c78230672a3030deafd52de 100644
--- a/src/plugins/studia/writes.ml
+++ b/src/plugins/studia/writes.ml
@@ -65,7 +65,7 @@ let compare w1 w2 =
(** Does the functions called at [stmt] modify directly or indirectly [zlval] *)
let effects_of_call stmt zlval effects =
let aux_kf (direct, indirect) kf =
- let inout = !Db.Operational_inputs.get_internal_precise ~stmt kf in
+ let inout = Inout.Operational_inputs.get_internal_precise ~stmt kf in
let out = inout.Inout_type.over_outputs in
if Zone.intersects out zlval then
if Eva.Analysis.use_spec_instead_of_definition kf then
@@ -89,7 +89,7 @@ class find_write_insts zlval = object (self)
let aux_call lvopt _kf _args _loc =
(* Direct effect through the writing of [lvopt], or indirect inside
the call. *)
- let z = !Db.Outputs.statement stmt in
+ let z = Inout.Outputs.statement stmt in
if Zone.intersects z zlval then
let direct = match lvopt with
| None -> false
@@ -106,7 +106,7 @@ class find_write_insts zlval = object (self)
match i with
| Set _ | Local_init(_, AssignInit _, _) ->
(* Effect only throuh the written l-value *)
- let z = !Db.Outputs.statement stmt in
+ let z = Inout.Outputs.statement stmt in
if Zone.intersects z zlval then begin
res <- Assign stmt :: res
end
@@ -123,7 +123,7 @@ end
let inst_writes z =
let vis = new find_write_insts z in
let aux_kf_fundec kf =
- let all_out = !Db.Operational_inputs.get_internal_precise kf in
+ let all_out = Inout.Operational_inputs.get_internal_precise kf in
let zout = all_out.Inout_type.over_outputs in
if Zone.intersects zout z then begin
let fundec = Kernel_function.get_definition kf in
diff --git a/tests/slicing/simple_intra_slice.ml b/tests/slicing/simple_intra_slice.ml
index 7a7e189a1c90ae91ae2a9165430481ed0d3d05d7..a5df5c95d1f7fd6d0e63cfad5922857b62fc0e50 100644
--- a/tests/slicing/simple_intra_slice.ml
+++ b/tests/slicing/simple_intra_slice.ml
@@ -47,7 +47,7 @@ let main _ =
in
let print_outputs fct_name =
let fct = Globals.Functions.find_by_name fct_name in
- let outs = !Db.Outputs.get_external fct in
+ let outs = Inout.Outputs.get_external fct in
Format.printf "Sorties de la fonction %s = %a\n"
fct_name Locations.Zone.pretty outs
in