Module Elementary.Make

Functor that creates an abstract domain that abstracts a minimal function graph, from an abstract domain for the input values of the graph, and an abstract domain for the output values of the graph.

The resulting abstract domain for function graphs is "elementary" in the sense of F. Bourdoncle 1. It is implemented as an association list, that maps elements of the domain to elements of the codomain. The meaning is that of a function that maps an element x to the join of all the elements of the codomain that are associated to an element of the domain that covers x, i.e., that intersects with x.

The widening strategy is simple: when entries that are not covered must be added, they are first widenened with some already present entries.

1 Bourdoncle, F. Abstract Interpretation by Dynamic Partitioning J. Funct. Program., 1992, 2, 407-423

Parameters

module D1 : sig ... end
module D2 : sig ... end

Signature

include Sigs.MFG with type dom = D1.t and type codom = D2.t and type strategy = strategy
type dom = D1.t
type codom = D2.t
type t
type strategy = strategy
val bot : t
val is_bot : t -> bool
val init : dom -> t
val leq : t -> t -> bool
val map : (dom -> codom) -> t -> t
val apply : t -> dom -> codom
val join : t -> t -> t
val meet : t -> t -> t
val widen_gen : strategy array -> int -> t -> t -> t
val default_strategy : strategy array
val widen : int -> t -> t -> t
val pp : Stdlib.Format.formatter -> t -> unit
val iter : (dom -> codom -> unit) -> t -> unit
val dom : t -> dom list