Parameter `Make._`

module Terms = Terms

val name : string

type t

Type for elements of the abstract domain. The interface is persistent but the implementation can be imperative.

type binary = Operator.Function_symbol.binary Terms.t

Represent binary, integer and boolean dimensions/variables in the abstract domain.

type integer = Operator.Function_symbol.integer Terms.t

type boolean = Operator.Function_symbol.boolean Terms.t

type enum = Operator.Function_symbol.enum Terms.t

val equal : t -> t -> bool

val top : t

module Integer_Query : sig ... end

Projection to a non-relational basis.

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

widened_fixpoint_step ~previous ~previous_tup ~next ~next_tup bool ~res_tup where:

previous is the previous domain state and previous_tup the tuple of phi arguments;
next is the next domain state obtained by joining execution of the function body and initial state and next_tup the phi arguments;
bool is false if we know that the fixpoint is not reached yet, and true otherwise;
res_tup is the terms corresponding to the phi function;

returns a triple (context,bool) where:

context is the new domain state;
bool is true if the fixpoint is reached, and false if not reached or we don't know.

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

Returns None if the result is bottom.

module Domain_Arity : sig ... end

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

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

module Binary_Forward : 
  Operator.BINARY_FORWARD
    with module Arity := Domain_Arity
     and type boolean := boolean
     and type binary := binary

module Enum_Forward : 
  Operator.ENUM_FORWARD
    with module Arity := Domain_Arity
     and type boolean := boolean
     and type enum := enum

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

val integer_pretty : t -> Stdlib.Format.formatter -> integer -> unit

val binary_pretty : 
  size:Units.In_bits.t ->
  t ->
  Stdlib.Format.formatter ->
  binary ->
  unit

val enum_pretty : t -> Stdlib.Format.formatter -> enum -> unit

val pretty : Stdlib.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)

Tells if fixpoint is reached, and prepare to write the new values. The returned pair (bool,function) allows to decide whether we should end the fixpoint computation; the function represents a continuation, and the boolean tells whether the fixpoint is reached (if yes, we can close, but we don't have to).

Parameter Make._

Parameter `Make._`