Commit 0fbb2bec authored by Hai Dang's avatar Hai Dang
Browse files

Remove a TODO in na stack

parent a1492abc
......@@ -36,6 +36,7 @@ Proof.
Qed.
Definition NAStack_def := fixpoint NAStack'.
(* The stack resources contain freeable blocks, so that we can deallocate it. *)
Definition NAStack s A := ( s 1 NAStack_def s A)%I.
End defs.
......@@ -53,7 +54,6 @@ Proof.
(* allocation *)
wp_apply wp_new; [done..|].
iIntros (s) "([H†|%] & Hs & Hm)"; [|done].
(* TODO: we never reclaim the head, so H† is unused. *)
wp_let.
(* initialize head as 0 *)
rewrite own_loc_na_vec_singleton. wp_write.
......
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