From 85245d48b831b93eb09802a657f4601387be5094 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Dec 2017 20:09:21 +0100
Subject: [PATCH] Test case for fetch-and-add.

---
 theories/tests/heap_lang.v | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 6c6cb5072..b1a162b23 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -20,7 +20,7 @@ Section LiftingTests.
     end.
   Qed.
 
-  Definition heap_e  : expr :=
+  Definition heap_e : expr :=
     let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
 
   Lemma heap_e_spec E : WP heap_e @ E {{ v, ⌜v = #2⌝ }}%I.
@@ -62,6 +62,15 @@ Section LiftingTests.
     wp_alloc l''. wp_let. by repeat wp_load.
   Qed.
 
+  Definition heap_e5 : expr :=
+    let: "x" := ref (ref #1) in FAA (!"x") (#10 + #1) + ! !"x".
+
+  Lemma heap_e5_spec E : WP heap_e5 @ E {{ v, ⌜v = #13⌝ }}%I.
+  Proof.
+    rewrite /heap_e5. wp_alloc l. wp_alloc l'. wp_let.
+    wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done.
+  Qed.
+
   Definition FindPred : val :=
     rec: "pred" "x" "y" :=
       let: "yp" := "y" + #1 in
-- 
GitLab