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 |
(* |
| *) |
| |
Ptr of |
(* |
| *) |
| |
Arr of |
(* |
| *) |
type
clause =
| |
Valid of |
| |
Separated of |
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