Arm_params (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.Arm

val arm_mov_ofs : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.lval ->
  Expr.assgn_tag ->
  Stack_alloc_params.mov_kind ->
  Expr.pexpr ->
  Expr.pexpr ->
  (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
    Expr.instr_r
    option

val arm_immediate : 
  (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 ->
  Arm_extra.arm_extended_op Expr.instr_r

val arm_swap : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.assgn_tag ->
  Expr.var_i ->
  Expr.var_i ->
  Expr.var_i ->
  Expr.var_i ->
  (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
    Expr.instr_r

val arm_saparams : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  (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
    Stack_alloc_params.stack_alloc_params

val arm_allocate_stack_frame : 
  (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 option ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr list)
    list

val arm_free_stack_frame : 
  (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 option ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr list)
    list

val arm_set_up_sp_register : 
  (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 ->
  Wsize.wsize ->
  Expr.var_i ->
  Expr.var_i ->
  ((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 list)
    list

val arm_tmp : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Ident.Ident.ident

val arm_tmp2 : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Ident.Ident.ident

val arm_lmove : 
  (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 list

val arm_check_ws : Eqtype.Equality.sort -> bool

val arm_lstore : 
  (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 ->
  Expr.var_i ->
  (Fexpr.lexpr list * Arm_extra.arm_extended_op Sopn.sopn) * Fexpr.rexpr list

val arm_lload : 
  (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

val arm_liparams : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  (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
    Linearization.linearization_params

val arm_fvars_correct : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.progT ->
  (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
    Expr.fun_decl
    list ->
  bool

val arm_loparams : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  ((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,
    Arm_lowering.lowering_options)
    Arch_params.lowering_params

val arm_shparams : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  (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
    Slh_lowering.sh_params

val condt_of_rflag : Arm_decl.rflag -> Arm_decl.condt

val condt_not : Arm_decl.condt -> Arm_decl.condt

val condt_and : Arm_decl.condt -> Arm_decl.condt -> Arm_decl.condt option

val condt_or : Arm_decl.condt -> Arm_decl.condt -> Arm_decl.condt option

val is_rflags_GE : Arm_decl.rflag -> Arm_decl.rflag -> bool

val assemble_cond : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.instr_info ->
  Fexpr.fexpr ->
  Arm_decl.condt Compiler_util.cexec

val is_valid_address : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_decl.reg_address ->
  bool

val arm_agparams : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  (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)
    Asm_gen.asm_gen_params

val arm_szparams : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  (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
    Stack_zeroization.stack_zeroization_params

val arm_is_move_op : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  (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.asm_op_t ->
  bool

val arm_params : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  (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,
    Arm_lowering.lowering_options)
    Arch_params.architecture_params