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