diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-11 11:57:02 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-11 11:57:02 +0000 |
commit | bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc (patch) | |
tree | 3efa5cb51e9bb3edc935f42dbd630fce9a170804 /driver | |
parent | cd2449aabe7b259b0fdb8aaa2af65c2b8957ab32 (diff) | |
download | compcert-bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc.tar.gz compcert-bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc.zip |
- Added alignment constraints to memory loads and stores.
- In Cminor and below, removed pointer validity check in semantics of
comparisons, so that evaluation of expressions is independent of
memory state.
- In Cminor and below, removed "alloc" instruction.
- Cleaned up commented-away parts.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Complements.v | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/driver/Complements.v b/driver/Complements.v index fc2fa533..938c4888 100644 --- a/driver/Complements.v +++ b/driver/Complements.v @@ -240,26 +240,6 @@ Qed. (** ** Determinism for terminating executions. *) -(* -Lemma star_star_inv: - forall ge s t1 s1, star step ge s t1 s1 -> - forall t2 s2 w w1 w2, star step ge s t2 s2 -> - possible_trace w t1 w1 -> possible_trace w t2 w2 -> - exists t, (star step ge s1 t s2 /\ t2 = t1 ** t) - \/ (star step ge s2 t s1 /\ t1 = t2 ** t). -Proof. - induction 1; intros. - exists t2; left; split; auto. - inv H2. exists (t1 ** t2); right; split. econstructor; eauto. auto. - possibleTraceInv. - exploit step_deterministic. eexact H. eexact H5. eauto. eauto. - intros [U [V W]]. subst s5 t3 w3. - exploit IHstar; eauto. intros [t [ [Q R] | [Q R] ]]. - subst t4. exists t; left; split. auto. traceEq. - subst t2. exists t; right; split. auto. traceEq. -Qed. -*) - Lemma steps_deterministic: forall ge s0 t1 s1, star step ge s0 t1 s1 -> forall r1 r2 t2 s2 w0 w1 w2, star step ge s0 t2 s2 -> |