Module Make.Offset

include Memory_sig.FIXED_SIZE_VALUE_DOMAIN with module Scalar = Scalar and module Context = Scalar.Context and type binary = Scalar.binary and type boolean = Scalar.boolean and module Context = Scalar.Context

module Scalar = Scalar

include Memory_sig.WITH_FIXED_SIZE_VALUE with module Scalar := Scalar with type binary = Scalar.binary with type boolean = Scalar.boolean

include Memory_sig.WITH_ADDRESS with module Scalar := Scalar with type binary = Scalar.binary with type boolean = Scalar.boolean

include Memory_sig.AADT with module Scalar := Scalar

type boolean = Scalar.boolean

type binary = Scalar.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 with module Context = Scalar.Context with module Context = Scalar.Context

include Sig.With_Boolean_Forward with type boolean := boolean

include Sig.With_Boolean with type boolean := boolean with module Context = Scalar.Context with module Context = Scalar.Context 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 Fully_expanded_finite_region.Enumerable_offset with module Scalar := Scalar and type offset = Scalar.binary and type boolean := boolean

include Memory_sig.OFFSET with module Scalar := Scalar with type offset = Scalar.binary with type boolean := boolean

include Memory_sig.AADT with module Scalar := Scalar

include Memory_sig.WITH_OFFSET with module Scalar := Scalar and type boolean = Scalar.boolean with type offset = Scalar.binary with type boolean := boolean

type offset = Scalar.binary

module Offset : sig ... end

val offset_pretty : Scalar.Context.t -> Stdlib.Format.formatter -> offset -> unit

val offset_empty : Scalar.Context.t -> offset

val serialize_offset : widens:bool -> Scalar.Context.t -> offset -> Scalar.Context.t -> offset -> 'a Scalar.Context.in_acc -> (offset, 'a) Scalar.Context.result

Transfer functions

val offset_zero : max:int option -> Scalar.Context.t -> offset

Beginning of a region (offset 0) of size max (in bytes, if known and/or useful).

val offset_shift : offset:int -> max:int option -> Scalar.Context.t -> offset -> offset

offset_shift offset:k o adds a suffix .f, i.e. returns o.f when the field f has relative offset k.

val offset_index : int -> Scalar.Context.t -> offset -> Scalar.binary -> offset

offset_index size:k o i adds a suffix [i], i.e. returns o[i] when o was pointing to an array of elements of size k.

val offset_sub : Scalar.Context.t -> offset -> offset -> Scalar.binary

offset_sub o1 o2 when o1 is a suffix of o2 returns the suffix part. E.g. offset_sub o1.k.a[3] o1 returns .k.a[3].

val offset_le : Scalar.Context.t -> offset -> offset -> boolean

Offset comparison.

val offset_eq : Scalar.Context.t -> offset -> offset -> boolean

val offset_within_bounds : size:Units.In_bits.t -> Scalar.Context.t -> offset -> boolean

Check that all array indices operation are within bound.

val offset_choose : Operator.Choice.t -> Scalar.Context.t -> offset -> offset

val boolean2scalar_bool : Scalar.Context.t -> boolean -> Scalar.boolean

Lift/unlift a boolean to a Scalar.boolean. Probably this should not be part of the domain signature.

val scalar_bool2boolean : Scalar.Context.t -> Scalar.boolean -> boolean

val fold_crop : size:Units.In_bits.t -> Scalar.Context.t -> offset -> inf:Z.t -> sup:Z.t -> (Z.t -> 'a -> 'a) -> 'a -> 'a

val is_precise : size:Units.In_bits.t -> Scalar.Context.t -> offset -> Z.t Memory_sig.precision

val in_bounds : size:Units.In_bits.t -> Scalar.Context.t -> offset -> inf:Z.t -> sup:Z.t -> bool