Module Make.Query

module Binary_Lattice : Sig.Binary_Lattice

module Enum_Lattice : Sig.Enum_Lattice

val enum : Context.t -> enum -> Enum_Lattice.t

val binary : size:Units.In_bits.t -> Context.t -> binary -> Binary_Lattice.t

val reachable : Context.t -> memory -> Domains.Sig.Quadrivalent.t

Reachable means that the set of memory states is not empty.

• If we return Top (i.e. {True,False}), then the memory may be reachable;
• If we return True, then the memory is reachable;
• If we return False or Bottom, the memory is not reachable.