Region
Interface for the Region plug-in.
Each function is assigned a region map. Areas in the map represents l-values or, more generally, class of nodes. Regions are classes equivalences of nodes that represents a collection of addresses (at some program point).
Regions can be subdivided into sub-regions. Hence, given two regions, either one is included into the other, or they are separated. Hence, given two l-values, if their associated regions are separated, then they can not be aliased.
Nodes are elementary elements of a region map. Variables maps to nodes, and one can move to one node to another by struct or union field or array element. Two disting nodes might belong to the same region. However, it is possible to normalize nodes and obtain a unique identifier for all nodes in a region.
val get_map : Frama_c_kernel.Cil_types.kernel_function -> map
val cvar : map -> Frama_c_kernel.Cil_types.varinfo -> node
val field : map -> node -> Frama_c_kernel.Cil_types.fieldinfo -> node
val index : map -> node -> Frama_c_kernel.Cil_types.typ -> node
val lval : map -> Frama_c_kernel.Cil_types.lval -> node
val exp : map -> Frama_c_kernel.Cil_types.exp -> node option
val roots : map -> node -> Frama_c_kernel.Cil_types.varinfo list
val reads : map -> node -> Frama_c_kernel.Cil_types.typ list
val writes : map -> node -> Frama_c_kernel.Cil_types.typ list
val shifts : map -> node -> Frama_c_kernel.Cil_types.typ list