summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2022-04-20 11:51:39 +0200
committerSon Ho2022-04-20 11:51:39 +0200
commitbaa2c0d091b56f97127f536640e2274256072360 (patch)
tree4cf80c60c2889ebb526bc35a2869bde4e73d0901 /tests
parenta5f685ae8d5f5ce5f6052b13bad2208364e003c5 (diff)
Update the evaluation of matches for the cases where the scrutinee is a
shared loan
Diffstat (limited to 'tests')
-rw-r--r--tests/misc/NoNestedBorrows.fst14
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
+