Module Wp.LayoutSource

Region Utilities

Sourcemodule type Data = sig ... end

L-Path

Generalized l-values

Sourcemodule Offset : sig ... end
Sourcemodule Lvalue : Data with type t = lvalue

Access

Sourcetype alias =
  1. | NotUsed
  2. | NotAliased
  3. | Aliased
Sourcetype usage =
  1. | Value
  2. | Deref
  3. | Array
Sourcemodule Alias : sig ... end
Sourcemodule Usage : sig ... end
Sourcemodule Deref : Data with type t = deref

R-Values

Sourcetype 'a value =
  1. | Int of Ctypes.c_int
  2. | Float of Ctypes.c_float
  3. | Pointer of 'a
Sourcemodule Value : sig ... end
Sourcemodule Matrix : sig ... end

Overlays

Sourcetype dim =
  1. | Raw of int
  2. | Dim of int * int list
Sourcetype 'a range = private {
  1. ofs : int;
  2. len : int;
  3. reg : 'a;
  4. dim : dim;
}
Sourcetype 'a overlay = 'a range list
Sourcetype 'a merger = raw:bool -> 'a -> 'a -> 'a
Sourcemodule Range : sig ... end
Sourcemodule Overlay : sig ... end

Compound Layout

Sourcetype 'a layout = {
  1. sizeof : int;
  2. layout : 'a overlay;
}
Sourcemodule Compound : sig ... end

Clustering

Sourcetype 'a cluster =
  1. | Empty
  2. | Garbled
  3. | Chunk of 'a value
  4. | Layout of 'a layout
Sourcemodule Cluster : sig ... end

Roots

Sourcetype 'a from =
  1. | Fvar of Frama_c_kernel.Cil_types.varinfo
  2. | Ffield of 'a * int
  3. | Findex of 'a
  4. | Fderef of 'a
  5. | Farray of 'a
Sourcetype root =
  1. | Rnone
  2. | Rfield of Frama_c_kernel.Cil_types.varinfo * int
  3. | Rindex of Frama_c_kernel.Cil_types.varinfo
  4. | Rtop
Sourcemodule Root : sig ... end

Chunks

Sourcetype chunks = Qed.Intset.t
Sourcetype 'a chunk =
  1. | Mref of 'a
    (*

    Constant pointers to region

    *)
  2. | Mmem of root * 'a value
    (*

    Aliased values

    *)
  3. | Mraw of root * 'a option
    (*

    Bits that may points-to

    *)
  4. | Mcomp of chunks * 'a overlay
    (*

    Aliased chunks & overlay

    *)
Sourcemodule Chunk : sig ... end

Options

Sourcemodule RW : sig ... end

Read-Write access

Sourcemodule Flat : sig ... end

Flatten arrays

Sourcemodule Pack : sig ... end

Pack fields