Domain_builder (frama-c-eva.Eva.Domain

module type InputDomain = sig ... end

module type LeafDomain = sig ... end

Part 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.t

Automatically 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.t

module 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.t

module 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.t

module Restrict
  (Context : Abstract_context.S)
  (Value : Abstract_value.S with type context = Context.t)
  (Domain : sig ... end)
  (_ : sig ... end) : 
  sig ... end