package codex

  1. Overview
  2. Docs
The Codex library for building static analysers based on abstract interpretation

Install 

dune-project
 Dependency

codex.top Edit opam file Versions (1)

Authors

  1. M
    Matthieu Lemerre
  2. J
    Julien Simonnet
  3. O
    Olivier Nicole
  4. P
    Paul Robert
  5. D
    Dorian Lesbre
  6. I
    Iker Canut
  7. C
    Corentin Gendreau
  8. G
    Guillaume Girol
  9. C
    Charles Babu
  10. J
    Jérôme Faucheux

Maintainers

  1. M
    Matthieu Lemerre <matthieu.lemerre@cea.fr>

Sources

1.0-rc4.tar.gz
md5=bc7266a140c6886add673ede90e335d3
sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

doc/codex.whilelib/Whilelib/While_analysis/NonRelationalDomain/index.html

Module While_analysis.NonRelationalDomain

module Terms : sig ... end
val name : string
type t
val equal : t -> t -> bool
val top : t
module Integer_Query : sig ... end
module Query : sig ... end
val nondet : doma:t -> tupa:Terms.any Immutable_array.t -> domb:t -> tupb:Terms.any Immutable_array.t -> tupres:Terms.any Immutable_array.t -> t
val widened_fixpoint_step : previous:t -> previous_tup:Terms.any Immutable_array.t -> next:t -> next_tup:Terms.any Immutable_array.t -> bool -> res_tup:Terms.any Immutable_array.t -> t * bool
val integer_empty : t -> integer -> t
val boolean_empty : t -> boolean -> t
val binary_empty : size:Units.In_bits.t -> t -> binary -> t
val enum_empty : t -> enum -> t
val integer_unknown : t -> integer -> t
val boolean_unknown : t -> boolean -> t
val binary_unknown : size:Units.In_bits.t -> t -> binary -> t
val enum_unknown : enumsize:int -> t -> enum -> t
val assume : t -> boolean -> t option
module Domain_Arity : sig ... end
module Boolean_Forward : sig ... end
module Integer_Forward : sig ... end
module Binary_Forward : sig ... end
module Enum_Forward : sig ... end
val boolean_pretty : t -> Format.formatter -> boolean -> unit
val integer_pretty : t -> Format.formatter -> integer -> unit
val binary_pretty : size:Units.In_bits.t -> t -> Format.formatter -> binary -> unit
val enum_pretty : t -> Format.formatter -> enum -> unit
val pretty : Format.formatter -> t -> unit
val fixpoint_open : unit -> unit
val fixpoint_step : lvl:int -> iteration:int -> t -> actuals:Terms.any Immutable_array.t -> t -> args:Terms.any Immutable_array.t -> t -> finals:Terms.any Immutable_array.t -> bool * (close:bool -> Terms.any Immutable_array.t -> t)