Module Library_functions

module Library_functions: sig .. end

Associates 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)

Associates 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

Auxiliary function that registers a new variable declared by Value within the kernel internal tables

val returned_value : Kernel_function.t -> Cvalue.Model.t -> Cvalue.V.t * Cvalue.Model.t