diff options
Diffstat (limited to 'tests/fstar/misc/NoNestedBorrows.fst')
| -rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 37 |
1 files changed, 14 insertions, 23 deletions
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index 0fd0c1dc..ffcc32f3 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -220,10 +220,9 @@ let _ = assert_norm (test_list1 = Return ()) (** [no_nested_borrows::test_box1]: Source: 'src/no_nested_borrows.rs', lines 208:0-208:18 *) let test_box1 : result unit = - let b = 0 in - let* (_, deref_mut_back) = alloc_boxed_Box_deref_mut i32 b in - let* b1 = deref_mut_back 1 in - let* x = alloc_boxed_Box_deref i32 b1 in + let* (_, deref_mut_back) = alloc_boxed_Box_deref_mut i32 0 in + let* b = deref_mut_back 1 in + let* x = alloc_boxed_Box_deref i32 b in if not (x = 1) then Fail Failure else Return () (** Unit test for [no_nested_borrows::test_box1] *) @@ -263,8 +262,7 @@ let is_cons (t : Type0) (l : list_t t) : result bool = (** [no_nested_borrows::test_is_cons]: Source: 'src/no_nested_borrows.rs', lines 253:0-253:21 *) let test_is_cons : result unit = - let l = List_Nil in - let* b = is_cons i32 (List_Cons 0 l) in + let* b = is_cons i32 (List_Cons 0 List_Nil) in if not b then Fail Failure else Return () (** Unit test for [no_nested_borrows::test_is_cons] *) @@ -281,8 +279,7 @@ let split_list (t : Type0) (l : list_t t) : result (t & (list_t t)) = (** [no_nested_borrows::test_split_list]: Source: 'src/no_nested_borrows.rs', lines 267:0-267:24 *) let test_split_list : result unit = - let l = List_Nil in - let* p = split_list i32 (List_Cons 0 l) in + let* p = split_list i32 (List_Cons 0 List_Nil) in let (hd, _) = p in if not (hd = 0) then Fail Failure else Return () @@ -388,26 +385,25 @@ let list_rev (t : Type0) (l : list_t t) : result (list_t t) = (** [no_nested_borrows::test_list_functions]: Source: 'src/no_nested_borrows.rs', lines 398:0-398:28 *) let test_list_functions : result unit = - let l = List_Nil in - let l1 = List_Cons 2 l in - let l2 = List_Cons 1 l1 in - let* i = list_length i32 (List_Cons 0 l2) in + let l = List_Cons 2 List_Nil in + let l1 = List_Cons 1 l in + let* i = list_length i32 (List_Cons 0 l1) in if not (i = 3) then Fail Failure else - let* i1 = list_nth_shared i32 (List_Cons 0 l2) 0 in + let* i1 = list_nth_shared i32 (List_Cons 0 l1) 0 in if not (i1 = 0) then Fail Failure else - let* i2 = list_nth_shared i32 (List_Cons 0 l2) 1 in + let* i2 = list_nth_shared i32 (List_Cons 0 l1) 1 in if not (i2 = 1) then Fail Failure else - let* i3 = list_nth_shared i32 (List_Cons 0 l2) 2 in + let* i3 = list_nth_shared i32 (List_Cons 0 l1) 2 in if not (i3 = 2) then Fail Failure else - let* (_, list_nth_mut_back) = list_nth_mut i32 (List_Cons 0 l2) 1 in + let* (_, list_nth_mut_back) = list_nth_mut i32 (List_Cons 0 l1) 1 in let* ls = list_nth_mut_back 3 in let* i4 = list_nth_shared i32 ls 0 in if not (i4 = 0) @@ -448,9 +444,7 @@ let id_mut_pair3 (t1 t2 : Type0) (x : t1) (y : t2) : result ((t1 & t2) & (t1 -> result t1) & (t2 -> result t2)) = - let back_'a = fun ret -> Return ret in - let back_'b = fun ret -> Return ret in - Return ((x, y), back_'a, back_'b) + Return ((x, y), Return, Return) (** [no_nested_borrows::id_mut_pair4]: Source: 'src/no_nested_borrows.rs', lines 426:0-426:92 *) @@ -458,10 +452,7 @@ let id_mut_pair4 (t1 t2 : Type0) (p : (t1 & t2)) : result ((t1 & t2) & (t1 -> result t1) & (t2 -> result t2)) = - let (x, x1) = p in - let back_'a = fun ret -> Return ret in - let back_'b = fun ret -> Return ret in - Return ((x, x1), back_'a, back_'b) + let (x, x1) = p in Return ((x, x1), Return, Return) (** [no_nested_borrows::StructWithTuple] Source: 'src/no_nested_borrows.rs', lines 433:0-433:34 *) |