From 43838a40fa29e76b7f71590f0b5739df88141813 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 29 Jun 2018 09:59:37 +0200
Subject: [PATCH] test 'not a CAS' error message as well

---
 tests/heap_lang.ref | 5 +++++
 tests/heap_lang.v   | 7 +++++++
 2 files changed, 12 insertions(+)

diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index ee03be85c..c02464537 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -73,3 +73,8 @@
 The command has indeed failed with message:
 Ltac call to "wp_cas_suc" failed.
 Tactic failure: wp_cas_suc: Values are not safe to compare for CAS.
+"not_cas"
+     : string
+The command has indeed failed with message:
+Ltac call to "wp_cas_suc" failed.
+Tactic failure: wp_cas_suc: cannot find 'CAS' in (#())%E.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 7efc06e02..eba3026da 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -170,6 +170,13 @@ Section error_tests.
   Proof.
     iIntros "H↦". Fail wp_cas_suc.
   Abort.
+
+  Check "not_cas".
+  Lemma not_cas :
+    (WP #() {{ _, True }})%I.
+  Proof.
+    Fail wp_cas_suc.
+  Abort.
 End error_tests.
 
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
-- 
GitLab