Module Wp.Layout

Region Utilities

module type Data = sig ... end

L-Path

type offset =
| Field of Frama_c_kernel.Cil_types.fieldinfo
| 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 =
| NotUsed
| NotAliased
| Aliased
type usage =
| Value
| Deref
| Array
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 Frama_c_kernel.Cil_types.varinfo
| Ffield of 'a * int
| Findex of 'a
| Fderef of 'a
| Farray of 'a
type root =
| Rnone
| Rfield of Frama_c_kernel.Cil_types.varinfo * int
| Rindex of Frama_c_kernel.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