From 0013d8531e896e2e791816ff7f972f95bd7f940f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Nov 2018 09:10:33 +0100
Subject: [PATCH] Fix bug in `wp_cas_suc`.

This closes issue #220.
---
 tests/heap_lang.v              | 5 +++++
 theories/heap_lang/proofmode.v | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index f00723e45..082649a8d 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -78,6 +78,11 @@ Section tests.
   Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, ⌜ w = #true ⌝ }})%I.
   Proof. wp_lam. wp_op. by case_bool_decide. Qed.
 
+  Definition heap_e7 : val := λ: "v", CAS "v" #0 #1.
+
+  Lemma heap_e7_spec l : l ↦ #0 -∗ WP heap_e7 #l [{_,  l ↦ #1 }].
+  Proof. iIntros. wp_lam. wp_cas_suc. auto. Qed.
+
   Definition FindPred : val :=
     rec: "pred" "x" "y" :=
       let: "yp" := "y" + #1 in
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 6baede50e..90e561f2f 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -511,7 +511,7 @@ Tactic Notation "wp_cas_suc" :=
     |try congruence
     |try fast_done (* vals_cas_compare_safe *)
     |simpl; try wp_value_head]
-  | |- envs_entails _ (twp ?E ?e ?Q) =>
+  | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_suc _ _ _ _ _ K))
       |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
-- 
GitLab