sig
type param =
NotUsed
| ByAddr
| ByValue
| ByShift
| ByRef
| InContext
| InArray
val pp_param : 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
type zone =
Var of Cil_types.varinfo
| Ptr of Cil_types.varinfo
| Arr of Cil_types.varinfo
type clause =
Valid of Wp.MemoryContext.zone
| Separated of Wp.MemoryContext.zone list list
val requires : Wp.MemoryContext.partition -> Wp.MemoryContext.clause list
val pp_zone : Format.formatter -> Wp.MemoryContext.zone -> unit
val pp_clause : Format.formatter -> Wp.MemoryContext.clause -> unit
end