jasmin 2026.09.0 (latest) · OCaml Package

val sz_init : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (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.extended_op
    Linear.lcmd

val store_zero : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Expr.var_i ->
  BinNums.coq_Z ->
  (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.extended_op
    Linear.linstr_r

val sz_loop : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Label.label ->
  Wsize.wsize ->
  (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.extended_op
    Linear.lcmd

val restore_sp : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  ((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
    Linear.linstr
    list

val stack_zero_loop : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Label.label ->
  Wsize.wsize ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (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.extended_op
    Linear.lcmd

val stack_zero_loop_vars : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Var0.SvExtra.Sv.t

val sz_unrolled : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (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.extended_op
    Linear.lcmd

val stack_zero_unrolled : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (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.extended_op
    Linear.lcmd

val stack_zero_unrolled_vars : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Var0.SvExtra.Sv.t

val stack_zeroization_cmd : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Stack_zero_strategy.stack_zero_strategy ->
  Ident.Ident.ident ->
  Label.label ->
  Wsize.wsize ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  ((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.extended_op
     Linear.lcmd
   * Var0.SvExtra.Sv.t)
    Compiler_util.cexec

package jasmin

Module Jasmin.Riscv_stack_zeroization

Module `Jasmin.Riscv_stack_zeroization`