sig
  type lrange =
      R_index of Cil_types.term
    | R_range of Cil_types.term option * Cil_types.term option
  type lpath = {
    loc : Cil_types.location;
    lnode : RegionAnnot.lnode;
    ltype : Cil_types.typ;
  }
  and lnode =
      L_var of Cil_types.varinfo
    | L_region of string
    | L_addr of RegionAnnot.lpath
    | L_star of Cil_types.typ * RegionAnnot.lpath
    | L_shift of RegionAnnot.lpath * Cil_types.typ * RegionAnnot.lrange
    | L_index of RegionAnnot.lpath * Cil_types.typ * RegionAnnot.lrange
    | L_field of RegionAnnot.lpath * Cil_types.fieldinfo list
    | L_cast of Cil_types.typ * RegionAnnot.lpath
  module Lpath :
    sig
      type t = RegionAnnot.lpath
      val equal : RegionAnnot.Lpath.t -> RegionAnnot.Lpath.t -> bool
      val compare : RegionAnnot.Lpath.t -> RegionAnnot.Lpath.t -> int
      val pretty : Stdlib.Format.formatter -> RegionAnnot.Lpath.t -> unit
    end
  type region_pattern = FREE | PVAR | PREF | PMEM | PVECTOR | PMATRIX
  type region_spec = {
    region_name : string option;
    region_pattern : RegionAnnot.region_pattern;
    region_lpath : RegionAnnot.lpath list;
  }
  val p_name : RegionAnnot.region_pattern -> string
  val of_extension : Cil_types.acsl_extension -> RegionAnnot.region_spec list
  val of_behavior : Cil_types.behavior -> RegionAnnot.region_spec list
  val register : unit -> unit
end