package frama-c

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

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.

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.