Commit 0dc38cb3 authored by Ralf Jung's avatar Ralf Jung

wp_alloc: test more patterns

parent 89bc9c1f
......@@ -30,6 +30,26 @@
WP let: "x" := #l in let: "y" := ref #1 in "x" <- ! "x" + #1;; ! "x"
@ E [{ v, ⌜v = #2⌝ }]
1 subgoal
Σ : gFunctors
H : heapG Σ
l : loc
============================
"Hl1" : l ↦{1 / 2} #0
"Hl2" : l ↦{1 / 2} #0
--------------------------------------∗
True
1 subgoal
Σ : gFunctors
H : heapG Σ
l : loc
============================
--------------------------------------∗
True
1 subgoal
Σ : gFunctors
......
......@@ -123,6 +123,14 @@ Section tests.
iIntros (?) "?". wp_cas as ? | ?. done. done.
Qed.
Lemma wp_alloc_split :
WP Alloc #0 {{ _, True }}%I.
Proof. wp_alloc l as "[Hl1 Hl2]". Show. done. Qed.
Lemma wp_alloc_drop :
WP Alloc #0 {{ _, True }}%I.
Proof. wp_alloc l as "_". Show. done. Qed.
End tests.
Section printing_tests.
......
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