module Operational_inputs: sig
.. end
type
t = Inout_type.t
= {
}
val top : t
type
compute_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:
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
: 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 : Stdlib.Format.formatter -> Kernel_function.t -> unit
val pretty_operational_inputs_external : Stdlib.Format.formatter -> Kernel_function.t -> unit
val pretty_operational_inputs_external_with_formals : Stdlib.Format.formatter -> Kernel_function.t -> unit