diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-04-27 21:14:07 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-04-27 21:14:07 +0200 |
| commit | 350ef360f0875b687a7e14edb6cb6d4556e7ae0a (patch) | |
| tree | bd8aa866c8b0e9dc5f1f4f7e34ab2798a7e195a3 | |
| parent | 800760b1d98cfc14e771d7adae0ee5f675e56bdb (diff) | |
| parent | 44a32019dae027a5ed7795c6048a39be43c3158a (diff) | |
| download | compcert-kvx-patched_for_velus.tar.gz compcert-kvx-patched_for_velus.zip | |
Merge branch 'kvx-work-velus' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into HEADpatched_for_velus
| -rw-r--r-- | backend/Stackingproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index d8505369..0a2a25e4 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1088,7 +1088,7 @@ 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. - try change 4 with (size_chunk Mptr) in SEP. + try 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. |