Module Operational_inputs

module Operational_inputs: sig .. end

type t = Inout_type.t = {
   over_inputs : Locations.Zone.t;
   over_inputs_if_termination : Locations.Zone.t;
   under_outputs_if_termination : Locations.Zone.t;
   over_outputs : Locations.Zone.t;
   over_outputs_if_termination : Locations.Zone.t;
}
val top : t
type compute_t = {
   over_inputs_d : Locations.Zone.t;
   under_outputs_d : Locations.Zone.t;
   over_outputs_d : Locations.Zone.t;
}
val empty : compute_t
val bottom : compute_t
val equal : compute_t -> compute_t -> bool
val join : compute_t ->
compute_t -> compute_t
val is_included : compute_t -> compute_t -> bool
val join_and_is_included : compute_t ->
compute_t -> compute_t * bool
val externalize_zone : with_formals:bool ->
Kernel_function.t -> Locations.Zone.t -> Locations.Zone.t
val eval_assigns : Kernel_function.t ->
Db.Value.state -> Cil_types.assigns -> t
val compute_using_prototype_state : Db.Value.state -> Kernel_function.t -> t
val compute_using_given_spec_state : Db.Value.state -> Cil_types.spec -> Kernel_function.t -> t
val compute_using_prototype : ?stmt:Cil_types.stmt -> Kernel_function.t -> t
module Internals: Kernel_function.Make_Table(Inout_type)(sig
val name : string
val dependencies : State.t list
val size : int
end)
module CallsiteHash: Value_types.Callsite.Hashtbl
module CallwiseResults: State_builder.Hashtbl(Value_types.Callsite.Hashtbl)(Inout_type)(sig
val size : int
val dependencies : State.t list
val name : string
end)
module Computer: 
functor (Fenv : Dataflows.FUNCTION_ENV-> 
functor (X : sig
val _version : string
val _kf : Cil_types.kernel_function
val stmt_state : Cil_types.stmt -> Db.Value.state
val at_call : Cil_types.stmt -> Cil_types.kernel_function -> Inout_type.t
end-> sig .. end
val externalize : with_formals:bool -> Kernel_function.t -> Inout_type.t -> Inout_type.t
val compute_externals_using_prototype : ?stmt:Cil_types.stmt -> Kernel_function.t -> Inout_type.t
val get_internal_aux : ?stmt:Cil_types.stmt -> Kernel_function.t -> Db.Operational_inputs.t
val get_external_aux : ?stmt:Cil_types.stmt -> Kernel_function.t -> Db.Operational_inputs.t
val extract_inout_from_froms : Function_Froms.froms -> Locations.Zone.t * Locations.Zone.t
module Callwise: sig .. end
module FunctionWise: sig .. end
val get_internal : Internals.key -> Internals.data
val raw_externals : with_formals:bool -> Kernel_function.t -> Inout_type.t
module Externals: Kernel_function.Make_Table(Inout_type)(sig
val name : string
val dependencies : State.t list
val size : int
end)
val get_external : Externals.key -> Externals.data
val compute_external : Externals.key -> unit
module Externals_With_Formals: Kernel_function.Make_Table(Inout_type)(sig
val name : string
val dependencies : State.t list
val size : int
end)
val get_external_with_formals : Externals_With_Formals.key ->
Externals_With_Formals.data
val compute_external_with_formals : Externals_With_Formals.key -> unit
val pretty_operational_inputs_internal : Format.formatter -> Kernel_function.t -> unit
val pretty_operational_inputs_external : Format.formatter -> Kernel_function.t -> unit
val pretty_operational_inputs_external_with_formals : Format.formatter -> Kernel_function.t -> unit