sig
type validity = Valid | Nullable
type param =
NotUsed
| ByAddr
| ByValue
| ByShift
| ByRef
| InContext of Wp.MemoryContext.validity
| InArray of Wp.MemoryContext.validity
val pp_param : Stdlib.Format.formatter -> Wp.MemoryContext.param -> unit
type partition
val empty : Wp.MemoryContext.partition
val set :
Cil_types.varinfo ->
Wp.MemoryContext.param ->
Wp.MemoryContext.partition -> Wp.MemoryContext.partition
val compute :
string ->
(Cil_types.kernel_function -> Wp.MemoryContext.partition) -> unit
val add_behavior :
Cil_types.kernel_function ->
string ->
(Cil_types.kernel_function -> Wp.MemoryContext.partition) -> unit
val warn :
Cil_types.kernel_function ->
string ->
(Cil_types.kernel_function -> Wp.MemoryContext.partition) -> unit
end