Module Jasmin.Wsize

type __ = Obj.t
type wsize =
  1. | U8
  2. | U16
  3. | U32
  4. | U64
  5. | U128
  6. | U256
type is_wsize =
  1. | Coq_is_U8
  2. | Coq_is_U16
  3. | Coq_is_U32
  4. | Coq_is_U64
  5. | Coq_is_U128
  6. | Coq_is_U256
val wsize_tag : wsize -> BinNums.positive
val is_wsize_inhab : wsize -> is_wsize
type box_wsize_U8 =
  1. | Box_wsize_U8
type wsize_fields_t = __
val wsize_fields : wsize -> wsize_fields_t
val wsize_eqb_fields : (wsize -> wsize -> bool) -> BinNums.positive -> wsize_fields_t -> wsize_fields_t -> bool
val wsize_eqb : wsize -> wsize -> bool
val wsize_eqb_OK : wsize -> wsize -> Bool.reflect
type velem =
  1. | VE8
  2. | VE16
  3. | VE32
  4. | VE64
type is_velem =
  1. | Coq_is_VE8
  2. | Coq_is_VE16
  3. | Coq_is_VE32
  4. | Coq_is_VE64
val velem_tag : velem -> BinNums.positive
val is_velem_inhab : velem -> is_velem
type box_velem_VE8 =
  1. | Box_velem_VE8
type velem_fields_t = __
val velem_fields : velem -> velem_fields_t
val velem_eqb_fields : (velem -> velem -> bool) -> BinNums.positive -> velem_fields_t -> velem_fields_t -> bool
val velem_eqb : velem -> velem -> bool
val wsize_of_velem : velem -> wsize
type pelem =
  1. | PE1
  2. | PE2
  3. | PE4
  4. | PE8
  5. | PE16
  6. | PE32
  7. | PE64
  8. | PE128
type is_pelem =
  1. | Coq_is_PE1
  2. | Coq_is_PE2
  3. | Coq_is_PE4
  4. | Coq_is_PE8
  5. | Coq_is_PE16
  6. | Coq_is_PE32
  7. | Coq_is_PE64
  8. | Coq_is_PE128
val pelem_tag : pelem -> BinNums.positive
val is_pelem_inhab : pelem -> is_pelem
type box_pelem_PE1 =
  1. | Box_pelem_PE1
type pelem_fields_t = __
val pelem_fields : pelem -> pelem_fields_t
val pelem_eqb_fields : (pelem -> pelem -> bool) -> BinNums.positive -> pelem_fields_t -> pelem_fields_t -> bool
val pelem_eqb : pelem -> pelem -> bool
type signedness =
  1. | Signed
  2. | Unsigned
type is_signedness =
  1. | Coq_is_Signed
  2. | Coq_is_Unsigned
val signedness_tag : signedness -> BinNums.positive
val is_signedness_inhab : signedness -> is_signedness
type box_signedness_Signed =
  1. | Box_signedness_Signed
type signedness_fields_t = __
val signedness_fields : signedness -> signedness_fields_t
val signedness_eqb_fields : (signedness -> signedness -> bool) -> BinNums.positive -> signedness_fields_t -> signedness_fields_t -> bool
val signedness_eqb : signedness -> signedness -> bool
val signedness_eqb_OK : signedness -> signedness -> Bool.reflect
val coq_HB_unnamed_factory_1 : signedness Eqtype.Coq_hasDecEq.axioms_
val wsize_signedness__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_3 : wsize Eqtype.Coq_hasDecEq.axioms_
val wsize_wsize__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val wsize_eq_dec : wsize -> wsize -> bool
val wsizes : wsize list
val wsize_cmp : wsize -> wsize -> Datatypes.comparison
val size_8_16 : wsize -> bool
val size_8_32 : wsize -> bool
val size_8_64 : wsize -> bool
val size_16_32 : wsize -> bool
val size_16_64 : wsize -> bool
val size_32_64 : wsize -> bool
val size_64_128 : wsize -> bool
val size_128_256 : wsize -> bool
val string_of_wsize : wsize -> string
val string_of_ve_sz : velem -> wsize -> string
val pp_s : string -> unit -> string
val pp_sz : string -> wsize -> unit -> string
val pp_ve_sz : string -> velem -> wsize -> unit -> string
val pp_ve_sz_ve_sz : string -> velem -> wsize -> velem -> wsize -> unit -> string
val pp_sz_sz : string -> bool -> wsize -> wsize -> unit -> string
type reg_kind =
  1. | Normal
  2. | Extra
type is_reg_kind =
  1. | Coq_is_Normal
  2. | Coq_is_Extra
val reg_kind_tag : reg_kind -> BinNums.positive
val is_reg_kind_inhab : reg_kind -> is_reg_kind
type box_reg_kind_Normal =
  1. | Box_reg_kind_Normal
type reg_kind_fields_t = __
val reg_kind_fields : reg_kind -> reg_kind_fields_t
val reg_kind_eqb_fields : (reg_kind -> reg_kind -> bool) -> BinNums.positive -> reg_kind_fields_t -> reg_kind_fields_t -> bool
val reg_kind_eqb : reg_kind -> reg_kind -> bool
type writable =
  1. | Constant
  2. | Writable
type reference =
  1. | Direct
  2. | Pointer of writable
type v_kind =
  1. | Const
  2. | Stack of reference
  3. | Reg of reg_kind * reference
  4. | Inline
  5. | Global
type safe_cond =
  1. | NotZero of wsize * Datatypes.nat
  2. | X86Division of wsize * signedness
  3. | InRangeMod32 of wsize * BinNums.coq_Z * BinNums.coq_Z * Datatypes.nat
  4. | ULt of wsize * Datatypes.nat * BinNums.coq_Z
  5. | UGe of wsize * BinNums.coq_Z * Datatypes.nat
  6. | UaddLe of wsize * Datatypes.nat * Datatypes.nat * BinNums.coq_Z
  7. | AllInit of wsize * BinNums.positive * Datatypes.nat
  8. | ScFalse
type coq_PointerData = wsize
type coq_MSFsize = wsize