(** Testing function calls and CWP resources *) From iris_c.vcgen Require Import proofmode. Section tests_vcg. Context `{cmonadG Σ}. Definition c_id : val := λ: "v", c_ret "v". Lemma test_invoke_1 (l: cloc) R : l ↦C #42 -∗ CWP callᶜ (c_ret c_id) (∗ᶜ ♯ₗl) @ R {{ v, ⌜v = #42⌝ ∗ l ↦C #42 }}%I. Proof. iIntros "Hl". vcg. iIntros "Hl !> $ !>". cwp_lam. vcg. iIntros "Hl". vcg_continue. eauto. Qed. Definition plus_pair : val := λ: "vv", "v1" ←ᶜ c_ret (Fst "vv");ᶜ "v2" ←ᶜ c_ret (Snd "vv");ᶜ (c_ret "v1") +ᶜ (c_ret "v2"). Lemma test_invoke_2 R : CWP callᶜ (c_ret plus_pair) (♯21 |||ᶜ ♯21) @ R {{ v, ⌜v = #42⌝ }}%I. Proof. iIntros. vcg. iIntros "!> $ !>". cwp_lam. vcg. by vcg_continue. Qed. Lemma test_invoke_3 (l : cloc) R : l ↦C #21 -∗ CWP callᶜ (c_ret plus_pair) (∗ᶜ ♯ₗl |||ᶜ ∗ᶜ ♯ₗl) @ R {{ v, ⌜v = #42⌝ ∗ l ↦C #21 }}%I. Proof. iIntros. vcg. iIntros "Hl !> $ !>". cwp_lam. vcg. iIntros "Hl". vcg_continue; eauto. Qed. End tests_vcg.