Commit 350ef360 authored by David Monniaux's avatar David Monniaux
Browse files

Merge branch 'kvx-work-velus' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into HEAD

parents 800760b1 44a32019
Pipeline #65610 waiting for manual action with stage
......@@ -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.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment