diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-12-29 16:55:38 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-12-29 16:55:38 +0000 |
commit | 8539759095f95f2fbb680efc7633d868099114c8 (patch) | |
tree | 3401d7cd91686026090a21f600cf70ea4372ebf3 /cfrontend/ClightBigstep.v | |
parent | 7e9c6fc9a51adc5e488c590d83c1e8ef5a256c9f (diff) | |
download | compcert-8539759095f95f2fbb680efc7633d868099114c8.tar.gz compcert-8539759095f95f2fbb680efc7633d868099114c8.zip |
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
Diffstat (limited to 'cfrontend/ClightBigstep.v')
-rw-r--r-- | cfrontend/ClightBigstep.v | 18 |
1 files changed, 9 insertions, 9 deletions
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 *) |