Parameter MakeForAADT.D

include Memory_sig.AADT

module Scalar : Sig.BASE

include Memory_sig.WITH_BOOLEAN_REDEFINITION with module Context = Scalar.Context

include Sig.With_Boolean_Forward

type boolean

include Sig.With_Boolean with type boolean := boolean with module Context = Scalar.Context

module Context = Scalar.Context

module Boolean : Datatype_sig.S with type t = boolean

val boolean_pretty : Context.t -> Stdlib.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 assume : Context.t -> boolean -> Context.t option