Commit 0013d853 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix bug in `wp_cas_suc`.

This closes issue #220.
parent 8d2e6a66
......@@ -78,6 +78,11 @@ Section tests.
Lemma heap_e6_spec (v : val) : (WP heap_e6 v {{ w, w = #true }})%I.
Proof. wp_lam. wp_op. by case_bool_decide. Qed.
Definition heap_e7 : val := λ: "v", CAS "v" #0 #1.
Lemma heap_e7_spec l : l #0 - WP heap_e7 #l [{_, l #1 }].
Proof. iIntros. wp_lam. wp_cas_suc. auto. Qed.
Definition FindPred : val :=
rec: "pred" "x" "y" :=
let: "yp" := "y" + #1 in
......
......@@ -511,7 +511,7 @@ Tactic Notation "wp_cas_suc" :=
|try congruence
|try fast_done (* vals_cas_compare_safe *)
|simpl; try wp_value_head]
| |- envs_entails _ (twp ?E ?e ?Q) =>
| |- envs_entails _ (twp ?s ?E ?e ?Q) =>
first
[reshape_expr e ltac:(fun K e' => eapply (tac_twp_cas_suc _ _ _ _ _ K))
|fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
......
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