package jasmin

  1. Overview
  2. Docs
package jasmin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Jasmin.X86_extra

type __ = Obj.t
module E : sig ... end
type x86_extra_op =
  1. | Oset0 of Wsize.wsize
  2. | Oconcat128
  3. | Ox86MOVZX32
  4. | Ox86MULX of Wsize.wsize
  5. | Ox86MULX_hi of Wsize.wsize
  6. | Ox86SLHinit
  7. | Ox86SLHupdate
  8. | Ox86SLHmove
  9. | Ox86SLHprotect of Wsize.reg_kind * Wsize.wsize
val x86_extra_op_rect : (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (Wsize.reg_kind -> Wsize.wsize -> 'a1) -> x86_extra_op -> 'a1
val x86_extra_op_rec : (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (Wsize.reg_kind -> Wsize.wsize -> 'a1) -> x86_extra_op -> 'a1
type is_x86_extra_op =
  1. | Coq_is_Oset0 of Wsize.wsize * Wsize.is_wsize
  2. | Coq_is_Oconcat128
  3. | Coq_is_Ox86MOVZX32
  4. | Coq_is_Ox86MULX of Wsize.wsize * Wsize.is_wsize
  5. | Coq_is_Ox86MULX_hi of Wsize.wsize * Wsize.is_wsize
  6. | Coq_is_Ox86SLHinit
  7. | Coq_is_Ox86SLHupdate
  8. | Coq_is_Ox86SLHmove
  9. | Coq_is_Ox86SLHprotect of Wsize.reg_kind * Wsize.is_reg_kind * Wsize.wsize * Wsize.is_wsize
val is_x86_extra_op_rect : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (Wsize.reg_kind -> Wsize.is_reg_kind -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> x86_extra_op -> is_x86_extra_op -> 'a1
val is_x86_extra_op_rec : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (Wsize.reg_kind -> Wsize.is_reg_kind -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> x86_extra_op -> is_x86_extra_op -> 'a1
val x86_extra_op_tag : x86_extra_op -> BinNums.positive
val is_x86_extra_op_inhab : x86_extra_op -> is_x86_extra_op
val is_x86_extra_op_functor : x86_extra_op -> is_x86_extra_op -> is_x86_extra_op
type box_x86_extra_op_Oset0 = Wsize.wsize
val coq_Box_x86_extra_op_Oset0_0 : box_x86_extra_op_Oset0 -> Wsize.wsize
type box_x86_extra_op_Oconcat128 =
  1. | Box_x86_extra_op_Oconcat128
type box_x86_extra_op_Ox86SLHprotect = {
  1. coq_Box_x86_extra_op_Ox86SLHprotect_0 : Wsize.reg_kind;
  2. coq_Box_x86_extra_op_Ox86SLHprotect_1 : Wsize.wsize;
}
val coq_Box_x86_extra_op_Ox86SLHprotect_0 : box_x86_extra_op_Ox86SLHprotect -> Wsize.reg_kind
val coq_Box_x86_extra_op_Ox86SLHprotect_1 : box_x86_extra_op_Ox86SLHprotect -> Wsize.wsize
type x86_extra_op_fields_t = __
val x86_extra_op_fields : x86_extra_op -> x86_extra_op_fields_t
val x86_extra_op_construct : BinNums.positive -> x86_extra_op_fields_t -> x86_extra_op option
val x86_extra_op_induction : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> (Wsize.reg_kind -> Wsize.is_reg_kind -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> x86_extra_op -> is_x86_extra_op -> 'a1
val x86_extra_op_eqb_fields : (x86_extra_op -> x86_extra_op -> bool) -> BinNums.positive -> x86_extra_op_fields_t -> x86_extra_op_fields_t -> bool
val x86_extra_op_eqb : x86_extra_op -> x86_extra_op -> bool
val x86_extra_op_eqb_OK : x86_extra_op -> x86_extra_op -> Bool.reflect
val x86_extra_op_eqb_OK_sumbool : x86_extra_op -> x86_extra_op -> bool
val coq_HB_unnamed_factory_1 : x86_extra_op Eqtype.Coq_hasDecEq.axioms_
val x86_extra_x86_extra_op__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_Oconcat128_instr : Sopn.instruction_desc
val coq_Ox86MOVZX32_instr : Sopn.instruction_desc
val coq_Ox86SLHinit_str : string
val coq_Ox86SLHinit_instr : Sopn.instruction_desc
val coq_Ox86SLHupdate_str : string
val coq_Ox86SLHupdate_instr : Sopn.instruction_desc
val coq_Ox86SLHmove_str : string
val coq_Ox86SLHmove_instr : Sopn.instruction_desc
val coq_Ox86SLHprotect_str : string
val prim_string : (string * x86_extra_op Sopn.prim_constructor) list
val re8_0 : Fexpr.rexpr
val re8_1 : Fexpr.rexpr
val eqC_x86_extra_op : x86_extra_op Utils0.eqTypeC