module Library_functions:sig
..end
kernel_function
to a fresh base for the address returned by
the kernel_function
.
Auxiliary function that registers a new variable declared by Value
within the kernel internal tables
module Retres:Kernel_function.Make_Table
(
Cil_datatype.Varinfo
)
(
sig
val name :string
val size :int
val dependencies :State.t list
end
)
val get : Retres.key -> Retres.data
val add_retres_to_state : with_alarms:CilE.warn_mode ->
Retres.key ->
Cvalue.Model.offsetmap ->
Cvalue.Model.t -> Retres.data * Cvalue.Model.t
module Returned_Val:Kernel_function.Make_Table
(
Base
)
(
sig
val dependencies :State.t list
val size :int
val name :string
end
)
kernel_function
to a fresh base for the address returned by
the kernel_function
.
val register_new_var : Cil_types.varinfo -> Cil_types.typ -> unit
val returned_value : Kernel_function.t -> Cvalue.Model.t -> Cvalue.V.t * Cvalue.Model.t