From 51e8bc524d570439f868ec0bdbf718cb53ca7669 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 30 Dec 2013 16:37:05 +0000
Subject: Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty
 struct/union). __builtin_memcpy_aligned now supports the case sz = 0.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2392 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/CSEproof.v      |  1 -
 backend/ValueAnalysis.v |  3 ---
 backend/ValueDomain.v   | 10 ++++------
 3 files changed, 4 insertions(+), 10 deletions(-)

(limited to 'backend')

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 6c9331a..317fb82 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -1135,7 +1135,6 @@ Proof.
     inv SOUND. eapply add_memcpy_holds; eauto. 
     eapply kill_loads_after_storebytes_holds; eauto. 
     eapply Mem.loadbytes_length; eauto. 
-    omega. 
     simpl. apply Ple_refl. 
   + apply CASE2; inv H0; auto.
   + apply CASE2; inv H0; auto.
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 396d8d4..0709f5d 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -1271,9 +1271,6 @@ Proof.
   eapply Mem.loadbytes_length; eauto. 
   intros. eapply loadbytes_sound; eauto. apply match_aptr_of_aval; auto. 
   eapply romatch_storebytes; eauto. 
-  exploit Mem.loadbytes_length; eauto. 
-  intros. exploit (nat_of_Z_eq sz). omega. rewrite <- H1; intros. 
-  destruct bytes. simpl in H2. omegaContradiction. congruence.
   eapply sound_stack_storebytes; eauto. 
 + (* annot *)
   intros (A & B); subst. 
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index 2c728d3..5d0e3ae 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -2727,16 +2727,14 @@ Qed.
 Lemma romatch_storebytes:
   forall m b ofs bytes m' rm,
   Mem.storebytes m b ofs bytes = Some m' ->
-  bytes <> nil ->
   romatch m rm ->
   romatch m' rm.
 Proof.
-  intros; red; intros. exploit H1; eauto. intros (A & B & C). split; auto. split.
+  intros; red; intros. exploit H0; eauto. intros (A & B & C). split; auto. split.
 - apply bmatch_inv with m; auto.
-  intros. eapply Mem.loadbytes_storebytes_other; eauto. 
-  left. red; intros; subst b0. elim (C ofs). apply Mem.perm_cur_max.
-  eapply Mem.storebytes_range_perm; eauto. 
-  destruct bytes. congruence. simpl length. rewrite inj_S. omega.
+  intros. eapply Mem.loadbytes_storebytes_disjoint; eauto. 
+  destruct (eq_block b0 b); auto. subst b0. right; red; unfold Intv.In; simpl; red; intros.
+  elim (C x). apply Mem.perm_cur_max. eapply Mem.storebytes_range_perm; eauto.
 - intros; red; intros; elim (C ofs0). eauto with mem.
 Qed.
 
-- 
cgit v1.2.3