Module Operational_inputs.Callwise

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 : (Operational_inputs.Internals.key * Inout_type.t CallsiteHash.t) list
Pervasives.ref
val call_for_callwise_inout : [< `Builtin of Value_types.call_result
| `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 ->
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