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 : 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