Commit 85245d48 authored by Robbert Krebbers's avatar Robbert Krebbers

Test case for fetch-and-add.

parent adb5b54a
...@@ -20,7 +20,7 @@ Section LiftingTests. ...@@ -20,7 +20,7 @@ Section LiftingTests.
end. end.
Qed. Qed.
Definition heap_e : expr := Definition heap_e : expr :=
let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x". let: "x" := ref #1 in "x" <- !"x" + #1 ;; !"x".
Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I. Lemma heap_e_spec E : WP heap_e @ E {{ v, v = #2 }}%I.
...@@ -62,6 +62,15 @@ Section LiftingTests. ...@@ -62,6 +62,15 @@ Section LiftingTests.
wp_alloc l''. wp_let. by repeat wp_load. wp_alloc l''. wp_let. by repeat wp_load.
Qed. Qed.
Definition heap_e5 : expr :=
let: "x" := ref (ref #1) in FAA (!"x") (#10 + #1) + ! !"x".
Lemma heap_e5_spec E : WP heap_e5 @ E {{ v, v = #13 }}%I.
Proof.
rewrite /heap_e5. wp_alloc l. wp_alloc l'. wp_let.
wp_load. wp_op. wp_faa. do 2 wp_load. wp_op. done.
Qed.
Definition FindPred : val := Definition FindPred : val :=
rec: "pred" "x" "y" := rec: "pred" "x" "y" :=
let: "yp" := "y" + #1 in let: "yp" := "y" + #1 in
......
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