From 00166237ccce1c74578ad338ddd492a6fa60d074 Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 2 Feb 2021 09:46:13 -0600
Subject: [PATCH] Add tests for wp_load and wp_store failures

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

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 776a2e02e..e27e60ad6 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -68,6 +68,26 @@
   --------------------------------------∗
   |={⊤}=> l ↦ #1
   
+"wp_load_fail"
+     : string
+The command has indeed failed with message:
+Tactic failure: wp_load: cannot find 'Load' in (Fork Skip).
+The command has indeed failed with message:
+Tactic failure: wp_load: cannot find 'Load' in (Fork Skip).
+"wp_load_no_ptsto"
+     : string
+The command has indeed failed with message:
+Tactic failure: wp_load: cannot find l ↦ ?.
+"wp_store_fail"
+     : string
+The command has indeed failed with message:
+Tactic failure: wp_store: cannot find 'Store' in (Fork Skip).
+The command has indeed failed with message:
+Tactic failure: wp_store: cannot find 'Store' in (Fork Skip).
+"wp_store_no_ptsto"
+     : string
+The command has indeed failed with message:
+Tactic failure: wp_store: cannot find l ↦ ?.
 1 goal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 9b9310bf1..ef63f45f9 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -149,6 +149,30 @@ Section tests.
     ⊢ WP e + #0 [{ _, True }].
   Proof. wp_bind (e + #0)%E. Abort.
 
+  Check "wp_load_fail".
+  Lemma wp_load_fail :
+    ⊢ WP Fork Skip {{ _, True }}.
+  Proof. Fail wp_load. Abort.
+  Lemma wp_load_fail :
+    ⊢ WP Fork Skip [{ _, True }].
+  Proof. Fail wp_load. Abort.
+  Check "wp_load_no_ptsto".
+  Lemma wp_load_fail (l: loc) :
+    ⊢ WP ! #l {{ _, True }}.
+  Proof. Fail wp_load. Abort.
+
+  Check "wp_store_fail".
+  Lemma wp_store_fail :
+    ⊢ WP Fork Skip {{ _, True }}.
+  Proof. Fail wp_store. Abort.
+  Lemma wp_store_fail :
+    ⊢ WP Fork Skip [{ _, True }].
+  Proof. Fail wp_store. Abort.
+  Check "wp_store_no_ptsto".
+  Lemma wp_store_fail (l: loc) :
+    ⊢ WP #l <- #0 {{ _, True }}.
+  Proof. Fail wp_store. Abort.
+
   Lemma wp_apply_evar e P :
     P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
   Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
-- 
GitLab