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.terms/Terms/Smt/MakeFirstOrder/argument-2-S/index.html

Parameter MakeFirstOrder.S

type logic
type command
val qf_uf : logic
val qf_lia : logic
val qf_nia : logic
val qf_lra : logic
val qf_auflia : logic
val auflia : logic
val auflira : logic
val aufnira : logic
val lra : logic
val qf_idl : logic
val qf_rdl : logic
val qf_ufidl : logic
val qf_bv : logic
val qf_ax : logic
val qf_abv : logic
val qf_aubv : logic
val horn : logic
type satisfiable =
  1. | Sat
  2. | Unsat
  3. | Unknown
val check_sat : unit -> satisfiable
val set_logic : logic -> unit
val set_option : string -> unit
type sort
type value
val assert_ : value -> unit
val get_assignment : unit -> unit
val declare_var : ?name:string -> sort -> value
val define_var : ?name:string -> sort -> value -> value
val bool : sort
val let_ : ?name:string -> value -> (value -> value) -> value
val forall : ?name:string -> sort -> (value -> value) -> value
val exists : ?name:string -> sort -> (value -> value) -> value
val (=) : value -> value -> value
val (||) : value -> value -> value
val (&&) : value -> value -> value
val (=>) : value -> value -> value
val and_list : value list -> value
val or_list : value list -> value
val not : value -> value
val true_ : value
val false_ : value
val int : sort
val numeral : int -> value
val numeralz : Z.t -> value
val (<) : value -> value -> value
val (<=) : value -> value -> value
val (-) : value -> value -> value
val neg : value -> value
val (+) : value -> value -> value
val (*) : value -> value -> value
val div : value -> value -> value
val modu : value -> value -> value
val array : sort -> sort -> sort
val select : value -> value -> value
val store : value -> value -> value -> value
val bitvec : int -> sort
val bvlit : size:int -> Z.t -> value
val concat : value -> value -> value
val bvnot : value -> value
val bvneg : value -> value
val bvand : value -> value -> value
val bvor : value -> value -> value
val bvadd : value -> value -> value
val bvmul : value -> value -> value
val bvudiv : value -> value -> value
val bvurem : value -> value -> value
val bvshl : value -> value -> value
val bvlshr : value -> value -> value
val bvult : value -> value -> value
val extract : first:int -> last:int -> value -> value
val bvxor : value -> value -> value
val bvsdiv : value -> value -> value
val bvsrem : value -> value -> value
val bvsmod : value -> value -> value
val bvule : value -> value -> value
val bvslt : value -> value -> value
val bvsle : value -> value -> value
val bvashr : value -> value -> value
val sign_extend : int -> value -> value
val zero_extend : int -> value -> value