package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa
doc/jasmin.jasmin/Jasmin/Arm_params_common/ARMFopn/index.html
Module Arm_params_common.ARMFopn
val to_opn :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
((Fexpr.lexpr list * Arm_instr_decl.arm_op) * Fexpr.rexpr list) ->
(Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr listval mov :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
(Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr listval sub :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
Expr.var_i ->
(Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr listval movi :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr listval addi :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr listval subi :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr listval bici :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr listval align :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
Wsize.wsize ->
(Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr listval li :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
BinNums.coq_Z ->
(Fexpr.lexpr list
* (Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt,
Arm_instr_decl.arm_op,
Arm_extra.arm_extra_op)
Arch_extra.extended_op
Sopn.sopn)
* Fexpr.rexpr listval smart_addi :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
((Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr list)
listval smart_subi :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
((Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr list)
listval smart_addi_tmp :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
((Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr list)
listval smart_subi_tmp :
(Arm_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arm_decl.rflag,
Arm_decl.condt)
Arch_extra.arch_toIdent ->
Expr.var_i ->
Expr.var_i ->
BinNums.coq_Z ->
((Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr list)
list