Fix

snu-sf · Jul 9, 2019 · b63ace0 · b63ace0
1 parent 9c556da
commit b63ace0
Show file tree

Hide file tree

Showing 7 changed files with 10 additions and 390 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
diff --git a/demo/mutrec/b.v b/demo/mutrec/b.v
diff --git 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.
Original file line number	Diff line number	Diff line change
Expand Up		@@ -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).