Module RegionAnnot

module RegionAnnot: sig .. end
Auto when `-wp-region`

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 : lnode;
   ltype : Cil_types.typ;
}
type lnode = 
| L_var of Cil_types.varinfo
| L_region of string
| L_addr of lpath
| L_star of Cil_types.typ * lpath
| L_shift of lpath * Cil_types.typ * lrange
| L_index of lpath * Cil_types.typ * lrange
| L_field of lpath * Cil_types.fieldinfo list
| L_cast of Cil_types.typ * lpath
module Lpath: sig .. end
type region_pattern = 
| FREE
| PVAR
| PREF
| PMEM
| PVECTOR
| PMATRIX
type region_spec = {
   region_name : string option;
   region_pattern : region_pattern;
   region_lpath : lpath list;
}
val p_name : region_pattern -> string
val of_extension : Cil_types.acsl_extension -> region_spec list
val of_behavior : Cil_types.behavior -> region_spec list
val register : unit -> unit
Auto when `-wp-region`