From 153bc7bd6b6314acc70a43ee09f827330fe6d1df Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 2 Feb 2021 17:16:40 +0100 Subject: [PATCH] use unique test names --- tests/heap_lang.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/heap_lang.v b/tests/heap_lang.v index ef63f45f9..aed38ac39 100644 --- a/tests/heap_lang.v +++ b/tests/heap_lang.v @@ -153,11 +153,11 @@ Section tests. Lemma wp_load_fail : ⊢ WP Fork Skip {{ _, True }}. Proof. Fail wp_load. Abort. - Lemma wp_load_fail : + Lemma twp_load_fail : ⊢ WP Fork Skip [{ _, True }]. Proof. Fail wp_load. Abort. Check "wp_load_no_ptsto". - Lemma wp_load_fail (l: loc) : + Lemma wp_load_fail_no_ptsto (l : loc) : ⊢ WP ! #l {{ _, True }}. Proof. Fail wp_load. Abort. @@ -165,11 +165,11 @@ Section tests. Lemma wp_store_fail : ⊢ WP Fork Skip {{ _, True }}. Proof. Fail wp_store. Abort. - Lemma wp_store_fail : + Lemma twp_store_fail : ⊢ WP Fork Skip [{ _, True }]. Proof. Fail wp_store. Abort. Check "wp_store_no_ptsto". - Lemma wp_store_fail (l: loc) : + Lemma wp_store_fail_no_ptsto (l : loc) : ⊢ WP #l <- #0 {{ _, True }}. Proof. Fail wp_store. Abort. -- GitLab