Module Simple.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 rather naive, as it keeps only one abstract value for the (over-approximation) of the set of inputs and one abstract value for the (over-approximation) of the set of outputs.

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 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 meet : t -> t -> t
val dom : t -> dom list
val iter : (dom -> codom -> unit) -> t -> unit