Module MemoryContext

module MemoryContext: sig .. end
&x the cell x

type param = 
| NotUsed
| ByAddr
| ByValue
| ByShift
| ByRef
| InContext
| InArray
val pp_param : Format.formatter -> param -> unit
type partition 
val empty : partition
val set : Cil_types.varinfo ->
param -> partition -> partition
type zone = 
| Var of Cil_types.varinfo (*
&x the cell x
*)
| Ptr of Cil_types.varinfo (*
p the cell pointed by p
*)
| Arr of Cil_types.varinfo (*
p+(..) the cell and its neighbors pointed by p
*)
type clause = 
| Valid of zone
| Separated of zone list list
val requires : partition -> clause list
Build the separation clause from a partition, including the clauses related to the pointer validity
val pp_zone : Format.formatter -> zone -> unit
val pp_clause : Format.formatter -> clause -> unit