Commit f1b53440 authored by Dan Frumin's avatar Dan Frumin

Working on memcpy

parent ba09905d
......@@ -101,7 +101,19 @@ Section memcpy.
(* Ouch, this goal is ugly. We either need to embed naturals into the
reified syntax, or let the binop evaluator be total and generate
side-conditions (here 0 ≤ n) for the result to be well-formed. *)
Admitted.
rewrite cloc_of_to_val /=. case_option_guard; last first.
{ exfalso. omega. } simpl.
iExists (cloc_to_val (cloc_plus p n)). rewrite Nat2Z.id.
iSplit; eauto.
vcg_continue. rewrite !cloc_plus_0 Qp_half_half.
iIntros "Hqq Hpp".
iPoseProof (memcpy_body_spec with "Hp Hq Hpp Hqq") as "H"; [done|done|].
iApply (awp_wand with "H").
iIntros (v) "[Hp Hq]". vcg_continue.
repeat vcg_continue. (* TODO WTF?? *)
eauto with iFrame.
Qed.
End memcpy.
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