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

1 files changed, 15 insertions, 18 deletions

diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 2b409ab9..ec4780e2 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -251,10 +251,10 @@ Fixpoint sizeof (t: type) : Z :=
   | Tfloat F32 _ => 4
   | Tfloat F64 _ => 8
   | Tpointer _ _ => 4
-  | Tarray t' n _ => sizeof t' * Zmax 1 n
+  | Tarray t' n _ => sizeof t' * Zmax 0 n
   | Tfunction _ _ _ => 1
-  | Tstruct _ fld _ => align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
-  | Tunion _ fld _ => align (Zmax 1 (sizeof_union fld)) (alignof t)
+  | Tstruct _ fld _ => align (sizeof_struct fld 0) (alignof t)
+  | Tunion _ fld _ => align (sizeof_union fld) (alignof t)
   | Tcomp_ptr _ _ => 4
   end
 
@@ -271,25 +271,23 @@ with sizeof_union (fld: fieldlist) : Z :=
   end.
 
 Lemma sizeof_pos:
-  forall t, sizeof t > 0.
+  forall t, sizeof t >= 0
+with sizeof_struct_incr:
+  forall fld pos, pos <= sizeof_struct fld pos.
 Proof.
-Local Opaque alignof.
-  assert (X: forall n t, n > 0 -> align n (alignof t) > 0).
+- Local Opaque alignof.
+  assert (X: forall n t, n >= 0 -> align n (alignof t) >= 0).
   {
     intros. generalize (align_le n (alignof t) (alignof_pos t)). omega.
   }
   induction t; simpl; try xomega.
   destruct i; omega.
   destruct f; omega.
-  apply Zmult_gt_0_compat. auto. xomega.
-  apply X. xomega. 
-  apply X. xomega.
-Qed.
-
-Lemma sizeof_struct_incr:
-  forall fld pos, pos <= sizeof_struct fld pos.
-Proof.
-  induction fld; intros; simpl. omega. 
+  change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega. 
+  apply X. apply Zle_ge. apply sizeof_struct_incr. 
+  apply X. induction f; simpl; xomega.
+- induction fld; intros; simpl.
+  omega. 
   eapply Zle_trans. 2: apply IHfld.
   apply Zle_trans with (align pos (alignof t)). 
   apply align_le. apply alignof_pos.
@@ -318,9 +316,9 @@ Local Transparent alignof.
 - rewrite H; apply Zdivide_refl.
 - destruct H. rewrite H. apply Z.divide_mul_l; auto. 
 - apply Zdivide_refl.
-- change (alignof (Tstruct i f a) | align (Z.max 1 (sizeof_struct f 0)) (alignof (Tstruct i f a))).
+- change (alignof (Tstruct i f a) | align (sizeof_struct f 0) (alignof (Tstruct i f a))).
   apply align_divides. apply alignof_pos.
-- change (alignof (Tunion i f a) | align (Z.max 1 (sizeof_union f)) (alignof (Tunion i f a))).
+- change (alignof (Tunion i f a) | align (sizeof_union f) (alignof (Tunion i f a))).
   apply align_divides. apply alignof_pos.
 - rewrite H; apply Zdivide_refl.
 Qed.
@@ -376,7 +374,6 @@ Proof.
   split. auto.
 Local Opaque alignof. 
   simpl. eapply Zle_trans; eauto. 
-  apply Zle_trans with (Z.max 1 (sizeof_struct fld 0)). xomega. 
   apply align_le. apply alignof_pos. 
 Qed.