Wp.Regionmodule R : Layout.Data with type t = regionmodule Map : Qed.Idxmap.S with type key = regionmodule Set : Qed.Idxset.S with type elt = regionval create : unit -> mapval is_empty : map -> boolval id : region -> intval add_offset : map -> region -> Layout.offset -> regionval field_offset : map -> Frama_c_kernel.Cil_types.fieldinfo -> int * intval get_froms : map -> region -> region Layout.from listval get_roots : map -> region -> Layout.rootval is_garbled : region -> boolval has_pointed : region -> boolval has_layout : region -> boolval has_offset : region -> Layout.offset -> boolval has_copies : region -> boolval has_deref : region -> boolval has_names : region -> boolval has_return : map -> boolval get_offset : map -> region -> Layout.offset -> region optionval acs_read : region -> Layout.lvalue -> unitval acs_write : region -> Layout.lvalue -> unitval acs_shift : region -> Layout.lvalue -> unitval acs_deref : region -> Layout.deref -> unitval is_read : region -> boolval is_written : region -> boolval is_shifted : region -> boolval is_aliased : region -> boolval iter_read : ( Layout.lvalue -> unit ) -> region -> unitval iter_write : ( Layout.lvalue -> unit ) -> region -> unitval iter_shift : ( Layout.lvalue -> unit ) -> region -> unitval iter_deref : ( Layout.deref -> unit ) -> region -> unitval iter_offset : map -> ( Layout.offset -> region -> unit ) -> region -> unitval iter_vars :
map ->
( Frama_c_kernel.Cil_types.varinfo -> region -> unit ) ->
unitval of_cvar : map -> Frama_c_kernel.Cil_types.varinfo -> regionval cluster : map -> region -> region Layout.clusterval chunk : map -> region -> region Layout.chunkval chunks : map -> region -> Layout.chunksval fusion : map -> unitval fusionned : map -> boolval fixpoint : map -> unit