From 8539759095f95f2fbb680efc7633d868099114c8 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 29 Dec 2012 16:55:38 +0000
Subject: Merge of the clightgen branch: - Alternate semantics for Clight where
 function parameters are temporaries,   not variables - New pass SimplLocals
 that turns non-addressed local variables into   temporaries - Simplified
 Csharpminor, Cshmgen and Cminorgen accordingly - SimplExpr starts its
 temporaries above variable names, therefoe   Cminorgen no longer needs to
 encode variable names and temps names. - Simplified Cminor parser & printer,
 as well as Errors, accordingly. - New tool clightgen to produce Clight AST in
 Coq-parsable .v files. - Removed side condition "return type is void" on
 rules skip_seq   in the semantics of CompCert C, Clight, C#minor, Cminor. -
 Adapted RTLgenproof accordingly (now uses a memory extension).

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2083 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/ClightBigstep.v | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'cfrontend/ClightBigstep.v')

diff --git a/cfrontend/ClightBigstep.v b/cfrontend/ClightBigstep.v
index 7603b6b2..293ea5df 100644
--- a/cfrontend/ClightBigstep.v
+++ b/cfrontend/ClightBigstep.v
@@ -299,14 +299,14 @@ Lemma exec_stmt_eval_funcall_steps:
   (forall e le m s t le' m' out,
    exec_stmt ge e le m s t le' m' out ->
    forall f k, exists S,
-   star step ge (State f s k e le m) t S
+   star step1 ge (State f s k e le m) t S
    /\ outcome_state_match e le' m' f k out S)
 /\
   (forall m fd args t m' res,
    eval_funcall ge m fd args t m' res ->
    forall k,
    is_call_cont k ->
-   star step ge (Callstate fd args k m) t (Returnstate res k m')).
+   star step1 ge (Callstate fd args k m) t (Returnstate res k m')).
 Proof.
   apply exec_stmt_funcall_ind; intros.
 
@@ -450,7 +450,7 @@ Proof.
 
 (* call internal *)
   destruct (H3 f k) as [S1 [A1 B1]].
-  eapply star_left. eapply step_internal_function; eauto.
+  eapply star_left. eapply step_internal_function; eauto. econstructor; eauto.
   eapply star_right. eexact A1. 
    inv B1; simpl in H4; try contradiction.
   (* Out_normal *)
@@ -477,7 +477,7 @@ Lemma exec_stmt_steps:
    forall e le m s t le' m' out,
    exec_stmt ge e le m s t le' m' out ->
    forall f k, exists S,
-   star step ge (State f s k e le m) t S
+   star step1 ge (State f s k e le m) t S
    /\ outcome_state_match e le' m' f k out S.
 Proof (proj1 exec_stmt_eval_funcall_steps).
 
@@ -486,7 +486,7 @@ Lemma eval_funcall_steps:
    eval_funcall ge m fd args t m' res ->
    forall k,
    is_call_cont k ->
-   star step ge (Callstate fd args k m) t (Returnstate res k m').
+   star step1 ge (Callstate fd args k m) t (Returnstate res k m').
 Proof (proj2 exec_stmt_eval_funcall_steps).
 
 Definition order (x y: unit) := False.
@@ -494,12 +494,12 @@ Definition order (x y: unit) := False.
 Lemma evalinf_funcall_forever:
   forall m fd args T k,
   evalinf_funcall ge m fd args T ->
-  forever_N step order ge tt (Callstate fd args k m) T.
+  forever_N step1 order ge tt (Callstate fd args k m) T.
 Proof.
   cofix CIH_FUN.
   assert (forall e le m s T f k,
           execinf_stmt ge e le m s T ->
-          forever_N step order ge tt (State f s k e le m) T).
+          forever_N step1 order ge tt (State f s k e le m) T).
   cofix CIH_STMT.
   intros. inv H.
 
@@ -558,13 +558,13 @@ Proof.
 (* call internal *)
   intros. inv H0.
   eapply forever_N_plus.
-  eapply plus_one. econstructor; eauto. 
+  eapply plus_one. econstructor; eauto. econstructor; eauto.
   apply H; eauto.
   traceEq.
 Qed.
 
 Theorem bigstep_semantics_sound:
-  bigstep_sound (bigstep_semantics prog) (semantics prog).
+  bigstep_sound (bigstep_semantics prog) (semantics1 prog).
 Proof.
   constructor; simpl; intros.
 (* termination *)
-- 
cgit