module Callwise: sig
.. end
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 : (Operational_inputs.Internals.key * Inout_type.t CallsiteHash.t) list
Stdlib.ref
val call_for_callwise_inout : [< `Builtin of (Function_Froms.froms * Locations.Zone.t) option
| `Def
| `Memexec
| `Spec of Cil_types.spec ] *
Db.Value.state * (Operational_inputs.Internals.key * 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 : (Operational_inputs.Internals.key * Cil_types.kinstr) list ->
Inout_type.t -> unit
val compute_call_from_value_states : Cil_types.kernel_function ->
Value_types.Callstack.Hashtbl.key ->
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 Stdlib.Lazy.t * 'a)
Value_types.callback_result -> unit