module RegionAnnot:sig
..end
type
lrange =
| |
R_index of |
| |
R_range of |
type
lpath = {
|
loc : |
|
lnode : |
|
ltype : |
type
lnode =
| |
L_var of |
| |
L_region of |
| |
L_addr of |
| |
L_star of |
| |
L_shift of |
| |
L_index of |
| |
L_field of |
| |
L_cast of |
module Lpath:sig
..end
type
region_pattern =
| |
FREE |
| |
PVAR |
| |
PREF |
| |
PMEM |
| |
PVECTOR |
| |
PMATRIX |
type
region_spec = {
|
region_name : |
|
region_pattern : |
|
region_lpath : |
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`