diff options
Diffstat (limited to 'tests/misc/NoNestedBorrows.fst')
| -rw-r--r-- | tests/misc/NoNestedBorrows.fst | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst index 48186932..d272bb86 100644 --- a/tests/misc/NoNestedBorrows.fst +++ b/tests/misc/NoNestedBorrows.fst @@ -538,3 +538,17 @@ let _ = assert_norm (test_weird_borrows1_fwd = Return ()) let test_mem_replace_fwd_back (px : u32) : result u32 = let i = mem_replace_fwd u32 px 1 in if not (i = 0) then Fail else Return 2 +(** [no_nested_borrows::test_shared_borrow_bool1] *) +let test_shared_borrow_bool1_fwd (b : bool) : result u32 = + if b then Return 0 else Return 1 + +(** [no_nested_borrows::test_shared_borrow_bool2] *) +let test_shared_borrow_bool2_fwd : result u32 = Return 0 + +(** [no_nested_borrows::test_shared_borrow_enum1] *) +let test_shared_borrow_enum1_fwd (l : list_t u32) : result u32 = + begin match l with | ListCons i l0 -> Return 1 | ListNil -> Return 0 end + +(** [no_nested_borrows::test_shared_borrow_enum2] *) +let test_shared_borrow_enum2_fwd : result u32 = Return 0 + |