diff options
author | Son Ho | 2022-04-21 12:29:24 +0200 |
---|---|---|
committer | Son Ho | 2022-04-21 12:29:24 +0200 |
commit | 9cda6b33d667b861f371e89e7cccaf43135cfc7a (patch) | |
tree | d864a2590ad213f0c56b6e4bb95a4e39c970eda7 /tests/misc/NoNestedBorrows.fst | |
parent | 029a12e25e1ee883ac98472f2e032b466d765307 (diff) |
Regenerate the test files
Diffstat (limited to 'tests/misc/NoNestedBorrows.fst')
-rw-r--r-- | tests/misc/NoNestedBorrows.fst | 18 |
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 () |