diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref index e27e60ad64920131249f553471d855e479e56dd9..0e1632838da9351acc3a7be9a4aedc8a2f86aa92 100644 --- a/tests/heap_lang.ref +++ b/tests/heap_lang.ref @@ -71,9 +71,9 @@ "wp_load_fail" : string The command has indeed failed with message: -Tactic failure: wp_load: cannot find 'Load' in (Fork Skip). +Tactic failure: wp_load: cannot find 'Load' in (Fork #()). The command has indeed failed with message: -Tactic failure: wp_load: cannot find 'Load' in (Fork Skip). +Tactic failure: wp_load: cannot find 'Load' in (Fork #()). "wp_load_no_ptsto" : string The command has indeed failed with message: @@ -81,9 +81,9 @@ Tactic failure: wp_load: cannot find l ↦ ?. "wp_store_fail" : string The command has indeed failed with message: -Tactic failure: wp_store: cannot find 'Store' in (Fork Skip). +Tactic failure: wp_store: cannot find 'Store' in (Fork #()). The command has indeed failed with message: -Tactic failure: wp_store: cannot find 'Store' in (Fork Skip). +Tactic failure: wp_store: cannot find 'Store' in (Fork #()). "wp_store_no_ptsto" : string The command has indeed failed with message: diff --git a/tests/heap_lang.v b/tests/heap_lang.v index aed38ac393d8e285249992931c41e06d9ca150b6..2e6e82782112fac46036d29e37624c6aaa200931 100644 --- a/tests/heap_lang.v +++ b/tests/heap_lang.v @@ -151,10 +151,10 @@ Section tests. Check "wp_load_fail". Lemma wp_load_fail : - ⊢ WP Fork Skip {{ _, True }}. + ⊢ WP Fork #() {{ _, True }}. Proof. Fail wp_load. Abort. Lemma twp_load_fail : - ⊢ WP Fork Skip [{ _, True }]. + ⊢ WP Fork #() [{ _, True }]. Proof. Fail wp_load. Abort. Check "wp_load_no_ptsto". Lemma wp_load_fail_no_ptsto (l : loc) : @@ -163,10 +163,10 @@ Section tests. Check "wp_store_fail". Lemma wp_store_fail : - ⊢ WP Fork Skip {{ _, True }}. + ⊢ WP Fork #() {{ _, True }}. Proof. Fail wp_store. Abort. Lemma twp_store_fail : - ⊢ WP Fork Skip [{ _, True }]. + ⊢ WP Fork #() [{ _, True }]. Proof. Fail wp_store. Abort. Check "wp_store_no_ptsto". Lemma wp_store_fail_no_ptsto (l : loc) :