Wp.RegionAnnottype 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 ... endtype region_spec = {region_name : string option; |
region_pattern : region_pattern; |
region_lpath : lpath list; |
}val p_name : region_pattern -> stringval of_extension : Frama_c_kernel.Cil_types.acsl_extension -> region_spec listval of_behavior : Frama_c_kernel.Cil_types.behavior -> region_spec list