Frama-C API - RegionAnnot
type lrange =
| R_index of Frama_c_kernel.Cil_types.term
| R_range of Frama_c_kernel.Cil_types.term option * Frama_c_kernel.Cil_types.term option
type lpath = {
loc : Frama_c_kernel.Cil_types.location;
lnode : lnode;
ltype : Frama_c_kernel.Cil_types.typ;
}
and lnode =
| L_var of Frama_c_kernel.Cil_types.varinfo
| L_region of string
| L_addr of lpath
| L_star of Frama_c_kernel.Cil_types.typ * lpath
| L_shift of lpath * Frama_c_kernel.Cil_types.typ * lrange
| L_index of lpath * Frama_c_kernel.Cil_types.typ * lrange
| L_field of lpath * Frama_c_kernel.Cil_types.fieldinfo list
| L_cast of Frama_c_kernel.Cil_types.typ * lpath
module Lpath : sig ... end
type region_spec = {
region_name : string option;
region_pattern : region_pattern;
region_lpath : lpath list;
}
val p_name : region_pattern -> string
val of_extension : Frama_c_kernel.Cil_types.acsl_extension -> region_spec list
val of_behavior : Frama_c_kernel.Cil_types.behavior -> region_spec list