Module type `Memory_sig.ADDRESS`

Representation of pointers inside some memory regions.

include AADT_WITH_BOOLEAN

include AADT

module Scalar : Sig.BASE

include 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

include WITH_ADDRESS with module Scalar := Scalar and type boolean := boolean

include AADT with module Scalar := Scalar

type binary

module Binary : Datatype_sig.S with type t = binary

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

val binary_empty : size:Units.In_bits.t -> Scalar.Context.t -> binary

val satisfiable : Scalar.Context.t -> boolean -> Smtbackend.Smtlib_sig.sat

val serialize : 
  widens:bool ->
  size:Units.In_bits.t ->
  Scalar.Context.t ->
  binary ->
  Scalar.Context.t ->
  binary ->
  'a Scalar.Context.in_acc ->
  (binary, 'a) Scalar.Context.result

Serialize functions also return their de-serializer.

val bchoose : 
  size:Units.In_bits.t ->
  Operator.Choice.t ->
  Scalar.Context.t ->
  binary ->
  binary

val bindex : 
  size:Units.In_bits.t ->
  int ->
  Scalar.Context.t ->
  binary ->
  Scalar.binary ->
  binary

bindex ~size k ctx address expr is address + k * expr

val bisub : 
  size:Units.In_bits.t ->
  Scalar.Context.t ->
  binary ->
  binary ->
  Scalar.binary

pointer substraction.

val bshift : 
  size:Units.In_bits.t ->
  offset:int ->
  max:int option ->
  Scalar.Context.t ->
  binary ->
  binary

bshift ~size ~offset ~max ctx address is address + offset. In addition, further shifts/index are bounded by max.

val ble : 
  size:Units.In_bits.t ->
  Scalar.Context.t ->
  binary ->
  binary ->
  boolean

Pointer comparison.

val beq : 
  size:Units.In_bits.t ->
  Scalar.Context.t ->
  binary ->
  binary ->
  boolean

val binary_unknown : size:Units.In_bits.t -> Scalar.Context.t -> binary

val binary_unknown_typed : 
  size:Units.In_bits.t ->
  Scalar.Context.t ->
  Types.TypedC.typ ->
  binary

val check_type : 
  size:Units.In_bits.t ->
  Scalar.Context.t ->
  Types.TypedC.typ ->
  binary ->
  binary Types.Type_check_tree.t

Type check a binary value

val binary2scalar_binary : 
  size:Units.In_bits.t ->
  Scalar.Context.t ->
  binary ->
  Scalar.binary

val type_of : 
  size:Units.In_bits.t ->
  Scalar.Context.t ->
  binary ->
  Types.TypedC.typ option

Returns the type of a function, or None if unknown.

val within_bounds : 
  size:Units.In_bits.t ->
  Scalar.Context.t ->
  binary ->
  boolean

Check that all array indices operation are within bound.

module Query : sig ... end

Module type Memory_sig.ADDRESS

Module type `Memory_sig.ADDRESS`