Remove_globals (p.jasmin.2026.03.0.doc.jasmin.jasmin.Jasmin.Remove

val type_of_glob_value : Global.glob_value -> Type.atype

module E : sig ... end

val check_data : Global.glob_value -> Global.glob_value -> bool

val check : Global.glob_value -> Global.glob_decl -> bool

val find_glob : 
  Expr.instr_info ->
  Expr.var_i ->
  Global.glob_decl list ->
  Global.glob_value ->
  (Compiler_util.pp_error_loc, Var0.Var.var) Utils0.result

val add_glob : 
  (Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident) ->
  Expr.instr_info ->
  Var0.Var.var ->
  Global.glob_decl list ->
  Global.glob_value ->
  (Compiler_util.pp_error_loc, Global.glob_decl list) Utils0.result

val evaluate_bytes : 
  Expr.instr_info ->
  Var0.Var.var ->
  Expr.pexpr list ->
  (Compiler_util.pp_error_loc, Values.values) Utils0.result

val array_from_cells : 
  Flag_combination.coq_FlagCombinationParams ->
  Expr.instr_info ->
  Var0.Var.var ->
  BinNums.positive ->
  Expr.pexpr list ->
  (Compiler_util.pp_error_loc, Warray_.WArray.array) Utils0.result

val extend_glob_i : 
  'a1 Sopn.asmOp ->
  (Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident) ->
  Flag_combination.coq_FlagCombinationParams ->
  'a1 Expr.instr ->
  Global.glob_decl list ->
  (Compiler_util.pp_error_loc, Global.glob_decl list) Utils0.result

val extend_glob_prog : 
  'a1 Sopn.asmOp ->
  (Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident) ->
  Flag_combination.coq_FlagCombinationParams ->
  'a1 Expr.uprog ->
  (Compiler_util.pp_error_loc, Global.glob_decl list) Utils0.result

val get_var_ : 
  Expr.instr_info ->
  Var0.Var.var Var0.Mvar.t ->
  Expr.gvar ->
  (Compiler_util.pp_error_loc, Expr.gvar) Utils0.result

val remove_glob_e : 
  Expr.instr_info ->
  Var0.Var.var Var0.Mvar.t ->
  Expr.pexpr ->
  (Compiler_util.pp_error_loc, Expr.pexpr) Utils0.result

val remove_glob_lv : 
  Expr.instr_info ->
  Var0.Var.var Var0.Mvar.t ->
  Expr.lval ->
  (Compiler_util.pp_error_loc, Expr.lval) Utils0.result

val remove_glob : 
  'a1 Sopn.asmOp ->
  (Var0.Var.var Var0.Mvar.t ->
    'a1 Expr.instr ->
    (Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list) Compiler_util.cexec) ->
  Var0.Var.var Var0.Mvar.t ->
  'a1 Expr.instr list ->
  (Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list) Compiler_util.cexec

val merge_glob : 
  Var0.Var.var ->
  Var0.Var.var option ->
  Var0.Var.var option ->
  Var0.Var.var option

val coq_Mincl : Var0.Var.var Var0.Mvar.t -> Var0.Var.var Var0.Mvar.t -> bool

val merge_env : 
  Var0.Var.var Var0.Mvar.t ->
  Var0.Var.var Var0.Mvar.t ->
  Var0.Var.var Var0.Mvar.t

val loop : 
  'a1 Sopn.asmOp ->
  (Var0.Var.var Var0.Mvar.t ->
    (Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list) Compiler_util.cexec) ->
  Datatypes.nat ->
  Var0.Var.var Var0.Mvar.t ->
  (Compiler_util.pp_error_loc, Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list)
    Utils0.result

type 'asm_op check2_r =

| Check2_r of Expr.pexpr * Var0.Var.var Var0.Mvar.t * 'asm_op Expr.instr list * Var0.Var.var Var0.Mvar.t * 'asm_op Expr.instr list

type 'asm_op loop2_r =

| Loop2_r of Expr.pexpr * 'asm_op Expr.instr list * 'asm_op Expr.instr list * Var0.Var.var Var0.Mvar.t

val loop2 : 
  'a1 Sopn.asmOp ->
  (Var0.Var.var Var0.Mvar.t -> 'a1 check2_r Compiler_util.cexec) ->
  Datatypes.nat ->
  Var0.Var.var Var0.Mvar.t ->
  (Compiler_util.pp_error_loc, 'a1 loop2_r) Utils0.result

val remove_glob_i : 
  'a1 Sopn.asmOp ->
  Flag_combination.coq_FlagCombinationParams ->
  Global.glob_decl list ->
  Var0.Var.var Var0.Mvar.t ->
  'a1 Expr.instr ->
  (Var0.Var.var Var0.Mvar.t * 'a1 Expr.instr list) Compiler_util.cexec

val remove_glob_fundef : 
  'a1 Sopn.asmOp ->
  Flag_combination.coq_FlagCombinationParams ->
  Global.glob_decl list ->
  'a1 Expr.ufundef ->
  (Compiler_util.pp_error_loc, ('a1, Expr.extra_fun_t) Expr._fundef)
    Utils0.result

val remove_glob_prog : 
  'a1 Sopn.asmOp ->
  (Global.glob_decl list -> Var0.Var.var -> Ident.Ident.ident) ->
  Flag_combination.coq_FlagCombinationParams ->
  'a1 Expr.uprog ->
  (Compiler_util.pp_error_loc,
    ('a1, Expr.extra_fun_t, Expr.extra_prog_t) Expr._prog)
    Utils0.result