Commit 62b6b4ff authored by Dan Frumin's avatar Dan Frumin
Browse files

Quickfix in a_free

parent eeee4aab
...@@ -31,14 +31,14 @@ Definition a_free : val := λ: "x", ...@@ -31,14 +31,14 @@ Definition a_free : val := λ: "x",
let: "i" := Snd "v" in let: "i" := Snd "v" in
match: !"l" with match: !"l" with
NONE => assert: #false (* double free *) NONE => assert: #false (* double free *)
| SOME "l" => | SOME "ll" =>
(* We need to make sure `i = 0` and that all `0 ... length of block` are (* We need to make sure `i = 0` and that all `0 ... length of block` are
unlocked. TODO: this means we need to change the spec of `alloc` back so unlocked. TODO: this means we need to change the spec of `alloc` back so
that we can actually establish we initially have the pointer to the first that we can actually establish we initially have the pointer to the first
element of the array. *) element of the array. *)
assert: ("i" = #0);; assert: ("i" = #0);;
let: "n" := llength "l" in let: "n" := llength "ll" in
a_free_check "env" "l" #0 "n" a_free_check "env" "ll" #0 "n";;
"l" <- NONE "l" <- NONE
end end
). ).
......
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