package jasmin

  1. Overview
  2. Docs

Module Jasmin.Arm_decl

type __ = Obj.t
val arm_reg_size : Wsize.wsize
val arm_xreg_size : Wsize.wsize
type register =
  1. | R00
  2. | R01
  3. | R02
  4. | R03
  5. | R04
  6. | R05
  7. | R06
  8. | R07
  9. | R08
  10. | R09
  11. | R10
  12. | R11
  13. | R12
  14. | LR
  15. | SP
val register_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
val register_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
type is_register =
  1. | Coq_is_R00
  2. | Coq_is_R01
  3. | Coq_is_R02
  4. | Coq_is_R03
  5. | Coq_is_R04
  6. | Coq_is_R05
  7. | Coq_is_R06
  8. | Coq_is_R07
  9. | Coq_is_R08
  10. | Coq_is_R09
  11. | Coq_is_R10
  12. | Coq_is_R11
  13. | Coq_is_R12
  14. | Coq_is_LR
  15. | Coq_is_SP
val is_register_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> is_register -> 'a1
val is_register_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> is_register -> 'a1
val register_tag : register -> BinNums.positive
val is_register_inhab : register -> is_register
val is_register_functor : register -> is_register -> is_register
type box_register_R00 =
  1. | Box_register_R00
type register_fields_t = __
val register_fields : register -> register_fields_t
val register_construct : BinNums.positive -> register_fields_t -> register option
val register_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> is_register -> 'a1
val register_eqb_fields : (register -> register -> bool) -> BinNums.positive -> register_fields_t -> register_fields_t -> bool
val register_eqb : register -> register -> bool
val register_eqb_OK : register -> register -> Datatypes.reflect
val register_eqb_OK_sumbool : register -> register -> bool
val eqTC_register : register Utils0.eqTypeC
val arm_register_eqType : Eqtype.Equality.coq_type
val registers : register list
val finTC_register : register Utils0.finTypeC
val register_finType : Fintype.Finite.coq_type
val register_to_string : register -> string
val shift_kind_eqType : Eqtype.Equality.coq_type
val shift_kinds : Shift_kind.shift_kind list
val string_of_shift_kind : Shift_kind.shift_kind -> string
val check_shift_amount : Shift_kind.shift_kind -> BinNums.coq_Z -> bool
val shift_of_sop2 : Wsize.wsize -> Operators.sop2 -> Shift_kind.shift_kind option
type arm_caimm_cond =
  1. | CAimmC_arm_shift_amout of Shift_kind.shift_kind
  2. | CAimmC_arm_wencoding of Arm_expand_imm.expected_wencoding
  3. | CAimmC_arm_0_8_16_24
val arm_caimm_cond_rect : (Shift_kind.shift_kind -> 'a1) -> (Arm_expand_imm.expected_wencoding -> 'a1) -> 'a1 -> arm_caimm_cond -> 'a1
val arm_caimm_cond_rec : (Shift_kind.shift_kind -> 'a1) -> (Arm_expand_imm.expected_wencoding -> 'a1) -> 'a1 -> arm_caimm_cond -> 'a1
type is_arm_caimm_cond =
  1. | Coq_is_CAimmC_arm_shift_amout of Shift_kind.shift_kind * Shift_kind.is_shift_kind
  2. | Coq_is_CAimmC_arm_wencoding of Arm_expand_imm.expected_wencoding * Arm_expand_imm.is_expected_wencoding
  3. | Coq_is_CAimmC_arm_0_8_16_24
val arm_caimm_cond_tag : arm_caimm_cond -> BinNums.positive
val is_arm_caimm_cond_inhab : arm_caimm_cond -> is_arm_caimm_cond
val is_arm_caimm_cond_functor : arm_caimm_cond -> is_arm_caimm_cond -> is_arm_caimm_cond
type box_arm_caimm_cond_CAimmC_arm_shift_amout = Shift_kind.shift_kind
val coq_Box_arm_caimm_cond_CAimmC_arm_shift_amout_0 : box_arm_caimm_cond_CAimmC_arm_shift_amout -> Shift_kind.shift_kind
type box_arm_caimm_cond_CAimmC_arm_wencoding = Arm_expand_imm.expected_wencoding
val coq_Box_arm_caimm_cond_CAimmC_arm_wencoding_0 : box_arm_caimm_cond_CAimmC_arm_wencoding -> Arm_expand_imm.expected_wencoding
type box_arm_caimm_cond_CAimmC_arm_0_8_16_24 =
  1. | Box_arm_caimm_cond_CAimmC_arm_0_8_16_24
type arm_caimm_cond_fields_t = __
val arm_caimm_cond_fields : arm_caimm_cond -> arm_caimm_cond_fields_t
val arm_caimm_cond_construct : BinNums.positive -> arm_caimm_cond_fields_t -> arm_caimm_cond option
val arm_caimm_cond_eqb_fields : (arm_caimm_cond -> arm_caimm_cond -> bool) -> BinNums.positive -> arm_caimm_cond_fields_t -> arm_caimm_cond_fields_t -> bool
val arm_caimm_cond_eqb : arm_caimm_cond -> arm_caimm_cond -> bool
val arm_caimm_cond_eqb_OK : arm_caimm_cond -> arm_caimm_cond -> Datatypes.reflect
val arm_caimm_cond_eqb_OK_sumbool : arm_caimm_cond -> arm_caimm_cond -> bool
val eqTC_arm_caimm_cond : arm_caimm_cond Utils0.eqTypeC
val arm_check_CAimm : arm_caimm_cond -> Wsize.wsize -> Word0.word -> bool
val arm_caimm_cond_pp : arm_caimm_cond -> string
val is_expandable : BinNums.coq_Z -> bool
val is_expandable_or_shift : BinNums.coq_Z -> bool