diff options
Diffstat (limited to 'x86/Stacklayout.v')
| -rw-r--r-- | x86/Stacklayout.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/x86/Stacklayout.v b/x86/Stacklayout.v index 44fd43b2..22c68099 100644 --- a/x86/Stacklayout.v +++ b/x86/Stacklayout.v @@ -72,7 +72,7 @@ Local Opaque Z.add Z.mul sepconj range. assert (0 <= 4 * b.(bound_outgoing)) by omega. assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). assert (olink + w <= ocs) by (unfold ocs; omega). - assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). + assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega). @@ -88,13 +88,13 @@ Local Opaque Z.add Z.mul sepconj range. rewrite sep_swap34. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. - apply range_split_2. fold olink. omega. omega. + apply range_split_2. fold olink. omega. omega. apply range_split. omega. apply range_split_2. fold ol. omega. omega. apply range_drop_right with ostkdata. omega. rewrite sep_swap. apply range_drop_left with (ostkdata + bound_stack_data b). omega. - rewrite sep_swap. + rewrite sep_swap. exact H. Qed. @@ -115,11 +115,11 @@ Proof. assert (0 <= 4 * b.(bound_outgoing)) by omega. assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). assert (olink + w <= ocs) by (unfold ocs; omega). - assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). + assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega). - split. omega. omega. + split. omega. omega. Qed. Lemma frame_env_aligned: |