Module Layout

module Layout: sig .. end
Region Utilities

module type Data = sig .. end

L-Path


type offset = 
| Field of Cil_types.fieldinfo
| Index of Cil_types.typ * int
type lvalue = 
| Eval of Cil_types.exp
| Tval of Cil_types.term
| Assigned of Cil_types.stmt
module Offset: sig .. end
module Lvalue: Data  with type t = lvalue

Access


type alias = 
| NotUsed
| NotAliased
| Aliased
type usage = 
| Value
| Deref
| Array
type deref = usage * Cil_types.typ 
module Alias: sig .. end
module Usage: sig .. end
module Deref: Data  with type t = deref

R-Values


type 'a value = 
| Int of Ctypes.c_int
| Float of Ctypes.c_float
| Pointer of 'a
module Value: sig .. end
module Matrix: sig .. end

Overlays


type dim = 
| Raw of int
| Dim of int * int list
type 'a range = private {
   ofs : int;
   len : int;
   reg : 'a;
   dim : dim;
}
type 'a overlay = 'a range list 
type 'a merger = raw:bool -> 'a -> 'a -> 'a 
module Range: sig .. end
module Overlay: sig .. end

Compound Layout


type 'a layout = {
   sizeof : int;
   layout : 'a overlay;
}
module Compound: sig .. end

Clustering


type 'a cluster = 
| Empty
| Garbled
| Chunk of 'a value
| Layout of 'a layout
module Cluster: sig .. end

Roots


type 'a from = 
| Fvar of Cil_types.varinfo
| Ffield of 'a * int
| Findex of 'a
| Fderef of 'a
| Farray of 'a
type root = 
| Rnone
| Rfield of Cil_types.varinfo * int
| Rindex of Cil_types.varinfo
| Rtop
module Root: sig .. end

Chunks


type chunks = Qed.Intset.t 
type 'a chunk = 
| Mref of 'a (*
Constant pointers to region
*)
| Mmem of root * 'a value (*
Aliased values
*)
| Mraw of root * 'a option (*
Bits that may points-to
*)
| Mcomp of chunks * 'a overlay (*
Aliased chunks & overlay
*)
module Chunk: sig .. end

Options


module RW: sig .. end
Read-Write access
module Flat: sig .. end
Flatten arrays
module Pack: sig .. end
Pack fields