module Callwise: sig
.. end
val compute_callwise : unit -> bool
val merge_call_in_local_table : CallsiteHash.key -> Inout_type.t CallsiteHash.t -> Inout_type.t -> unit
val merge_call_in_global_tables : Operational_inputs.Internals.key * Cil_types.kinstr -> Inout_type.t -> unit
val merge_local_table_in_global_ones : Inout_type.t CallsiteHash.t -> unit
val call_inout_stack : (Kernel_function.t * Inout_type.t 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.t -> unit
val compute_call_from_value_states : Cil_types.kernel_function ->
Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t -> Operational_inputs.t
val record_for_callwise_inout : Db.Value.callstack *
(Cvalue.Model.t Cil_datatype.Stmt.Hashtbl.t Lazy.t * 'a)
Value_types.callback_result -> unit
val add_hooks : unit -> unit