Previous  Up  Next

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