Module Library_functions

module Library_functions: sig .. end
Associates kernel_function to a fresh base for the address returned by the kernel_function.

val add_retres_to_state : Cil_types.kernel_function ->
Cvalue.V_Offsetmap.t -> Cvalue.Model.t -> Cil_types.varinfo * Cvalue.Model.t
val returned_value : Cil_types.kernel_function -> Cvalue.Model.t -> Cvalue.V.t * Cvalue.Model.t