From b63ace0a0668f842dc178b0ad991babe0eb559e8 Mon Sep 17 00:00:00 2001 From: alxest Date: Tue, 9 Jul 2019 14:33:22 +0900 Subject: [PATCH] Fix --- demo/DemoTarget.v | 2 +- demo/mutrec/MutrecA.v | 2 +- demo/mutrec/MutrecB.v | 6 +- demo/mutrec/MutrecHeader.v | 2 +- demo/mutrec/a.v | 381 ------------------------------------- demo/mutrec/b.v | 1 - proof/Preservation.v | 6 +- 7 files changed, 10 insertions(+), 390 deletions(-) delete mode 100644 demo/mutrec/a.v delete mode 100644 demo/mutrec/b.v diff --git a/demo/DemoTarget.v b/demo/DemoTarget.v index dc7bf780..9a37efd9 100644 --- a/demo/DemoTarget.v +++ b/demo/DemoTarget.v @@ -27,7 +27,7 @@ Definition code: list instruction := ]. Definition func: function := - mkfunction (Some (mksignature [Tlong] (Some Tfloat) cc_default)) code + mkfunction (mksignature [Tlong] (Some Tfloat) cc_default true) code . Definition prog: program := mkprogram [(func_id, (Gfun (Internal func)))] [func_id ; main_id] main_id. diff --git a/demo/mutrec/MutrecA.v b/demo/mutrec/MutrecA.v index 3ca53127..72b00d2b 100644 --- a/demo/mutrec/MutrecA.v +++ b/demo/mutrec/MutrecA.v @@ -57,7 +57,7 @@ Definition composites : list composite_definition := nil. Definition global_definitions : list (ident * globdef fundef type) := ((g_id, Gfun(External (EF_external "g" - (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default)) + (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default true)) (Tcons tint Tnil) tint cc_default)) :: (_memoized, Gvar v_memoized) :: (f_id, Gfun(Internal func_f)) :: nil). diff --git a/demo/mutrec/MutrecB.v b/demo/mutrec/MutrecB.v index c17cc4e8..aa25a1ec 100644 --- a/demo/mutrec/MutrecB.v +++ b/demo/mutrec/MutrecB.v @@ -49,7 +49,7 @@ Definition code: list instruction := Pleal RDI (Addrmode (Some RBX) None (inl (- 1))); (* leal -1(%ebx), %edi *) - Pcall_s f_id (mksignature [Tint] (Some Tint) cc_default); + Pcall_s f_id (mksignature [Tint] (Some Tint) cc_default true); (* call f *) Pleal RAX (Addrmode (Some RAX) (Some (RBX, 1)) (inl 0)); @@ -77,13 +77,13 @@ Definition code: list instruction := ]. Definition func_g: function := - mkfunction (Some (mksignature [Tint] (Some Tint) cc_default)) code + mkfunction (mksignature [Tint] (Some Tint) cc_default true) code . Definition global_definitions : list (ident * globdef fundef unit) := ((f_id, Gfun(External (EF_external "f" - (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default)))) :: (_memoized, Gvar v_memoized) :: + (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default true)))) :: (_memoized, Gvar v_memoized) :: (g_id, Gfun(Internal func_g)) :: nil). Definition public_idents : list ident := diff --git a/demo/mutrec/MutrecHeader.v b/demo/mutrec/MutrecHeader.v index 75cb1446..27b8f610 100644 --- a/demo/mutrec/MutrecHeader.v +++ b/demo/mutrec/MutrecHeader.v @@ -91,5 +91,5 @@ Qed. Require AST. -Definition fg_sig: AST.signature := (AST.mksignature [AST.Tint] (Some AST.Tint) AST.cc_default). +Definition fg_sig: AST.signature := (AST.mksignature [AST.Tint] (Some AST.Tint) AST.cc_default true). diff --git a/demo/mutrec/a.v b/demo/mutrec/a.v deleted file mode 100644 index 7f020016..00000000 --- a/demo/mutrec/a.v +++ /dev/null @@ -1,381 +0,0 @@ -From Coq Require Import String List ZArith. -From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs. -Local Open Scope Z_scope. - -Module Info. - Definition version := "3.5"%string. - Definition build_number := ""%string. - Definition build_tag := ""%string. - Definition arch := "x86"%string. - Definition model := "64"%string. - Definition abi := "standard"%string. - Definition bitsize := 64. - Definition big_endian := false. - Definition source_file := "a.c"%string. - Definition normalized := false. -End Info. - -Definition ___builtin_ais_annot : ident := 1%positive. -Definition ___builtin_annot : ident := 8%positive. -Definition ___builtin_annot_intval : ident := 9%positive. -Definition ___builtin_bswap : ident := 2%positive. -Definition ___builtin_bswap16 : ident := 4%positive. -Definition ___builtin_bswap32 : ident := 3%positive. -Definition ___builtin_bswap64 : ident := 34%positive. -Definition ___builtin_clz : ident := 35%positive. -Definition ___builtin_clzl : ident := 36%positive. -Definition ___builtin_clzll : ident := 37%positive. -Definition ___builtin_ctz : ident := 38%positive. -Definition ___builtin_ctzl : ident := 39%positive. -Definition ___builtin_ctzll : ident := 40%positive. -Definition ___builtin_debug : ident := 52%positive. -Definition ___builtin_fabs : ident := 5%positive. -Definition ___builtin_fmadd : ident := 43%positive. -Definition ___builtin_fmax : ident := 41%positive. -Definition ___builtin_fmin : ident := 42%positive. -Definition ___builtin_fmsub : ident := 44%positive. -Definition ___builtin_fnmadd : ident := 45%positive. -Definition ___builtin_fnmsub : ident := 46%positive. -Definition ___builtin_fsqrt : ident := 6%positive. -Definition ___builtin_membar : ident := 10%positive. -Definition ___builtin_memcpy_aligned : ident := 7%positive. -Definition ___builtin_nop : ident := 51%positive. -Definition ___builtin_read16_reversed : ident := 47%positive. -Definition ___builtin_read32_reversed : ident := 48%positive. -Definition ___builtin_va_arg : ident := 12%positive. -Definition ___builtin_va_copy : ident := 13%positive. -Definition ___builtin_va_end : ident := 14%positive. -Definition ___builtin_va_start : ident := 11%positive. -Definition ___builtin_write16_reversed : ident := 49%positive. -Definition ___builtin_write32_reversed : ident := 50%positive. -Definition ___compcert_i64_dtos : ident := 19%positive. -Definition ___compcert_i64_dtou : ident := 20%positive. -Definition ___compcert_i64_sar : ident := 31%positive. -Definition ___compcert_i64_sdiv : ident := 25%positive. -Definition ___compcert_i64_shl : ident := 29%positive. -Definition ___compcert_i64_shr : ident := 30%positive. -Definition ___compcert_i64_smod : ident := 27%positive. -Definition ___compcert_i64_smulh : ident := 32%positive. -Definition ___compcert_i64_stod : ident := 21%positive. -Definition ___compcert_i64_stof : ident := 23%positive. -Definition ___compcert_i64_udiv : ident := 26%positive. -Definition ___compcert_i64_umod : ident := 28%positive. -Definition ___compcert_i64_umulh : ident := 33%positive. -Definition ___compcert_i64_utod : ident := 22%positive. -Definition ___compcert_i64_utof : ident := 24%positive. -Definition ___compcert_va_composite : ident := 18%positive. -Definition ___compcert_va_float64 : ident := 17%positive. -Definition ___compcert_va_int32 : ident := 15%positive. -Definition ___compcert_va_int64 : ident := 16%positive. -Definition _f : ident := 55%positive. -Definition _g : ident := 53%positive. -Definition _main : ident := 56%positive. -Definition _x : ident := 54%positive. -Definition _t'1 : ident := 57%positive. - -Definition f_f := {| - fn_return := tint; - fn_callconv := cc_default; - fn_params := ((_x, tint) :: nil); - fn_vars := nil; - fn_temps := ((_t'1, tint) :: nil); - fn_body := -(Ssequence - (Sifthenelse (Ebinop Oeq (Etempvar _x tint) (Econst_int (Int.repr 0) tint) - tint) - (Sreturn (Some (Econst_int (Int.repr 0) tint))) - Sskip) - (Ssequence - (Scall (Some _t'1) - (Evar _g (Tfunction (Tcons tint Tnil) tint cc_default)) - ((Ebinop Osub (Etempvar _x tint) (Econst_int (Int.repr 1) tint) tint) :: - nil)) - (Sreturn (Some (Ebinop Osub - (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _x tint) - tint) (Econst_int (Int.repr 1) tint) tint))))) -|}. - -Definition composites : list composite_definition := -nil. - -Definition global_definitions : list (ident * globdef fundef type) := -((___builtin_ais_annot, - Gfun(External (EF_builtin "__builtin_ais_annot" - (mksignature (AST.Tlong :: nil) None - {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) - (Tcons (tptr tschar) Tnil) tvoid - {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) :: - (___builtin_bswap, - Gfun(External (EF_builtin "__builtin_bswap" - (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default)) - (Tcons tuint Tnil) tuint cc_default)) :: - (___builtin_bswap32, - Gfun(External (EF_builtin "__builtin_bswap32" - (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default)) - (Tcons tuint Tnil) tuint cc_default)) :: - (___builtin_bswap16, - Gfun(External (EF_builtin "__builtin_bswap16" - (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default)) - (Tcons tushort Tnil) tushort cc_default)) :: - (___builtin_fabs, - Gfun(External (EF_builtin "__builtin_fabs" - (mksignature (AST.Tfloat :: nil) (Some AST.Tfloat) - cc_default)) (Tcons tdouble Tnil) tdouble cc_default)) :: - (___builtin_fsqrt, - Gfun(External (EF_builtin "__builtin_fsqrt" - (mksignature (AST.Tfloat :: nil) (Some AST.Tfloat) - cc_default)) (Tcons tdouble Tnil) tdouble cc_default)) :: - (___builtin_memcpy_aligned, - Gfun(External (EF_builtin "__builtin_memcpy_aligned" - (mksignature - (AST.Tlong :: AST.Tlong :: AST.Tlong :: AST.Tlong :: - nil) None cc_default)) - (Tcons (tptr tvoid) - (Tcons (tptr tvoid) (Tcons tulong (Tcons tulong Tnil)))) tvoid - cc_default)) :: - (___builtin_annot, - Gfun(External (EF_builtin "__builtin_annot" - (mksignature (AST.Tlong :: nil) None - {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) - (Tcons (tptr tschar) Tnil) tvoid - {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) :: - (___builtin_annot_intval, - Gfun(External (EF_builtin "__builtin_annot_intval" - (mksignature (AST.Tlong :: AST.Tint :: nil) - (Some AST.Tint) cc_default)) - (Tcons (tptr tschar) (Tcons tint Tnil)) tint cc_default)) :: - (___builtin_membar, - Gfun(External (EF_builtin "__builtin_membar" - (mksignature nil None cc_default)) Tnil tvoid cc_default)) :: - (___builtin_va_start, - Gfun(External (EF_builtin "__builtin_va_start" - (mksignature (AST.Tlong :: nil) None cc_default)) - (Tcons (tptr tvoid) Tnil) tvoid cc_default)) :: - (___builtin_va_arg, - Gfun(External (EF_builtin "__builtin_va_arg" - (mksignature (AST.Tlong :: AST.Tint :: nil) None - cc_default)) (Tcons (tptr tvoid) (Tcons tuint Tnil)) - tvoid cc_default)) :: - (___builtin_va_copy, - Gfun(External (EF_builtin "__builtin_va_copy" - (mksignature (AST.Tlong :: AST.Tlong :: nil) None - cc_default)) - (Tcons (tptr tvoid) (Tcons (tptr tvoid) Tnil)) tvoid cc_default)) :: - (___builtin_va_end, - Gfun(External (EF_builtin "__builtin_va_end" - (mksignature (AST.Tlong :: nil) None cc_default)) - (Tcons (tptr tvoid) Tnil) tvoid cc_default)) :: - (___compcert_va_int32, - Gfun(External (EF_external "__compcert_va_int32" - (mksignature (AST.Tlong :: nil) (Some AST.Tint) - cc_default)) (Tcons (tptr tvoid) Tnil) tuint - cc_default)) :: - (___compcert_va_int64, - Gfun(External (EF_external "__compcert_va_int64" - (mksignature (AST.Tlong :: nil) (Some AST.Tlong) - cc_default)) (Tcons (tptr tvoid) Tnil) tulong - cc_default)) :: - (___compcert_va_float64, - Gfun(External (EF_external "__compcert_va_float64" - (mksignature (AST.Tlong :: nil) (Some AST.Tfloat) - cc_default)) (Tcons (tptr tvoid) Tnil) tdouble - cc_default)) :: - (___compcert_va_composite, - Gfun(External (EF_external "__compcert_va_composite" - (mksignature (AST.Tlong :: AST.Tlong :: nil) - (Some AST.Tlong) cc_default)) - (Tcons (tptr tvoid) (Tcons tulong Tnil)) (tptr tvoid) cc_default)) :: - (___compcert_i64_dtos, - Gfun(External (EF_runtime "__compcert_i64_dtos" - (mksignature (AST.Tfloat :: nil) (Some AST.Tlong) - cc_default)) (Tcons tdouble Tnil) tlong cc_default)) :: - (___compcert_i64_dtou, - Gfun(External (EF_runtime "__compcert_i64_dtou" - (mksignature (AST.Tfloat :: nil) (Some AST.Tlong) - cc_default)) (Tcons tdouble Tnil) tulong cc_default)) :: - (___compcert_i64_stod, - Gfun(External (EF_runtime "__compcert_i64_stod" - (mksignature (AST.Tlong :: nil) (Some AST.Tfloat) - cc_default)) (Tcons tlong Tnil) tdouble cc_default)) :: - (___compcert_i64_utod, - Gfun(External (EF_runtime "__compcert_i64_utod" - (mksignature (AST.Tlong :: nil) (Some AST.Tfloat) - cc_default)) (Tcons tulong Tnil) tdouble cc_default)) :: - (___compcert_i64_stof, - Gfun(External (EF_runtime "__compcert_i64_stof" - (mksignature (AST.Tlong :: nil) (Some AST.Tsingle) - cc_default)) (Tcons tlong Tnil) tfloat cc_default)) :: - (___compcert_i64_utof, - Gfun(External (EF_runtime "__compcert_i64_utof" - (mksignature (AST.Tlong :: nil) (Some AST.Tsingle) - cc_default)) (Tcons tulong Tnil) tfloat cc_default)) :: - (___compcert_i64_sdiv, - Gfun(External (EF_runtime "__compcert_i64_sdiv" - (mksignature (AST.Tlong :: AST.Tlong :: nil) - (Some AST.Tlong) cc_default)) - (Tcons tlong (Tcons tlong Tnil)) tlong cc_default)) :: - (___compcert_i64_udiv, - Gfun(External (EF_runtime "__compcert_i64_udiv" - (mksignature (AST.Tlong :: AST.Tlong :: nil) - (Some AST.Tlong) cc_default)) - (Tcons tulong (Tcons tulong Tnil)) tulong cc_default)) :: - (___compcert_i64_smod, - Gfun(External (EF_runtime "__compcert_i64_smod" - (mksignature (AST.Tlong :: AST.Tlong :: nil) - (Some AST.Tlong) cc_default)) - (Tcons tlong (Tcons tlong Tnil)) tlong cc_default)) :: - (___compcert_i64_umod, - Gfun(External (EF_runtime "__compcert_i64_umod" - (mksignature (AST.Tlong :: AST.Tlong :: nil) - (Some AST.Tlong) cc_default)) - (Tcons tulong (Tcons tulong Tnil)) tulong cc_default)) :: - (___compcert_i64_shl, - Gfun(External (EF_runtime "__compcert_i64_shl" - (mksignature (AST.Tlong :: AST.Tint :: nil) - (Some AST.Tlong) cc_default)) - (Tcons tlong (Tcons tint Tnil)) tlong cc_default)) :: - (___compcert_i64_shr, - Gfun(External (EF_runtime "__compcert_i64_shr" - (mksignature (AST.Tlong :: AST.Tint :: nil) - (Some AST.Tlong) cc_default)) - (Tcons tulong (Tcons tint Tnil)) tulong cc_default)) :: - (___compcert_i64_sar, - Gfun(External (EF_runtime "__compcert_i64_sar" - (mksignature (AST.Tlong :: AST.Tint :: nil) - (Some AST.Tlong) cc_default)) - (Tcons tlong (Tcons tint Tnil)) tlong cc_default)) :: - (___compcert_i64_smulh, - Gfun(External (EF_runtime "__compcert_i64_smulh" - (mksignature (AST.Tlong :: AST.Tlong :: nil) - (Some AST.Tlong) cc_default)) - (Tcons tlong (Tcons tlong Tnil)) tlong cc_default)) :: - (___compcert_i64_umulh, - Gfun(External (EF_runtime "__compcert_i64_umulh" - (mksignature (AST.Tlong :: AST.Tlong :: nil) - (Some AST.Tlong) cc_default)) - (Tcons tulong (Tcons tulong Tnil)) tulong cc_default)) :: - (___builtin_bswap64, - Gfun(External (EF_builtin "__builtin_bswap64" - (mksignature (AST.Tlong :: nil) (Some AST.Tlong) - cc_default)) (Tcons tulong Tnil) tulong cc_default)) :: - (___builtin_clz, - Gfun(External (EF_builtin "__builtin_clz" - (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default)) - (Tcons tuint Tnil) tint cc_default)) :: - (___builtin_clzl, - Gfun(External (EF_builtin "__builtin_clzl" - (mksignature (AST.Tlong :: nil) (Some AST.Tint) - cc_default)) (Tcons tulong Tnil) tint cc_default)) :: - (___builtin_clzll, - Gfun(External (EF_builtin "__builtin_clzll" - (mksignature (AST.Tlong :: nil) (Some AST.Tint) - cc_default)) (Tcons tulong Tnil) tint cc_default)) :: - (___builtin_ctz, - Gfun(External (EF_builtin "__builtin_ctz" - (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default)) - (Tcons tuint Tnil) tint cc_default)) :: - (___builtin_ctzl, - Gfun(External (EF_builtin "__builtin_ctzl" - (mksignature (AST.Tlong :: nil) (Some AST.Tint) - cc_default)) (Tcons tulong Tnil) tint cc_default)) :: - (___builtin_ctzll, - Gfun(External (EF_builtin "__builtin_ctzll" - (mksignature (AST.Tlong :: nil) (Some AST.Tint) - cc_default)) (Tcons tulong Tnil) tint cc_default)) :: - (___builtin_fmax, - Gfun(External (EF_builtin "__builtin_fmax" - (mksignature (AST.Tfloat :: AST.Tfloat :: nil) - (Some AST.Tfloat) cc_default)) - (Tcons tdouble (Tcons tdouble Tnil)) tdouble cc_default)) :: - (___builtin_fmin, - Gfun(External (EF_builtin "__builtin_fmin" - (mksignature (AST.Tfloat :: AST.Tfloat :: nil) - (Some AST.Tfloat) cc_default)) - (Tcons tdouble (Tcons tdouble Tnil)) tdouble cc_default)) :: - (___builtin_fmadd, - Gfun(External (EF_builtin "__builtin_fmadd" - (mksignature - (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) - (Some AST.Tfloat) cc_default)) - (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble - cc_default)) :: - (___builtin_fmsub, - Gfun(External (EF_builtin "__builtin_fmsub" - (mksignature - (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) - (Some AST.Tfloat) cc_default)) - (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble - cc_default)) :: - (___builtin_fnmadd, - Gfun(External (EF_builtin "__builtin_fnmadd" - (mksignature - (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) - (Some AST.Tfloat) cc_default)) - (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble - cc_default)) :: - (___builtin_fnmsub, - Gfun(External (EF_builtin "__builtin_fnmsub" - (mksignature - (AST.Tfloat :: AST.Tfloat :: AST.Tfloat :: nil) - (Some AST.Tfloat) cc_default)) - (Tcons tdouble (Tcons tdouble (Tcons tdouble Tnil))) tdouble - cc_default)) :: - (___builtin_read16_reversed, - Gfun(External (EF_builtin "__builtin_read16_reversed" - (mksignature (AST.Tlong :: nil) (Some AST.Tint) - cc_default)) (Tcons (tptr tushort) Tnil) tushort - cc_default)) :: - (___builtin_read32_reversed, - Gfun(External (EF_builtin "__builtin_read32_reversed" - (mksignature (AST.Tlong :: nil) (Some AST.Tint) - cc_default)) (Tcons (tptr tuint) Tnil) tuint - cc_default)) :: - (___builtin_write16_reversed, - Gfun(External (EF_builtin "__builtin_write16_reversed" - (mksignature (AST.Tlong :: AST.Tint :: nil) None - cc_default)) (Tcons (tptr tushort) (Tcons tushort Tnil)) - tvoid cc_default)) :: - (___builtin_write32_reversed, - Gfun(External (EF_builtin "__builtin_write32_reversed" - (mksignature (AST.Tlong :: AST.Tint :: nil) None - cc_default)) (Tcons (tptr tuint) (Tcons tuint Tnil)) - tvoid cc_default)) :: - (___builtin_nop, - Gfun(External (EF_builtin "__builtin_nop" - (mksignature nil None cc_default)) Tnil tvoid cc_default)) :: - (___builtin_debug, - Gfun(External (EF_external "__builtin_debug" - (mksignature (AST.Tint :: nil) None - {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) - (Tcons tint Tnil) tvoid - {|cc_vararg:=true; cc_unproto:=false; cc_structret:=false|})) :: - (_g, - Gfun(External (EF_external "g" - (mksignature (AST.Tint :: nil) (Some AST.Tint) cc_default)) - (Tcons tint Tnil) tint cc_default)) :: (_f, Gfun(Internal f_f)) :: nil). - -Definition public_idents : list ident := -(_f :: _g :: ___builtin_debug :: ___builtin_nop :: - ___builtin_write32_reversed :: ___builtin_write16_reversed :: - ___builtin_read32_reversed :: ___builtin_read16_reversed :: - ___builtin_fnmsub :: ___builtin_fnmadd :: ___builtin_fmsub :: - ___builtin_fmadd :: ___builtin_fmin :: ___builtin_fmax :: - ___builtin_ctzll :: ___builtin_ctzl :: ___builtin_ctz :: ___builtin_clzll :: - ___builtin_clzl :: ___builtin_clz :: ___builtin_bswap64 :: - ___compcert_i64_umulh :: ___compcert_i64_smulh :: ___compcert_i64_sar :: - ___compcert_i64_shr :: ___compcert_i64_shl :: ___compcert_i64_umod :: - ___compcert_i64_smod :: ___compcert_i64_udiv :: ___compcert_i64_sdiv :: - ___compcert_i64_utof :: ___compcert_i64_stof :: ___compcert_i64_utod :: - ___compcert_i64_stod :: ___compcert_i64_dtou :: ___compcert_i64_dtos :: - ___compcert_va_composite :: ___compcert_va_float64 :: - ___compcert_va_int64 :: ___compcert_va_int32 :: ___builtin_va_end :: - ___builtin_va_copy :: ___builtin_va_arg :: ___builtin_va_start :: - ___builtin_membar :: ___builtin_annot_intval :: ___builtin_annot :: - ___builtin_memcpy_aligned :: ___builtin_fsqrt :: ___builtin_fabs :: - ___builtin_bswap16 :: ___builtin_bswap32 :: ___builtin_bswap :: - ___builtin_ais_annot :: nil). - -Definition prog : Clight.program := - mkprogram composites global_definitions public_idents _main Logic.I. - - diff --git a/demo/mutrec/b.v b/demo/mutrec/b.v deleted file mode 100644 index 8b137891..00000000 --- a/demo/mutrec/b.v +++ /dev/null @@ -1 +0,0 @@ - diff --git a/proof/Preservation.v b/proof/Preservation.v index d7289d38..55cd3e27 100644 --- a/proof/Preservation.v +++ b/proof/Preservation.v @@ -673,9 +673,11 @@ Proof. - inv INIT. rr. esplits; eauto. + refl. - inv STEP. ss. inv SUST. des. exploit Sound.system_axiom; try apply EXTCALL; eauto. - { instantiate (1:= Args.Cstyle _ _ _). ss. esplits; eauto. } + { instantiate (1:= Args.Cstyle _ _ _). ss. } + { rr. esplits; eauto. } { eapply Sound.system_skenv; eauto. eapply Sound.skenv_mle; eauto. } - i; des. r in RETV. des. ss. esplits; eauto. + { eauto. } + i; des. r in RETV. ss. des. ss. esplits; eauto. + etrans; eauto. + eapply Sound.skenv_mle; eauto. etrans; eauto. - inv FINAL. ss. des. esplits; eauto.