From 7811619480dd2f20143ceca34cde0068b7964c36 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 20 May 2020 14:34:51 +0200
Subject: [PATCH] test wp_free

---
 tests/heap_lang.v | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 90ad0e2c2..efed8387e 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -218,6 +218,18 @@ Section tests.
     iIntros "[$ _]". (* splits the fraction, not the app *)
   Qed.
 
+
+  Lemma test_wp_free l v :
+    {{{ l ↦ v }}} Free #l {{{ RET #(); True }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ". wp_free. iApply "HΦ". done.
+  Qed.
+
+  Lemma test_twp_free l v :
+    [[{ l ↦ v }]] Free #l [[{ RET #(); True }]].
+  Proof.
+    iIntros (Φ) "Hl HΦ". wp_free. iApply "HΦ". done.
+  Qed.
 End tests.
 
 Section inv_mapsto_tests.
-- 
GitLab