From 1f9c5efcdf73380bcedf32cc4aedd38fe3d03576 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 8 Jan 2020 13:05:16 +0100
Subject: [PATCH] add test for iAuIntro errors (status quo)

---
 tests/atomic.ref | 11 +++++++++++
 tests/atomic.v   | 17 +++++++++++++++++
 2 files changed, 28 insertions(+)

diff --git a/tests/atomic.ref b/tests/atomic.ref
index 6184f371c..7146b97ea 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -12,6 +12,17 @@
   AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
        << l ↦{q} v0, COMM Q -∗ Q >>
   
+"non_laterable"
+     : string
+The command has indeed failed with message:
+Tactic failure: iAuIntro: not all spatial assumptions are laterable.
+The command has indeed failed with message:
+Tactic failure: wp_apply: cannot apply
+(<<< ∀ (v : val) (q : Qp), ?Goal ↦{q} v >>>
+   ! #?Goal @ ⊤
+ <<< ?Goal ↦{q} v, RET v >>>).
+"printing"
+     : string
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/atomic.v b/tests/atomic.v
index 6e3b57077..4e69316d0 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -17,7 +17,24 @@ Section tests.
   Qed.
 End tests.
 
+(* Test if we get reasonable error messages with non-laterable assertions in the context. *)
+Section error.
+  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
+  Import atomic_heap.notation.
+
+  Check "non_laterable".
+  Lemma non_laterable (P : iProp Σ) (l : loc) :
+    P -∗ WP !#l {{ _, True }}.
+  Proof.
+    iIntros "HP". wp_apply load_spec. Fail iAuIntro.
+  Restart.
+    iIntros "HP". Fail awp_apply load_spec.
+  Abort.
+End error.  
+
+
 (* Test if AWP and the AU obtained from AWP print. *)
+Check "printing".
 Section printing.
   Context `{!heapG Σ}.
 
-- 
GitLab