summaryrefslogtreecommitdiff
path: root/tests/misc/NoNestedBorrows.fst
diff options
context:
space:
mode:
authorSon Ho2022-04-21 12:29:24 +0200
committerSon Ho2022-04-21 12:29:24 +0200
commit9cda6b33d667b861f371e89e7cccaf43135cfc7a (patch)
treed864a2590ad213f0c56b6e4bb95a4e39c970eda7 /tests/misc/NoNestedBorrows.fst
parent029a12e25e1ee883ac98472f2e032b466d765307 (diff)
Regenerate the test files
Diffstat (limited to 'tests/misc/NoNestedBorrows.fst')
-rw-r--r--tests/misc/NoNestedBorrows.fst18
1 files changed, 8 insertions, 10 deletions
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index e2457a72..8620f7e9 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -112,7 +112,7 @@ let _ = assert_norm (test_list1_fwd = Return ())
(** [no_nested_borrows::test_box1] *)
let test_box1_fwd : result unit =
- let i = 1 in let x = i in if not (x = 1) then Fail else Return ()
+ let b = 1 in let x = b in if not (x = 1) then Fail else Return ()
(** Unit test for [no_nested_borrows::test_box1] *)
let _ = assert_norm (test_box1_fwd = Return ())
@@ -192,10 +192,8 @@ let get_elem_test_fwd : result unit =
else
begin match get_elem_back i32 true 0 0 z0 with
| Fail -> Fail
- | Return (i, i0) ->
- if not (i = 1)
- then Fail
- else if not (i0 = 0) then Fail else Return ()
+ | Return (x, y) ->
+ if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
end
end
end
@@ -334,7 +332,7 @@ let rec list_nth_mut_back
| Return i0 ->
begin match list_nth_mut_back t tl i0 ret with
| Fail -> Fail
- | Return l0 -> Return (ListCons x l0)
+ | Return tl0 -> Return (ListCons x tl0)
end
end
end
@@ -392,20 +390,20 @@ let test_list_functions_fwd : result unit =
else
begin match list_nth_mut_back i32 (ListCons 0 l1) 1 3 with
| Fail -> Fail
- | Return l2 ->
- begin match list_nth_shared_fwd i32 l2 0 with
+ | Return ls ->
+ begin match list_nth_shared_fwd i32 ls 0 with
| Fail -> Fail
| Return i3 ->
if not (i3 = 0)
then Fail
else
- begin match list_nth_shared_fwd i32 l2 1 with
+ begin match list_nth_shared_fwd i32 ls 1 with
| Fail -> Fail
| Return i4 ->
if not (i4 = 3)
then Fail
else
- begin match list_nth_shared_fwd i32 l2 2 with
+ begin match list_nth_shared_fwd i32 ls 2 with
| Fail -> Fail
| Return i5 ->
if not (i5 = 2) then Fail else Return ()