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 Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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

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)