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 (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.1-Nickel.tar.gz

sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

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
Plug-in Development Guide

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 Bool : sig ... end

module Make_Lattice_Base
  (V : Lattice_type.Lattice_Value) : 
  Lattice_type.Lattice_Base with type l = V.t

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)

module type Collapse = sig ... end

module Make_Lattice_Product
  (L1 : Lattice_type.AI_Lattice_with_cardinal_one)
  (L2 : Lattice_type.AI_Lattice_with_cardinal_one)
  (_ : Collapse) : 
  Lattice_type.Lattice_Product with type t1 = L1.t and type t2 = L2.t

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

module Make_Lattice_UProduct
  (L1 : Lattice_type.AI_Lattice_with_cardinal_one)
  (L2 : Lattice_type.AI_Lattice_with_cardinal_one) : 
  Lattice_type.Lattice_UProduct with type t1 = L1.t and type t2 = L2.t

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

module Make_Lattice_Sum
  (L1 : Lattice_type.AI_Lattice_with_cardinal_one)
  (L2 : Lattice_type.AI_Lattice_with_cardinal_one) : 
  Lattice_type.Lattice_Sum with type t1 = L1.t and type t2 = L2.t