Module Riscv_params_common.RISCVFopn
val to_opn :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
((Fexpr.lexpr list
* (Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t')
* Fexpr.rexpr list) ->
(Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr listval mov :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
(Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr listval add :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
Expr.var_i ->
(Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr listval sub :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
Expr.var_i ->
(Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr listval li :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr listval addi :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr listval subi :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr listval andi :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr listval align :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
Wsize.wsize ->
(Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr listval smart_addi :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
((Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr list)
listval smart_subi :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
((Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr list)
listval smart_addi_tmp :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
((Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr list)
listval smart_subi_tmp :
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
((Fexpr.lexpr list
* ((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_t',
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
Riscv_extra.riscv_extra_op)
Arch_extra.extra_op_t)
Arch_extra.extended_op_gen
Sopn.sopn)
* Fexpr.rexpr list)
list