diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-28 20:44:24 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-28 20:44:24 +0200 |
| commit | c9e4b66c10f7abd432c47c3cb2a9579a814b4395 (patch) | |
| tree | c8550197e7afa585cf0d240405d9901a9110d728 | |
| parent | bf9ed342fdb0112cfefd895fb5c0f2cb43b9e74c (diff) | |
| download | compcert-kvx-c9e4b66c10f7abd432c47c3cb2a9579a814b4395.tar.gz compcert-kvx-c9e4b66c10f7abd432c47c3cb2a9579a814b4395.zip | |
applied the Velus patch
| -rw-r--r-- | backend/Stackingproof.v | 1 | ||||
| -rw-r--r-- | kvx/Stacklayout.v | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 1ede0194..49d2956e 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -139,6 +139,7 @@ Qed. (** * Memory assertions used to describe the contents of stack frames *) Local Opaque Z.add Z.mul Z.divide. +Local Hint Immediate perm_F_any : core. (** Accessing the stack frame using [load_stack] and [store_stack]. *) diff --git a/kvx/Stacklayout.v b/kvx/Stacklayout.v index 46202e03..740c0cf2 100644 --- a/kvx/Stacklayout.v +++ b/kvx/Stacklayout.v @@ -62,7 +62,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 (w := if Archi.ptr64 then 8 else 4). set (olink := align (4 * b.(bound_outgoing)) w). |