Module Sub.Address

module Scalar = Scalar

include Memory_sig.WITH_FIXED_SIZE_VALUE with module Scalar := Scalar

include Memory_sig.WITH_ADDRESS with module Scalar := Scalar

include Memory_sig.AADT with module Scalar := Scalar

type boolean

type 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_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.

include Sig.With_Binary with type boolean := boolean and type binary := binary and module Context := Scalar.Context

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 serialize_binary : 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

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

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

include Sig.With_Binary_Forward with module Context := Scalar.Context and type binary := binary and type boolean := boolean

module Binary_Forward : Operator.BINARY_FORWARD with module Arity := Sig.Context_Arity_Forward(Scalar.Context) and type boolean := boolean and type binary := binary

type enum

include Sig.With_Enum with type boolean := boolean and type enum := enum and module Context := Scalar.Context

module Enum : Datatype_sig.S with type t = enum

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

val serialize_enum : Scalar.Context.t -> enum -> Scalar.Context.t -> enum -> 'a Scalar.Context.in_acc -> (enum, 'a) Scalar.Context.result

val enum_empty : Scalar.Context.t -> enum

val enum_unknown : enumsize:int -> Scalar.Context.t -> enum

include Sig.With_Enum_Forward with module Context := Scalar.Context and type enum := enum and type boolean := boolean

module Enum_Forward : Operator.ENUM_FORWARD with module Arity := Sig.Context_Arity_Forward(Scalar.Context) and type boolean := boolean and type enum := enum

val union : Operator.Condition.t -> Scalar.Context.t -> 'a Scalar.Context.in_tuple -> 'a Scalar.Context.out_tuple

val global_symbol : Scalar.Context.t -> string -> Units.In_bits.t * binary

val add_global_symbol : size:Units.In_bits.t -> Scalar.Context.t -> string -> binary -> unit

val analyze_summary : Scalar.Context.t -> Types.TypedC.typ -> (Units.In_bits.t * binary) list -> bool * (Units.In_bits.t * binary) option

Check for given typ being a function type and a list of pairs of (size * argument) that all the arguments are correct for the function and returns a boolean (true if all arguments are correct) and the appropriate return value with its size (size * ret)

val addresses_in_binary : size:Units.In_bits.t -> Scalar.Context.t -> binary -> Scalar.Context.t -> binary -> (binary * binary) list

module Query : sig ... end

include Memory_sig.WITH_BOOLEAN_REDEFINITION with module Context = Scalar.Context and type boolean := boolean

include Sig.With_Boolean_Forward with type boolean := 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