functor (Values_To_Use : Values_To_Use_Sig) ->
functor (Froms_To_Use : Froms_To_Use_Sig) ->
functor (Recording_To_Do : Recording_Sig) ->
sig
type t' = {
additional_deps_table : From_compute.ZoneStmtMap.t;
additional_deps : Locations.Zone.t;
deps_table : Function_Froms.Memory.t;
}
val call_stack : Kernel_function.t Stack.t
val rebuild_additional_deps :
From_compute.ZoneStmtMap.t -> Locations.Zone.t
val merge_deps :
(Locations.Zone.t -> Function_Froms.Deps.t) ->
Function_Froms.Deps.from_deps -> Function_Froms.Deps.from_deps
val find :
Cil_types.stmt ->
Function_Froms.Memory.t ->
Cil_types.exp -> Function_Froms.Deps.from_deps
val empty_from : From_compute.Make.t'
val bottom_from : From_compute.Make.t'
module Computer :
sig
type t = From_compute.Make.t'
val bottom : From_compute.Make.t'
val callwise_states_with_formals :
(Kernel_function.t * Function_Froms.Memory.t) list
Cil_datatype.Stmt.Hashtbl.t
type substit = Froms of Function_Froms.Deps.t
val cached_substitute :
Function_Froms.Memory.t ->
Locations.Zone.t ->
Function_Froms.Deps.from_deps -> Function_Froms.Deps.from_deps
val display_one_from :
Format.formatter -> From_compute.Make.t' -> unit
val pretty :
Format.formatter -> From_compute.Make.Computer.t -> unit
val transfer_conditional_exp :
From_compute.ZoneStmtMap.key ->
Cil_types.exp -> From_compute.Make.t' -> From_compute.Make.t'
val join_and_is_included :
From_compute.Make.t' ->
From_compute.Make.t' -> From_compute.Make.t' * bool
val join :
From_compute.Make.t' ->
From_compute.Make.t' -> From_compute.Make.t'
val resolv_func_vinfo :
?deps:Locations.Zone.t ->
Cil_types.stmt ->
Cil_types.exp -> Locations.Zone.t * Kernel_function.Hptset.t
val transfer_instr :
Cil_datatype.Stmt.Hashtbl.key ->
Cil_types.instr ->
From_compute.Make.Computer.t -> From_compute.Make.Computer.t
val transfer_guard :
Cil_types.stmt ->
Cil_types.exp ->
From_compute.Make.t' ->
From_compute.Make.t' * From_compute.Make.t'
val eliminate_additional :
Cil_types.stmt -> From_compute.Make.t' -> From_compute.Make.t'
val transfer_stmt :
Cil_datatype.Stmt.Hashtbl.key -> t -> (Cil_types.stmt * t) list
val transfer_stmt :
Cil_datatype.Stmt.Hashtbl.key -> t -> (Cil_types.stmt * t) list
val doEdge :
Cil_types.stmt ->
Cil_types.stmt -> From_compute.Make.t' -> From_compute.Make.t'
val transfer_stmt :
Cil_datatype.Stmt.Hashtbl.key ->
From_compute.Make.Computer.t ->
(Cil_types.stmt * From_compute.Make.Computer.t) list
end
val externalize :
Cil_types.stmt ->
Cil_types.kernel_function ->
From_compute.Make.t' -> Function_Froms.froms
val compute_using_cfg : Kernel_function.t -> Function_Froms.froms
val compute_using_prototype :
Kernel_function.t -> Function_Froms.froms
val compute_and_return : Kernel_function.t -> Function_Froms.t
val compute : Kernel_function.t -> unit
end