From fbfb3ae7f2ff7f849b697251dbecd111011e6e8f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 6 Dec 2019 14:56:39 +0100
Subject: [PATCH] add a test for OffsetOf

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

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index ace305987..f353c853d 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -155,6 +155,14 @@ Section tests.
     by iApply "HΦ".
   Qed.
 
+  Lemma wp_load_array l :
+    {{{ l ↦∗ [ #0;#1;#2 ] }}} !(#l +ₗ #1) {{{ RET #1; True }}}.
+  Proof.
+    iIntros (Φ) "Hl HΦ". wp_op.
+    wp_apply (wp_load_offset _ _ _ 1 with "Hl"); first done.
+    iIntros "Hl". by iApply "HΦ".
+  Qed.
+
   Lemma test_array_app l vs1 vs2 :
     l ↦∗ (vs1 ++ vs2) -∗ l ↦∗ (vs1 ++ vs2).
   Proof.
-- 
GitLab