Module type `Memory_sig.OFFSET`

An AADT of offsets.

include AADT

module Scalar : Sig.BASE

include WITH_OFFSET
  with module Scalar := Scalar
   and type boolean = Scalar.boolean

type boolean = Scalar.boolean

type offset

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

Module type Memory_sig.OFFSET

Transfer functions

Module type `Memory_sig.OFFSET`