Commit 43838a40 authored by Ralf Jung's avatar Ralf Jung

test 'not a CAS' error message as well

parent 01663351
......@@ -73,3 +73,8 @@
The command has indeed failed with message:
Ltac call to "wp_cas_suc" failed.
Tactic failure: wp_cas_suc: Values are not safe to compare for CAS.
"not_cas"
: string
The command has indeed failed with message:
Ltac call to "wp_cas_suc" failed.
Tactic failure: wp_cas_suc: cannot find 'CAS' in (#())%E.
......@@ -170,6 +170,13 @@ Section error_tests.
Proof.
iIntros "H↦". Fail wp_cas_suc.
Abort.
Check "not_cas".
Lemma not_cas :
(WP #() {{ _, True }})%I.
Proof.
Fail wp_cas_suc.
Abort.
End error_tests.
Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment