package codex
The Codex library for building static analysers based on abstract interpretation
Install
dune-project
Dependency
Authors
Maintainers
Sources
1.0-rc4.tar.gz
md5=bc7266a140c6886add673ede90e335d3
sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386
doc/codex.domains/Domains/Log/Log_With_Focusing/argument-2-Sub/Query/index.html
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.