From 0dc38cb379acab43066f93cb7f617a6f34bbd2c3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Jul 2018 19:15:04 +0200
Subject: [PATCH] wp_alloc: test more patterns

---
 tests/heap_lang.ref | 20 ++++++++++++++++++++
 tests/heap_lang.v   |  8 ++++++++
 2 files changed, 28 insertions(+)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 1e739c094..b4ac2c10a 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -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
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index e863bf9b6..dd4a53e4e 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -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.
-- 
GitLab