package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2026.03.0.tar.bz2
sha256=dec62a3cd0cd42cfe96ec64b3cd3961e0e8a09fb92ceb64175cffb54fde50e40
doc/jasmin.jasmin/Jasmin/Remove_globals/index.html
Module Jasmin.Remove_globals
val type_of_glob_value : Global.glob_value -> Type.atypemodule E : sig ... endval check_data : Global.glob_value -> Global.glob_value -> boolval check : Global.glob_value -> Global.glob_decl -> boolval find_glob :
Expr.instr_info ->
Expr.var_i ->
Global.glob_decl list ->
Global.glob_value ->
(Compiler_util.pp_error_loc, Var0.Var.var) Utils0.resultval 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.resultval evaluate_bytes :
Expr.instr_info ->
Var0.Var.var ->
Expr.pexpr list ->
(Compiler_util.pp_error_loc, Values.values) Utils0.resultval 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.resultval 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.resultval 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.resultval get_var_ :
Expr.instr_info ->
Var0.Var.var Var0.Mvar.t ->
Expr.gvar ->
(Compiler_util.pp_error_loc, Expr.gvar) Utils0.resultval remove_glob_e :
Expr.instr_info ->
Var0.Var.var Var0.Mvar.t ->
Expr.pexpr ->
(Compiler_util.pp_error_loc, Expr.pexpr) Utils0.resultval remove_glob_lv :
Expr.instr_info ->
Var0.Var.var Var0.Mvar.t ->
Expr.lval ->
(Compiler_util.pp_error_loc, Expr.lval) Utils0.resultval 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.cexecval merge_glob :
Var0.Var.var ->
Var0.Var.var option ->
Var0.Var.var option ->
Var0.Var.var optionval coq_Mincl : Var0.Var.var Var0.Mvar.t -> Var0.Var.var Var0.Mvar.t -> boolval merge_env :
Var0.Var.var Var0.Mvar.t ->
Var0.Var.var Var0.Mvar.t ->
Var0.Var.var Var0.Mvar.tval 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.resulttype '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.resultval 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.cexecval 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.resultval 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