package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-beta-Gallium.tar.gz

sha256=095ffbb3086a6cd963a03e3defab4f0dc32e9a43f026e552ec9ae346a6e20522

doc/frama-c.kernel/Frama_c_kernel/Abstract_interp/index.html

Module `Frama_c_kernel.Abstract_interp`

Functors for generic lattices implementations.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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 =

| True
| False
| 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 Make_Lattice_Set
  (V : Datatype.S)
  (Set : Lattice_type.Hptset with type elt = V.t) : 
  Lattice_type.Lattice_Set with module O = Set

module Make_Hashconsed_Lattice_Set
  (V : Hptmap.Id_Datatype)
  (Set : Hptset.S with type elt = V.t) : 
  Lattice_type.Lattice_Set with module O = Set

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)