diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-28 22:52:13 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-28 22:52:13 +0200 |
| commit | f0de7ba427c47b8274d9b748a72c468ef32cec38 (patch) | |
| tree | d24968d8596c99612629fdb7ac7681cd70869067 | |
| parent | 44f346554115278ec9409bdcb9bc8ee32f4017db (diff) | |
| download | compcert-kvx-f0de7ba427c47b8274d9b748a72c468ef32cec38.tar.gz compcert-kvx-f0de7ba427c47b8274d9b748a72c468ef32cec38.zip | |
fix stacklayout for velus
| -rw-r--r-- | riscV/Stacklayout.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/Stacklayout.v b/riscV/Stacklayout.v index d0c6a526..369cda2b 100644 --- a/riscV/Stacklayout.v +++ b/riscV/Stacklayout.v @@ -59,7 +59,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. intros; simpl. set (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). |