sig
type region =
Var of Cil_types.varinfo
| Ptr of Cil_types.varinfo
| Arr of Cil_types.varinfo
val pp_region : Format.formatter -> Wp.Separation.region -> unit
type clause = {
mutex : Wp.Separation.region list;
other : Wp.Separation.region list;
}
val is_true : Wp.Separation.clause -> bool
val requires : Wp.Separation.clause list -> Wp.Separation.clause list
val pp_clause : Format.formatter -> Wp.Separation.clause -> unit
end