diff options
| author | Timothy Bourke <tim@tbrk.org> | 2017-04-05 15:02:50 +0200 |
|---|---|---|
| committer | Lionel Rieg <lionel.rieg@univ-grenoble-alpes.fr> | 2020-04-21 01:08:58 +0200 |
| commit | a3cf22317821f9f32e632344d51834a9a1524701 (patch) | |
| tree | a4f5f35015a530852e112ee92b3e1a59dc55e3a0 | |
| parent | d87ea150694745a1efee967285ee68845ac66f05 (diff) | |
| download | compcert-kvx-a3cf22317821f9f32e632344d51834a9a1524701.tar.gz compcert-kvx-a3cf22317821f9f32e632344d51834a9a1524701.zip | |
Fix other stacking proofs for range'
| -rw-r--r-- | arm/Stacklayout.v | 2 | ||||
| -rw-r--r-- | powerpc/Stacklayout.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/arm/Stacklayout.v b/arm/Stacklayout.v index 462d83ad..8e91f14b 100644 --- a/arm/Stacklayout.v +++ b/arm/Stacklayout.v @@ -64,7 +64,7 @@ Lemma frame_env_separated: ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) ** P. Proof. -Local Opaque Z.add Z.mul sepconj range. +Local Opaque Z.add Z.mul sepconj range'. intros; simpl. set (olink := 4 * b.(bound_outgoing)); set (ora := olink + 4); diff --git a/powerpc/Stacklayout.v b/powerpc/Stacklayout.v index cb3806bd..d5539b70 100644 --- a/powerpc/Stacklayout.v +++ b/powerpc/Stacklayout.v @@ -68,7 +68,7 @@ Lemma frame_env_separated: ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) ** P. Proof. -Local Opaque Z.add Z.mul sepconj range. +Local Opaque Z.add Z.mul sepconj range'. intros; simpl. set (ol := align (8 + 4 * b.(bound_outgoing)) 8). set (ora := ol + 4 * b.(bound_local)). |