- Revised non-overflow constraints on memory injections so that

  injections compose (Values, Memdata, Memory)
- Memory chunks: Mfloat64 now has alignment 8; introduced Mfloat64al32
  that works like old Mfloat64 (i.e. has alignment 4); simplified
  handling of memcpy builtin accordingly.


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

1 files changed, 2 insertions, 3 deletions

diff --git a/powerpc/eabi/Stacklayout.v b/powerpc/eabi/Stacklayout.v
index 22a2826..cd4d9ae 100644
--- a/powerpc/eabi/Stacklayout.v
+++ b/powerpc/eabi/Stacklayout.v
@@ -113,7 +113,7 @@ Remark frame_env_aligned:
   /\ (8 | fe.(fe_ofs_float_local))
   /\ (8 | fe.(fe_ofs_float_callee_save))
   /\ (4 | fe.(fe_ofs_retaddr))
-  /\ (4 | fe.(fe_stack_data))
+  /\ (8 | fe.(fe_stack_data))
   /\ (16 | fe.(fe_size)).
 Proof.
   intros.
@@ -133,8 +133,7 @@ Proof.
   set (x5 := x4 + 8 * bound_float_local b).
   assert (8 | x5). unfold x5. apply Zdivide_plus_r; auto. exists (bound_float_local b); ring.
   set (x6 := x5 + 8 * bound_float_callee_save b).
-  assert (4 | x6).
-    apply Zdivides_trans with 8. exists 2; auto.
+  assert (8 | x6).
     unfold x6. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring.
   set (x7 := align (x6 + bound_stack_data b) 16).
   assert (16 | x7). unfold x7; apply align_divides. omega.