Module Wp.Layout

Region Utilities

module type Data = sig ... end

L-Path

type offset =
  1. | Field of Frama_c_kernel.Cil_types.fieldinfo
  2. | Index of Frama_c_kernel.Cil_types.typ * int

Generalized l-values

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

Access

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

R-Values

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

Overlays

type dim =
  1. | Raw of int
  2. | Dim of int * int list
type 'a range = private {
  1. ofs : int;
  2. len : int;
  3. reg : 'a;
  4. 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 = {
  1. sizeof : int;
  2. layout : 'a overlay;
}
module Compound : sig ... end

Clustering

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

Roots

type '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
type root =
  1. | Rnone
  2. | Rfield of Frama_c_kernel.Cil_types.varinfo * int
  3. | Rindex of Frama_c_kernel.Cil_types.varinfo
  4. | Rtop
module Root : sig ... end

Chunks

type chunks = Qed.Intset.t
type '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

    *)
module Chunk : sig ... end

Options