module MemoryContext: sig
.. end
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 =
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