Tests.

tests/heap_lang.ref

@@ -188,6 +188,59 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   Heq : ∀ v : val, I v ↔ I #true
   ============================
   ⊢ l ↦_(λ _ : val, I #true) □
+"wp_iMod_fupd_atomic"
+     : string
+2 subgoals
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  E1, E2 : coPset
+  P : iPropI Σ
+  ============================
+  Atomic (stuckness_to_atomicity NotStuck) (#() #())
+
+subgoal 2 is:
+ "H" : P
+--------------------------------------∗
+WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
+
+"wp_iInv_atomic"
+     : string
+2 subgoals
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  N : namespace
+  E : coPset
+  P : iProp Σ
+  H : ↑N ⊆ E
+  ============================
+  Atomic (stuckness_to_atomicity NotStuck) (#() #())
+
+subgoal 2 is:
+ "H" : ▷ P
+"Hclose" : ▷ P ={E ∖ ↑N,E}=∗ emp
+--------------------------------------∗
+WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N,E}=> True }}
+
+"wp_iInv_atomic_acc"
+     : string
+2 subgoals
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  N : namespace
+  E : coPset
+  P : iProp Σ
+  H : ↑N ⊆ E
+  ============================
+  Atomic (stuckness_to_atomicity NotStuck) (#() #())
+
+subgoal 2 is:
+ "H" : ▷ P
+--------------------------------------∗
+WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
+
 1 subgoal
   
   Σ : gFunctors

tests/heap_lang.v

-From iris.base_logic.lib Require Import gen_inv_heap.
+From iris.base_logic.lib Require Import gen_inv_heap invariants.
 From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
 (* Import lang *again*. This used to break notation. *)
@@ -323,6 +323,34 @@ Section inv_mapsto_tests.
   Abort.
 End inv_mapsto_tests.
 
+Section atomic.
+  Context `{!heapG Σ}.
+
+  (* These tests check if a side-condition for [Atomic] is generated *)
+  Check "wp_iMod_fupd_atomic".
+  Lemma wp_iMod_fupd_atomic E1 E2 P :
+    (|={E1,E2}=> P) -∗ WP #() #() @ E1 {{ _, True }}.
+  Proof.
+    iIntros "H". iMod "H". Show.
+  Abort.
+
+  Check "wp_iInv_atomic".
+  Lemma wp_iInv_atomic N E P :
+    ↑ N ⊆ E →
+    inv N P -∗ WP #() #() @ E {{ _, True }}.
+  Proof.
+    iIntros (?) "H". iInv "H" as "H" "Hclose". Show.
+  Abort.
+  Check "wp_iInv_atomic_acc".
+  Lemma wp_iInv_atomic_acc N E P :
+    ↑ N ⊆ E →
+    inv N P -∗ WP #() #() @ E {{ _, True }}.
+  Proof.
+    (* Test if a side-condition for [Atomic] is generated *)
+    iIntros (?) "H". iInv "H" as "H". Show.
+  Abort.
+End atomic.
+
 Section printing_tests.
   Context `{!heapG Σ}.