package frama-c

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

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

module RW : sig ... end

Read-Write access

module Flat : sig ... end

Flatten arrays

module Pack : sig ... end

Pack fields

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