package frama-c

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

Generic Engine Signature

type op =
  1. | Op of string
    (*

    Infix or prefix operator

    *)
  2. | Assoc of string
    (*

    Left-associative binary operator (like + and -)

    *)
  3. | Call of string
    (*

    Logic function or predicate

    *)
type callstyle =
  1. | CallVar
    (*

    Call is f(x,...) ; f() can be written f

    *)
  2. | CallVoid
    (*

    Call is f(x,...) ; in f(), () is mandatory

    *)
  3. | CallApply
    (*

    Call is f x ...

    *)
type mode =
  1. | Mpositive
    (*

    Current scope is Prop in positive position.

    *)
  2. | Mnegative
    (*

    Current scope is Prop in negative position.

    *)
  3. | Mterm
    (*

    Current scope is Term.

    *)
  4. | Mterm_int
    (*

    Int is required but actual scope is Term.

    *)
  5. | Mterm_real
    (*

    Real is required but actual scope is Term.

    *)
  6. | Mint
    (*

    Current scope is Int.

    *)
  7. | Mreal
    (*

    Current scope is Real.

    *)
type flow =
  1. | Flow
  2. | Atom
type cmode =
  1. | Cprop
  2. | Cterm
type amode =
  1. | Aint
  2. | Areal
type pmode =
  1. | Positive
  2. | Negative
  3. | Boolean
type ('x, 'f) ftrigger =
  1. | TgAny
  2. | TgVar of 'x
  3. | TgGet of ('x, 'f) ftrigger * ('x, 'f) ftrigger
  4. | TgSet of ('x, 'f) ftrigger * ('x, 'f) ftrigger * ('x, 'f) ftrigger
  5. | TgFun of 'f * ('x, 'f) ftrigger list
  6. | TgProp of 'f * ('x, 'f) ftrigger list
type ('t, 'f, 'c) ftypedef =
  1. | Tabs
  2. | Tdef of 't
  3. | Trec of ('f * 't) list
  4. | Tsum of ('c * 't list) list
type scope = [
  1. | `Auto
  2. | `Unfolded
  3. | `Defined of string
]
module type Env = sig ... end

Generic Engine Signature

class type virtual ['z, 'adt, 'field, 'logic, 'tau, 'var, 'term, 'env] engine = object ... end
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