Module Domain_builder

module Domain_builder: sig .. end

Automatic builders to complete abstract domains from different simplified interfaces.

module type InputDomain = sig .. end

module type LeafDomain = sig .. end

Part of an abstract domain signature automatically built by the Domain_builder.Complete functor.

module Complete: functor (Domain : InputDomain) -> LeafDomain  with type t := Domain.t

Automatically builds some functions of an abstract domain.

module Complete_Minimal: functor (Value : Abstract_value.S) -> functor (Location : Abstract_location.S) -> functor (Domain : Simpler_domains.Minimal) -> Abstract_domain.Leaf  with type value = Value.t
                          and type location = Location.location
                          and type state = Domain.t

module Complete_Minimal_with_datatype: functor (Value : Abstract_value.S) -> functor (Location : Abstract_location.S) -> functor (Domain : Simpler_domains.Minimal_with_datatype) -> Abstract_domain.Leaf  with type value = Value.t
                          and type location = Location.location
                          and type state = Domain.t

module Complete_Simple_Cvalue: functor (Domain : Simpler_domains.Simple_Cvalue) -> Abstract_domain.Leaf  with type value = Cvalue.V.t
                          and type location = Precise_locs.precise_location
                          and type state = Domain.t

module Restrict: functor (Value : Abstract_value.S) -> functor (Domain : Abstract.Domain.Internal  with type value = Value.t) -> functor (Scope : sig

val functions : Domain_mode.function_mode list

end) -> Abstract.Domain.Internal  with type value = Value.t
                              and type location = Domain.location