- 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, 6 insertions, 4 deletions

diff --git a/arm/linux/Stacklayout.v b/arm/linux/Stacklayout.v
index 4521114f..d84da6ba 100644
--- a/arm/linux/Stacklayout.v
+++ b/arm/linux/Stacklayout.v
@@ -109,7 +109,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))
   /\ (8 | fe.(fe_size)).
 Proof.
   intros.
@@ -128,13 +128,15 @@ 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.
+  assert (4 | x6).
+    apply Zdivides_trans with 8. exists 2; auto. auto.
   set (x7 := x6 + 4).
   assert (4 | x7). unfold x7; apply Zdivide_plus_r; auto. exists 1; auto.
   set (x8 := x7 + 4).
-  assert (4 | x8). unfold x8; apply Zdivide_plus_r; auto. exists 1; auto.
+  assert (8 | x8). unfold x8, x7. replace (x6 + 4 + 4) with (x6 + 8) by omega.
+    apply Zdivide_plus_r; auto. exists 1; auto.
   set (x9 := align (x8 + bound_stack_data b) 8).
   assert (8 | x9). unfold x9; apply align_divides. omega.
   tauto.