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-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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

Module `Frama_c_kernel.Map_lattice`

Maps equipped with a lattice structure.

module type Value = sig ... end

module type Lattice = sig ... end

Complete semi-bounded lattice with over- and under-approximation, intersection and difference. No top value.

module type Lattice_with_cardinality = sig ... end

Complete lattice as above, plus a notion of cardinality on the values.

module type Map_Lattice = sig ... end

A map with a complete lattice structure.

module type Map_Lattice_with_cardinality = sig ... end

A notion of cardinality for maps with a complete lattice structure.

module type MapSet_Lattice = sig ... end

A lattice structure on top of maps from keys to values and sets of keys. The maps and the sets have their own lattice structure (see abstract_interp.ml for the lattice of sets). The sets are implicitly considered as maps binding all their keys to top. Any map is included in the set of its keys (and in any larger set).

module type MapSet_Lattice_with_cardinality = sig ... end

A notion of cardinality for mapset lattice.

module Make_Map_Lattice
  (Key : Hptmap.Id_Datatype)
  (Value : Lattice_type.Full_Lattice)
  (KVMap : Hptmap_sig.S with type key = Key.t and type v = Value.t) : 
  sig ... end

Equips an Hptmap with a lattice structure, provided that the values have a lattice structure.

module Make_MapSet_Lattice
  (Key : Hptmap.Id_Datatype)
  (KSet : Lattice_type.Lattice_Set with type O.elt = Key.t)
  (Value : Value)
  (KVMap : Map_Lattice with type key = Key.t and type v = Value.t) : 
  sig ... end

Builds a lattice mixing maps and sets, provided that each one has a lattice structure.