Module Operational_inputs

module Operational_inputs: sig .. end

type tt = Inout_type.tt = {
   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 : tt
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 catenate : compute_t ->
compute_t -> compute_t
val externalize_zone : with_formals:bool ->
Cil_types.kernel_function -> Locations.Zone.t -> Locations.Zone.t
val eval_assigns : Kernel_function.t ->
Db.Value.state ->
Cil_types.identified_term Cil_types.assigns -> tt
val compute_using_prototype_state : Db.Value.state -> Kernel_function.t -> tt
val compute_using_prototype : ?stmt:Cil_types.stmt -> Kernel_function.t -> tt
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(CallsiteHash)(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 ->
Cil_types.kernel_function -> 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
module Callwise: sig .. end
module FunctionWise: sig .. end
val get_internal : Internals.key -> Internals.data
val raw_externals : with_formals:bool -> Internals.key -> 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 : Kernel_function.t -> Externals.data
val compute_external : Kernel_function.t -> 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