Commit eeee4aab authored by Dan Frumin's avatar Dan Frumin

Fix the asserts in translation.v

parent 4bfe6d95
......@@ -30,13 +30,13 @@ Definition a_free : val := λ: "x",
let: "l" := Fst "v" in
let: "i" := Snd "v" in
match: !"l" with
NONE => assert #false (* double free *)
NONE => assert: #false (* double free *)
| SOME "l" =>
(* 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
that we can actually establish we initially have the pointer to the first
element of the array. *)
assert ("i" = #0);;
assert: ("i" = #0);;
let: "n" := llength "l" in
a_free_check "env" "l" #0 "n"
"l" <- NONE
......@@ -51,7 +51,7 @@ Definition a_store : val := λ: "x1" "x2",
let: "v" := Snd "vv" in
mset_add ("l", "i") "env" ;;
match: !"l" with
NONE => assert #false (* store after free *)
NONE => assert: #false (* store after free *)
| SOME "ll" => "l" <- SOME (linsert "i" "v" "ll") ;; "v"
end
).
......@@ -64,7 +64,7 @@ Definition a_load : val := λ: "x",
let: "i" := Snd "v" in
assert: (mset_member ("l", "i") "env" = #false);;
match: !"l" with
NONE => assert #false (* load after free *)
NONE => assert: #false (* load after free *)
| SOME "ll" => llookup "i" "ll"
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