package codex

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

The Codex library for building static analysers based on abstract interpretation

Install

dune-project

Dependency

codex.top Edit opam file Versions (1)

Authors

Maintainers

M

Matthieu Lemerre <matthieu.lemerre@cea.fr>

Sources

1.0-rc4.tar.gz

md5=bc7266a140c6886add673ede90e335d3

sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

doc/codex.domains/Domains/Memory_domains/Symbolic_boolean/Make/index.html

Module `Symbolic_boolean.Make`

Parameters

module B : AbstractBoolean

Signature

module Scalar := B.Scalar

include Sig.With_Boolean with module Context = B.Scalar.Context

module Context = B.Scalar.Context

type boolean

module Boolean : Datatype_sig.S with type t = boolean

val boolean_pretty : Context.t -> Format.formatter -> boolean -> unit

val serialize_boolean : 
  Context.t ->
  boolean ->
  Context.t ->
  boolean ->
  'a Context.in_acc ->
  (boolean, 'a) Context.result

val boolean_empty : Context.t -> boolean

Empty denotes that the concretization has no value (or it is the concrete value representing the absence of value). Note that this does not necessarily imply that some error occured; for instance the offset of an uninitialized pointer can be represented with empty. Emptyness testing is a simple way of communicating between domains.

val boolean_unknown : Context.t -> boolean

module Boolean_Forward : 
  Operator.BOOLEAN_FORWARD
    with module Arity := Sig.Context_Arity_Forward(Context)
     and type boolean := boolean

val query_boolean : Context.t -> boolean -> Lattices.Quadrivalent.t

val lift : B.boolean -> boolean

val assume : Context.t -> boolean -> Context.t option

val satisfiable : Context.t -> boolean -> Smtbackend.Smtlib_sig.sat