module Callwise: sig
.. end
val compute_callwise : unit -> bool
val merge_call_in_local_table : Operational_inputs.CallsiteHash.key ->
Inout_type.tt Operational_inputs.CallsiteHash.t -> Inout_type.tt -> unit
val merge_call_in_global_tables : Operational_inputs.Internals.key * Cil_types.kinstr -> Inout_type.tt -> unit
val merge_local_table_in_global_ones : Inout_type.t Operational_inputs.CallsiteHash.t -> unit
val call_inout_stack : (Kernel_function.t * Inout_type.t Operational_inputs.CallsiteHash.t) list
Pervasives.ref
val call_for_callwise_inout : Db.Value.state * (Kernel_function.t * Cil_types.kinstr) list -> unit
module MemExec: State_builder.Hashtbl
(
Datatype.Int.Hashtbl
)
(
Inout_type
)
(
sig
val size : int
val dependencies : State.t list
val name : string
end
)
val end_record : (Kernel_function.t * Cil_types.kinstr) list -> Inout_type.tt -> unit
val compute_call_from_value_states : Cil_types.kernel_function ->
Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t -> Operational_inputs.tt
val record_for_callwise_inout : Db.Value.callstack *
Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t Lazy.t Value_types.callback_result ->
unit
val add_hooks : unit -> unit