Frama-C API - Domain_builder
Automatic builders to complete abstract domains from different simplified interfaces.
module type InputDomain = Domain_store.InputDomainmodule type LeafDomain = sig ... endPart of an abstract domain signature automatically built by the Complete functor. These functions can be redefined to achieve better precision or performance. See Abstract_domain for more details.
module Complete (Domain : InputDomain) : LeafDomain with type t := Domain.tAutomatically builds some functions of an abstract domain.
module Complete_Minimal (Value : Abstract_value.Leaf) (Location : Abstract_location.Leaf) (Domain : Simpler_domains.Minimal) : Abstract_domain.Leaf with type context = unit and type value = Value.t and type location = Location.location and type state = Domain.tmodule Complete_Minimal_with_datatype (Value : Abstract_value.Leaf) (Location : Abstract_location.Leaf) (Domain : Simpler_domains.Minimal_with_datatype) : Abstract_domain.Leaf with type context = unit and type value = Value.t and type location = Location.location and type state = Domain.tmodule Complete_Simple_Cvalue (Domain : Simpler_domains.Simple_Cvalue) : Abstract_domain.Leaf with type context = unit and type value = Frama_c_kernel.Cvalue.V.t and type location = Frama_c_kernel.Precise_locs.precise_location and type state = Domain.tmodule Restrict (Context : Abstract_context.S) (Value : Abstract_value.S with type context = Context.t) (Domain : Abstract.Domain.Internal with type context = Context.t and type value = Value.t) (_ : sig ... end) : Abstract.Domain.Internal with type context = Context.t and type value = Value.t and type location = Domain.location