Frama-C API - Map_lattice
Maps equipped with a lattice structure.
module type Value = sig ... endmodule type Lattice = sig ... endComplete semi-bounded lattice with over- and under-approximation, intersection and difference. No top value.
module type Lattice_with_cardinality = sig ... endComplete lattice as above, plus a notion of cardinality on the values.
module type Map_Lattice = sig ... endA map with a complete lattice structure.
module type Map_Lattice_with_cardinality = sig ... endA notion of cardinality for maps with a complete lattice structure.
module type MapSet_Lattice = sig ... endA 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 ... endA 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 ... endEquips 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 ... endBuilds a lattice mixing maps and sets, provided that each one has a lattice structure.