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

Generalized l-values

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