Jasmin.Merge_varmapsmodule E : sig ... endval writefun_ra :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.t ->
(Var0.funname -> Var0.SvExtra.Sv.t) ->
Var0.funname ->
Var0.SvExtra.Sv.tval writefun_ra_call :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.t ->
(Var0.funname -> Var0.SvExtra.Sv.t) ->
Var0.funname ->
Var0.SvExtra.Sv.tval write_I_rec :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.t ->
(Var0.funname -> Var0.SvExtra.Sv.t) ->
Var0.SvExtra.Sv.t ->
'a1 Expr.instr ->
Var0.SvExtra.Sv.tval write_c_rec :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.t ->
(Var0.funname -> Var0.SvExtra.Sv.t) ->
Var0.SvExtra.Sv.t ->
'a1 Expr.instr list ->
Var0.SvExtra.Sv.tval write_c :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.t ->
(Var0.funname -> Var0.SvExtra.Sv.t) ->
'a1 Expr.instr list ->
Var0.SvExtra.Sv.tval write_fd :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.t ->
(Var0.funname -> Var0.SvExtra.Sv.t) ->
'a1 Expr.sfundef ->
Var0.SvExtra.Sv.tval get_wmap : Var0.SvExtra.Sv.t Var0.Mf.t -> Var0.funname -> Var0.SvExtra.Sv.tval mk_wmap :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.t ->
Var0.SvExtra.Sv.t Var0.Mf.tval check_wmap :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.t ->
Var0.SvExtra.Sv.t Var0.Mf.t ->
boolval check_fv :
Expr.instr_info ->
Var0.SvExtra.Sv.t ->
Var0.SvExtra.Sv.t ->
(Compiler_util.pp_error_loc, unit) Utils0.resultval check_e :
Expr.instr_info ->
Var0.SvExtra.Sv.t ->
Expr.pexpr ->
(Compiler_util.pp_error_loc, unit) Utils0.resultval check_es :
Expr.instr_info ->
Var0.SvExtra.Sv.t ->
Expr.pexpr list ->
(Compiler_util.pp_error_loc, unit) Utils0.resultval check_c :
'a1 Sopn.asmOp ->
(Var0.SvExtra.Sv.t ->
'a1 Expr.instr ->
Var0.SvExtra.Sv.t Compiler_util.cexec) ->
Var0.SvExtra.Sv.t ->
'a1 Expr.instr list ->
(Compiler_util.pp_error_loc, Var0.SvExtra.Sv.t) Utils0.resultval wloop :
'a1 Sopn.asmOp ->
(Var0.SvExtra.Sv.t ->
'a1 Expr.instr ->
Var0.SvExtra.Sv.t Compiler_util.cexec) ->
Expr.instr_info ->
'a1 Expr.instr list ->
Var0.SvExtra.Sv.t ->
'a1 Expr.instr list ->
Datatypes.nat ->
Var0.SvExtra.Sv.t ->
(Compiler_util.pp_error_loc, Var0.SvExtra.Sv.t) Utils0.resultval check_lv :
Expr.instr_info ->
Var0.SvExtra.Sv.t ->
Expr.lval ->
(Compiler_util.pp_error_loc, Var0.SvExtra.Sv.t) Utils0.resultval check_lvs :
Expr.instr_info ->
Var0.SvExtra.Sv.t ->
Expr.lval list ->
(Compiler_util.pp_error_loc, Var0.SvExtra.Sv.t) Utils0.resultval check_i :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.t ->
(Var0.funname -> Var0.SvExtra.Sv.t) ->
Wsize.wsize ->
Var0.SvExtra.Sv.t ->
'a1 Expr.instr ->
Var0.SvExtra.Sv.t Compiler_util.cexecval check_fd :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.t ->
(Var0.funname -> Var0.SvExtra.Sv.t) ->
Var0.funname ->
'a1 Expr.sfundef ->
(Compiler_util.pp_error_loc, unit) Utils0.resultval check_prog :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.t ->
(Var0.funname -> Var0.SvExtra.Sv.t) ->
(Compiler_util.pp_error_loc, (Var0.funname * unit) list) Utils0.resultval check :
Wsize.coq_PointerData ->
'a1 Sopn.asmOp ->
One_varmap.one_varmap_info ->
'a1 Expr.sprog ->
Var0.SvExtra.Sv.t ->
(Compiler_util.pp_error_loc, unit) Utils0.result