package frama-c

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

Functors for generic lattices implementations.

val feedback_approximation : ('a, Format.formatter, unit) format -> 'a
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

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)

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