Parameter MakeComplete.Block

include Memory_sig.AADT_WITH_BOOLEAN with module Scalar = Sub.Scalar

include Memory_sig.AADT with module Scalar = Sub.Scalar

module Scalar = Sub.Scalar

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

module Offset : Memory_sig.OFFSET with module Scalar = Scalar

module Value = Sub.Address

type offset = Offset.offset

type block

val pretty : Context.t -> Stdlib.Format.formatter -> block -> unit

include Operator.BLOCK_FORWARD with module Arity := Sig.Context_Arity_Forward(Context) and type boolean := boolean and type value := Value.binary and type block := block and type offset := offset

val sizeof : (block, offset) Sig.Context_Arity_Forward(Context).ar1

Size of a block in bytes

val concat : (block, block, block) Sig.Context_Arity_Forward(Context).ar2

Concatenates two blocks

val load : size:Units.In_bits.t -> (block, offset, Value.binary) Sig.Context_Arity_Forward(Context).ar2

Loads (extracts) a value of a fixed size at a given index from a block

val store : size:Units.In_bits.t -> (block, offset, Value.binary, block) Sig.Context_Arity_Forward(Context).ar3

Stores (writes) a fixed size value of a given index in a block

val binary_to_block : size:Units.In_bits.t -> (Value.binary, block) Sig.Context_Arity_Forward(Context).ar1

Converts a fixed size value to a block

val addresses_in_block : Context.t -> block -> Context.t -> block -> (Value.binary * Value.binary) list

val serialize : widens:bool -> Context.t -> block -> Context.t -> block -> 'a Context.in_acc -> (block, 'a) Context.result

val initial : Context.t -> Units.In_bytes.t -> block

Create an initial region of size int (in bytes). Only meaning full for memories that are a single contiguous region

val unknown : level:int -> Context.t -> block

val block_empty : Context.t -> block

An empty region, with no bound offset.

val block_unknown_typed : Context.t -> Types.TypedC.typ -> block

Returns an unknown block value with a given type.

val check_type : Context.t -> Types.TypedC.typ -> block -> block Types.Type_check_tree.t

Type check a block value