package codex
Module Sub.Query
module Binary_Lattice : Sig.Binary_Latticemodule Enum_Lattice : Sig.Enum_Latticeval enum : Context.t -> enum -> Enum_Lattice.tval binary : size:Units.In_bits.t -> Context.t -> binary -> Binary_Lattice.tval reachable : Context.t -> memory -> Domains.Sig.Quadrivalent.tReachable 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
FalseorBottom, the memory is not reachable.