val x86_op_align :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Wsize.wsize ->
Wsize.wsize ->
(Fexpr.lexpr list
* (X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Sopn.sopn)
* Fexpr.rexpr listval lea_ptr :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.lval ->
Expr.pexpr ->
Expr.assgn_tag ->
Expr.pexpr ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Expr.instr_rval x86_mov_ofs :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.lval ->
Expr.assgn_tag ->
Stack_alloc_params.mov_kind ->
Expr.pexpr ->
Expr.pexpr ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Expr.instr_r
optionval x86_saparams :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Stack_alloc_params.stack_alloc_paramsval x86_set_up_sp_register :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
BinNums.coq_Z ->
Wsize.wsize ->
Expr.var_i ->
Expr.var_i ->
((Fexpr.lexpr list
* (X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Sopn.sopn)
* Fexpr.rexpr list)
listval x86_liparams :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Linearization.linearization_paramsval x86_loparams :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
((X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op,
X86_lowering.lowering_options)
Arch_params.lowering_paramsval x86_sh_lower :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
Expr.lval list ->
Slh_ops.slh_op ->
Expr.pexpr list ->
((Expr.lval list
* (X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Sopn.sopn)
* Expr.pexpr list)
optionval x86_shparams :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Slh_lowering.sh_paramsval x86_agparams :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Asm_gen.asm_gen_paramsval x86_szparams :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Stack_zeroization.stack_zeroization_paramsval x86_is_move_op :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op)
Arch_extra.extended_op
Sopn.asm_op_t ->
boolval x86_params :
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt)
Arch_extra.arch_toIdent ->
(X86_decl.register,
X86_decl.register_ext,
X86_decl.xmm_register,
X86_decl.rflag,
X86_decl.condt,
X86_instr_decl.x86_op,
X86_extra.x86_extra_op,
X86_lowering.lowering_options)
Arch_params.architecture_params