package codex

You can search for identifiers within the package.

in-package search v0.2.0

Module `Single_value_abstraction.Ival`Source

Our main bitvector abstraction: interval and congruence abstraction, for both the signed and unsigned interpretation of bitvectors.

Sourcetype boolean = Lattices.Quadrivalent.boolean

Sourcetype integer = Framac_ival.Ival.t

Source

module Integer_Forward : 
  Operator.INTEGER_FORWARD
    with module Arity := Operator.Forward_Arity
     and type boolean := boolean
     and type integer := integer

Source

module Integer_Backward : 
  Operator.INTEGER_BACKWARD
    with module Arity := Operator.Backward_Arity
     and type boolean := boolean
     and type integer := integer

Source

module Boolean_Forward : 
  Operator.BOOLEAN_FORWARD
    with module Arity := Operator.Forward_Arity
     and type boolean := boolean

Source

module Boolean_Backward : 
  Operator.BOOLEAN_BACKWARD
    with module Arity := Operator.Backward_Arity
     and type boolean := boolean

Sourcemodule Boolean_Lattice : Lattices.Sig.BOOLEAN_LATTICE with type t = boolean

Sourcemodule Integer_Lattice : Lattices.Sig.INTEGER_LATTICE with type t = integer

Sourceval name : string

Sourcetype bitvector

Source

module Bitvector_Forward : 
  Operator.BITVECTOR_FORWARD_WITH_BIMUL_ADD
    with module Arity := Operator.Forward_Arity
     and type boolean := boolean
     and type bitvector := bitvector

Sourcemodule Bitvector_Backward : sig ... end

Source

module Bitvector_Lattice : 
  Lattices.Sig.BITVECTOR_LATTICE with type t = bitvector

Sourceval integer_is_singleton : integer -> Z.t option

package codex

Module Single_value_abstraction.IvalSource

Module `Single_value_abstraction.Ival`Source