From 800760b1d98cfc14e771d7adae0ee5f675e56bdb Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 27 Apr 2021 21:13:02 +0200 Subject: fix 4 --- backend/Stackingproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index bb75b920..d8505369 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. - 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. -- cgit