diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/misc/NoNestedBorrows.fst | 34 | ||||
| -rw-r--r-- | tests/misc/Paper.fst | 36 |
2 files changed, 35 insertions, 35 deletions
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst index d272bb86..e2457a72 100644 --- a/tests/misc/NoNestedBorrows.fst +++ b/tests/misc/NoNestedBorrows.fst @@ -60,11 +60,11 @@ let get_max_fwd (x : u32) (y : u32) : result u32 = let test3_fwd : result unit = begin match get_max_fwd 4 3 with | Fail -> Fail - | Return i -> + | Return x -> begin match get_max_fwd 10 11 with | Fail -> Fail - | Return i0 -> - begin match u32_add i i0 with + | Return y -> + begin match u32_add x y with | Fail -> Fail | Return z -> if not (z = 15) then Fail else Return () end @@ -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 i0 = i in if not (i0 = 1) then Fail else Return () + let i = 1 in let x = i in if not (x = 1) then Fail else Return () (** Unit test for [no_nested_borrows::test_box1] *) let _ = assert_norm (test_box1_fwd = Return ()) @@ -131,7 +131,7 @@ let test_panic_fwd (b : bool) : result unit = if b then Fail else Return () let test_copy_int_fwd : result unit = begin match copy_int_fwd 0 with | Fail -> Fail - | Return i -> if not (0 = i) then Fail else Return () + | Return y -> if not (0 = y) then Fail else Return () end (** Unit test for [no_nested_borrows::test_copy_int] *) @@ -183,19 +183,19 @@ let get_elem_back let get_elem_test_fwd : result unit = begin match get_elem_fwd i32 true 0 0 with | Fail -> Fail - | Return i -> - begin match i32_add i 1 with + | Return z -> + begin match i32_add z 1 with | Fail -> Fail - | Return z -> - if not (z = 1) + | Return z0 -> + if not (z0 = 1) then Fail else - begin match get_elem_back i32 true 0 0 z with + begin match get_elem_back i32 true 0 0 z0 with | Fail -> Fail - | Return (i0, i1) -> - if not (i0 = 1) + | Return (i, i0) -> + if not (i = 1) then Fail - else if not (i1 = 0) then Fail else Return () + else if not (i0 = 0) then Fail else Return () end end end @@ -355,10 +355,10 @@ let rec list_rev_aux_fwd (** [no_nested_borrows::list_rev] *) let list_rev_fwd_back (t : Type0) (l : list_t t) : result (list_t t) = - let l0 = mem_replace_fwd (list_t t) l ListNil in - begin match list_rev_aux_fwd t ListNil l0 with + let li = mem_replace_fwd (list_t t) l ListNil in + begin match list_rev_aux_fwd t ListNil li with | Fail -> Fail - | Return l1 -> Return l1 + | Return l0 -> Return l0 end (** [no_nested_borrows::test_list_functions] *) @@ -536,7 +536,7 @@ let _ = assert_norm (test_weird_borrows1_fwd = Return ()) (** [no_nested_borrows::test_mem_replace] *) 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 + let y = mem_replace_fwd u32 px 1 in if not (y = 0) then Fail else Return 2 (** [no_nested_borrows::test_shared_borrow_bool1] *) let test_shared_borrow_bool1_fwd (b : bool) : result u32 = diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst index 1278733b..a6ec184c 100644 --- a/tests/misc/Paper.fst +++ b/tests/misc/Paper.fst @@ -32,19 +32,19 @@ let choose_back let test_choose_fwd : result unit = begin match choose_fwd i32 true 0 0 with | Fail -> Fail - | Return i -> - begin match i32_add i 1 with + | Return z -> + begin match i32_add z 1 with | Fail -> Fail - | Return z -> - if not (z = 1) + | Return z0 -> + if not (z0 = 1) then Fail else - begin match choose_back i32 true 0 0 z with + begin match choose_back i32 true 0 0 z0 with | Fail -> Fail - | Return (i0, i1) -> - if not (i0 = 1) + | Return (i, i0) -> + if not (i = 1) then Fail - else if not (i1 = 0) then Fail else Return () + else if not (i0 = 0) then Fail else Return () end end end @@ -115,16 +115,16 @@ let test_nth_fwd : result unit = let l1 = ListCons 2 l0 in begin match list_nth_mut_fwd i32 (ListCons 1 l1) 2 with | Fail -> Fail - | Return i -> - begin match i32_add i 1 with + | Return x -> + begin match i32_add x 1 with | Fail -> Fail - | Return x -> - begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x with + | Return x0 -> + begin match list_nth_mut_back i32 (ListCons 1 l1) 2 x0 with | Fail -> Fail | Return l2 -> begin match sum_fwd l2 with | Fail -> Fail - | Return i0 -> if not (i0 = 7) then Fail else Return () + | Return i -> if not (i = 7) then Fail else Return () end end end @@ -138,13 +138,13 @@ let call_choose_fwd (p : (u32 & u32)) : result u32 = let (px, py) = p in begin match choose_fwd u32 true px py with | Fail -> Fail - | Return i -> - begin match u32_add i 1 with + | Return pz -> + begin match u32_add pz 1 with | Fail -> Fail - | Return pz -> - begin match choose_back u32 true px py pz with + | Return pz0 -> + begin match choose_back u32 true px py pz0 with | Fail -> Fail - | Return (i0, _) -> Return i0 + | Return (i, _) -> Return i end end end |