diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/misc/NoNestedBorrows.fst | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst index ef4a9f82..c83656bf 100644 --- a/tests/misc/NoNestedBorrows.fst +++ b/tests/misc/NoNestedBorrows.fst @@ -30,6 +30,10 @@ type sum_t (t1 t2 : Type0) = | SumLeft : t1 -> sum_t t1 t2 | SumRight : t2 -> sum_t t1 t2 +(** [no_nested_borrows::neg_test] *) +let neg_test_fwd (x : i32) : result i32 = + begin match i32_neg x with | Fail -> Fail | Return i -> Return i end + (** [no_nested_borrows::add_test] *) let add_test_fwd (x : u32) (y : u32) : result u32 = begin match u32_add x y with | Fail -> Fail | Return i -> Return i end @@ -42,6 +46,10 @@ let subs_test_fwd (x : u32) (y : u32) : result u32 = let div_test_fwd (x : u32) (y : u32) : result u32 = begin match u32_div x y with | Fail -> Fail | Return i -> Return i end +(** [no_nested_borrows::div_test1] *) +let div_test1_fwd (x : u32) : result u32 = + begin match u32_div x 2 with | Fail -> Fail | Return i -> Return i end + (** [no_nested_borrows::rem_test] *) let rem_test_fwd (x : u32) (y : u32) : result u32 = begin match u32_rem x y with | Fail -> Fail | Return i -> Return i end @@ -74,12 +82,6 @@ let test3_fwd : result unit = (** Unit test for [no_nested_borrows::test3] *) let _ = assert_norm (test3_fwd = Return ()) -(** [no_nested_borrows::test_neg] *) -let test_neg_fwd (x : i32) : result i32 = - if x = -2147483648 - then Fail - else begin match i32_neg x with | Fail -> Fail | Return i -> Return i end - (** [no_nested_borrows::test_neg1] *) let test_neg1_fwd : result unit = Return () |