Merge of branches/full-expr-4:

- Csyntax, Csem: source C language has side-effects within expressions,
  performs implicit casts, and has nondeterministic reduction semantics
  for expressions
- Cstrategy: deterministic red. sem. for the above
- Clight: the previous source C language, with pure expressions.
  Added: temporary variables + implicit casts.
- New pass SimplExpr to pull side-effects out of expressions
  (previously done in untrusted Caml code in cparser/)
- Csharpminor: added temporary variables to match Clight.
- Cminorgen: adapted, removed cast optimization (moved to back-end)
- CastOptim: RTL-level optimization of casts
- cparser: transformations Bitfields, StructByValue and StructAssign
  now work on non-simplified expressions
- Added pretty-printers for several intermediate languages,
  and matching -dxxx command-line flags.



git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 50 insertions, 0 deletions

diff --git a/common/Smallstep.v b/common/Smallstep.v
index cd61ec3..63426c1 100644
--- a/common/Smallstep.v
+++ b/common/Smallstep.v
@@ -66,6 +66,31 @@ Proof.
   intros. eapply star_step; eauto. apply star_refl. traceEq. 
 Qed.
 
+Lemma star_two:
+  forall ge s1 t1 s2 t2 s3 t,
+  step ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
+  star ge s1 t s3.
+Proof.
+  intros. eapply star_step; eauto. apply star_one; auto.  
+Qed.
+
+Lemma star_three:
+  forall ge s1 t1 s2 t2 s3 t3 s4 t,
+  step ge s1 t1 s2 -> step ge s2 t2 s3 -> step ge s3 t3 s4 -> t = t1 ** t2 ** t3 ->
+  star ge s1 t s4.
+Proof.
+  intros. eapply star_step; eauto. eapply star_two; eauto. 
+Qed.
+
+Lemma star_four:
+  forall ge s1 t1 s2 t2 s3 t3 s4 t4 s5 t,
+  step ge s1 t1 s2 -> step ge s2 t2 s3 ->
+  step ge s3 t3 s4 -> step ge s4 t4 s5 -> t = t1 ** t2 ** t3 ** t4 ->
+  star ge s1 t s5.
+Proof.
+  intros. eapply star_step; eauto. eapply star_three; eauto. 
+Qed.
+
 Lemma star_trans:
   forall ge s1 t1 s2, star ge s1 t1 s2 ->
   forall t2 s3 t, star ge s2 t2 s3 -> t = t1 ** t2 -> star ge s1 t s3.
@@ -103,6 +128,31 @@ Proof.
   intros. econstructor; eauto. apply star_refl. traceEq.
 Qed.
 
+Lemma plus_two:
+  forall ge s1 t1 s2 t2 s3 t,
+  step ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 ->
+  plus ge s1 t s3.
+Proof.
+  intros. eapply plus_left; eauto. apply star_one; auto.  
+Qed.
+
+Lemma plus_three:
+  forall ge s1 t1 s2 t2 s3 t3 s4 t,
+  step ge s1 t1 s2 -> step ge s2 t2 s3 -> step ge s3 t3 s4 -> t = t1 ** t2 ** t3 ->
+  plus ge s1 t s4.
+Proof.
+  intros. eapply plus_left; eauto. eapply star_two; eauto. 
+Qed.
+
+Lemma plus_four:
+  forall ge s1 t1 s2 t2 s3 t3 s4 t4 s5 t,
+  step ge s1 t1 s2 -> step ge s2 t2 s3 ->
+  step ge s3 t3 s4 -> step ge s4 t4 s5 -> t = t1 ** t2 ** t3 ** t4 ->
+  plus ge s1 t s5.
+Proof.
+  intros. eapply plus_left; eauto. eapply star_three; eauto. 
+Qed.
+
 Lemma plus_star:
   forall ge s1 t s2, plus ge s1 t s2 -> star ge s1 t s2.
 Proof.