package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct