Commit 616906bb authored by Robbert Krebbers's avatar Robbert Krebbers

Rename memcpy -> array_copy.

parent d81ae4c4
From iris_c.vcgen Require Import proofmode. From iris_c.vcgen Require Import proofmode.
Definition memcpy : val := λᶜ "arg", Definition array_copy : val := λᶜ "arg",
"p" mut c_ret (Fst "arg"); "p" mut c_ret (Fst "arg");
"q" mut c_ret (Fst (Snd "arg")); "q" mut c_ret (Fst (Snd "arg"));
"n" ←ᶜ c_ret (Snd (Snd "arg")); "n" ←ᶜ c_ret (Snd (Snd "arg"));
...@@ -9,10 +9,10 @@ Definition memcpy : val := λᶜ "arg", ...@@ -9,10 +9,10 @@ Definition memcpy : val := λᶜ "arg",
(c_ret "p" += 1) = ∗ᶜ(c_ret "q" += 1) (c_ret "p" += 1) = ∗ᶜ(c_ret "q" += 1)
}. }.
Lemma memcpy_spec `{cmonadG Σ} lxs lys xs ys n R : Lemma array_copy_spec `{cmonadG Σ} lxs lys xs ys n R :
length xs = n length ys = n length xs = n length ys = n
lxs C xs - lys C ys - lxs C xs - lys C ys -
CWP memcpy (cloc_to_val lxs, (cloc_to_val lys, #n))%V @ R {{ _, lxs C ys lys C ys }}. CWP array_copy (cloc_to_val lxs, (cloc_to_val lys, #n))%V @ R {{ _, lxs C ys lys C ys }}.
Proof. Proof.
iIntros (Hlen <-) "**". iApply cwp_fun; simpl. vcg. iIntros (p q) "**". iIntros (Hlen <-) "**". iApply cwp_fun; simpl. vcg. iIntros (p q) "**".
iApply (cwp_wand _ (λ _, p' q', p C p' q C q' iApply (cwp_wand _ (λ _, p' q', p C p' q C q'
......
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