diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-04-27 18:41:22 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-04-27 18:41:22 +0200 |
| commit | fe3b2e16814ec8265a39f429ec606b1174659a97 (patch) | |
| tree | 7d43dbeabe369e40773f378a7212137a76c02161 | |
| parent | d1439cc7bad4cd1a4d90211d17ca677484372896 (diff) | |
| download | compcert-kvx-fe3b2e16814ec8265a39f429ec606b1174659a97.tar.gz compcert-kvx-fe3b2e16814ec8265a39f429ec606b1174659a97.zip | |
fix pour ARM
| -rw-r--r-- | backend/Stackingproof.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index ed3eef04..bb75b920 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1088,7 +1088,8 @@ Local Opaque b fe. apply (frame_env_separated b) in SEP. replace (make_env b) with fe in SEP by auto. (* Store of parent *) rewrite sep_swap3 in SEP. - apply range_contains in SEP;[|apply perm_F_any|tauto]. + change 4 with (size_chunk Mptr) in SEP. + apply range_contains in SEP; [|apply perm_F_any|tauto]. exploit (contains_set_stack (fun v' => v' = parent) parent (fun _ => True) m2' Tptr). rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto. clear SEP; intros (m3' & STORE_PARENT & SEP). |