Jasmin.One_varmaptype one_varmap_info = {syscall_sig : 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