Jasmin.Stack_zeroizationmodule E : sig ... endtype 'asm_op stack_zeroization_params =
Stack_zero_strategy.stack_zero_strategy ->
Ident.Ident.ident ->
Label.label ->
Wsize.wsize ->
Wsize.wsize ->
BinNums.coq_Z ->
('asm_op Linear.lcmd * Var0.SvExtra.Sv.t) Compiler_util.cexecval stack_zeroization_lfd_body :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 stack_zeroization_params ->
Ident.Ident.ident ->
'a1 Linear.lfundef ->
Stack_zero_strategy.stack_zero_strategy ->
Wsize.wsize ->
'a1 Linear.lfundef Compiler_util.cexecval stack_zeroization_lfd :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 stack_zeroization_params ->
(Var0.funname ->
(Stack_zero_strategy.stack_zero_strategy * Wsize.wsize) option) ->
Ident.Ident.ident ->
Var0.funname ->
'a1 Linear.lfundef ->
'a1 Linear.lfundef Compiler_util.cexecval stack_zeroization_lprog :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 stack_zeroization_params ->
(Var0.funname ->
(Stack_zero_strategy.stack_zero_strategy * Wsize.wsize) option) ->
'a1 Linear.lprog ->
'a1 Linear.lprog Compiler_util.cexec