package frama-c

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

Functors for generic lattices implementations.

exception Error_Top

Raised by some functions when encountering a top value.

exception Error_Bottom

Raised by Lattice_Base.project.

exception Not_less_than

Raised by Lattice.cardinal_less_than.

exception Can_not_subdiv

Used by other modules e.g. Fval.subdiv_float_interval.

type truth =
  1. | True
  2. | False
  3. | Unknown
    (*

    Truth values with a possibility for 'Unknown'

    *)
val inv_truth : truth -> truth
module Comp : sig ... end

Signatures for comparison operators ==, !=, <, >, <=, >=.

module Int : sig ... end
module Rel : sig ... end

"Relative" integers. They are subtraction between two absolute integers

module Bool : sig ... end

See e.g. base.ml and locations.ml to see how this functor should be applied. The O module passed as argument is the same as O in the result. It is passed here to avoid having multiple modules calling Hptset.Make on the same argument (which is forbidden by the datatype library, and would cause hashconsing problems)

module type Collapse = sig ... end

If C.collapse then L1.bottom,_ = _,L2.bottom = bottom

Uncollapsed product. Literally the set of (e1, e2) ordered pairs equipped with the order (e1, e2) < (d1, d2) <==> e1 < d1 && e2 < d2.

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