From 2f866db478bb0c54dc1e604bdf5a7f22dda21bf1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 Jul 2022 08:22:16 -0400
Subject: [PATCH] add a test that uses heap_total

---
 tests/heap_lang.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 420b6229b..8e5fc551a 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -1,6 +1,6 @@
 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.
+From iris.heap_lang Require Import lang adequacy total_adequacy proofmode notation.
 (* Import lang *again*. This used to break notation. *)
 From iris.heap_lang Require Import lang.
 From iris.prelude Require Import options.
@@ -453,3 +453,10 @@ End error_tests.
 (* Test a closed proof *)
 Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (λ v _, v = #2).
 Proof. eapply (heap_adequacy heapΣ)=> ??. iIntros "_". by iApply heap_e_spec. Qed.
+
+Lemma heap_e_totally_adequate σ : sn erased_step ([heap_e], σ).
+Proof.
+  eapply (heap_total heapΣ NotStuck _ _ (const True))=> ??. iIntros "_".
+  rewrite /heap_e /=.
+  wp_alloc l. wp_load. wp_store. wp_load. auto.
+Qed.
-- 
GitLab