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/One_varmap/index.html
Module Jasmin.One_varmap
type one_varmap_info = {syscall_sig : (Wsize.wsize * BinNums.positive) Syscall_t.syscall_t -> ovm_syscall_sig_t;all_vars : Var0.SvExtra.Sv.t;callee_saved : Var0.SvExtra.Sv.t;vflags : Var0.SvExtra.Sv.t;
}val syscall_kill : one_varmap_info -> Var0.SvExtra.Sv.tval magic_variables :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.tval savedstackreg : Expr.saved_stack -> Var0.SvExtra.Sv.tval saved_stack_vm :
'a1 Sopn.asmOp ->
('a1, Expr.stk_fun_extra) Expr._fundef ->
Var0.SvExtra.Sv.tval ra_vm :
one_varmap_info ->
Expr.stk_fun_extra ->
Var0.SvExtra.Sv.t ->
Var0.SvExtra.Sv.tval ra_vm_return : Expr.stk_fun_extra -> Var0.SvExtra.Sv.tval ra_undef :
'a1 Sopn.asmOp ->
one_varmap_info ->
('a1, Expr.stk_fun_extra) Expr._fundef ->
Var0.SvExtra.Sv.t ->
Var0.SvExtra.Sv.tval tmp_call : Expr.stk_fun_extra -> Var0.SvExtra.Sv.tval fd_tmp_call :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
'a1 Expr.sprog ->
Var0.funname ->
Var0.SvExtra.Sv.t