Module MemoryContext

module MemoryContext: sig .. end

type param = 
| NotUsed
| ByAddr
| ByValue
| ByShift
| ByRef
| InContext
| InArray
val pp_param : Stdlib.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 : Stdlib.Format.formatter -> zone -> unit
val pp_clause : Stdlib.Format.formatter -> clause -> unit