Skip to content
Snippets Groups Projects
Commit 153bc7bd authored by Ralf Jung's avatar Ralf Jung
Browse files

use unique test names

parent fbf452f7
No related branches found
No related tags found
No related merge requests found
......@@ -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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment