Module `Region_suffix_tree.MakeOffset`

Parameters

module Scalar : Sig.BASE

Signature

include Memory_sig.OFFSET
  with module Scalar = Scalar
  with type boolean = Scalar.boolean

include Memory_sig.AADT with module Scalar = Scalar

module Scalar = Scalar

include Memory_sig.WITH_OFFSET
  with module Scalar := Scalar
   and type boolean = Scalar.boolean
  with 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

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

Module Region_suffix_tree.MakeOffset

Parameters

Signature

Transfer functions

Module `Region_suffix_tree.MakeOffset`