diff options
Diffstat (limited to 'tests/fstar/misc')
-rw-r--r-- | tests/fstar/misc/External.Funs.fst | 4 | ||||
-rw-r--r-- | tests/fstar/misc/Loops.Clauses.Template.fst | 3 | ||||
-rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 24 | ||||
-rw-r--r-- | tests/fstar/misc/NoNestedBorrows.fst | 7 | ||||
-rw-r--r-- | tests/fstar/misc/Paper.fst | 2 |
5 files changed, 18 insertions, 22 deletions
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index 6672b523..3ba20022 100644 --- a/tests/fstar/misc/External.Funs.fst +++ b/tests/fstar/misc/External.Funs.fst @@ -33,8 +33,8 @@ let custom_swap (t : Type0) (x : t) (y : t) (st : state) : result (state & (t & (t -> state -> result (state & (t & t))))) = - let* (st1, (x1, x2)) = core_mem_swap t x y st in - let back_'a = fun ret st2 -> Return (st2, (ret, x2)) in + let* (st1, (x1, y1)) = core_mem_swap t x y st in + let back_'a = fun ret st2 -> Return (st2, (ret, y1)) in Return (st1, (x1, back_'a)) (** [external::test_custom_swap]: diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst index c8ed16f4..e43f8170 100644 --- a/tests/fstar/misc/Loops.Clauses.Template.fst +++ b/tests/fstar/misc/Loops.Clauses.Template.fst @@ -13,8 +13,7 @@ unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit () (** [loops::sum_with_mut_borrows]: decreases clause Source: 'src/loops.rs', lines 19:0-31:1 *) unfold -let sum_with_mut_borrows_loop_decreases (max : u32) (mi : u32) (ms : u32) : nat - = +let sum_with_mut_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit () (** [loops::sum_with_shared_borrows]: decreases clause diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index c87f693b..7c099da2 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -25,15 +25,15 @@ let sum (max : u32) : result u32 = (** [loops::sum_with_mut_borrows]: loop 0: Source: 'src/loops.rs', lines 19:0-31:1 *) let rec sum_with_mut_borrows_loop - (max : u32) (mi : u32) (ms : u32) : - Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms)) + (max : u32) (i : u32) (s : u32) : + Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max i s)) = - if mi < max + if i < max then - let* ms1 = u32_add ms mi in - let* mi1 = u32_add mi 1 in - sum_with_mut_borrows_loop max mi1 ms1 - else u32_mul ms 2 + let* ms = u32_add s i in + let* mi = u32_add i 1 in + sum_with_mut_borrows_loop max mi ms + else u32_mul s 2 (** [loops::sum_with_mut_borrows]: Source: 'src/loops.rs', lines 19:0-19:44 *) @@ -185,11 +185,11 @@ let get_elem_mut (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result (usize & (usize -> result (alloc_vec_Vec (list_t usize)))) = - let* (l, index_mut_back) = + let* (ls, index_mut_back) = alloc_vec_Vec_index_mut (list_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in - let* (i, back) = get_elem_mut_loop x l in - let back1 = fun ret -> let* l1 = back ret in index_mut_back l1 in + let* (i, back) = get_elem_mut_loop x ls in + let back1 = fun ret -> let* l = back ret in index_mut_back l in Return (i, back1) (** [loops::get_elem_shared]: loop 0: @@ -207,10 +207,10 @@ let rec get_elem_shared_loop Source: 'src/loops.rs', lines 129:0-129:68 *) let get_elem_shared (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = - let* l = + let* ls = alloc_vec_Vec_index (list_t usize) usize (core_slice_index_SliceIndexUsizeSliceTInst (list_t usize)) slots 0 in - get_elem_shared_loop x l + get_elem_shared_loop x ls (** [loops::id_mut]: Source: 'src/loops.rs', lines 145:0-145:50 *) diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst index c71f8dbb..db63eb0d 100644 --- a/tests/fstar/misc/NoNestedBorrows.fst +++ b/tests/fstar/misc/NoNestedBorrows.fst @@ -425,8 +425,7 @@ let id_mut_pair1 (t1 t2 : Type0) (x : t1) (y : t2) : result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2))) = - let back_'a = fun ret -> let (x1, x2) = ret in Return (x1, x2) in - Return ((x, y), back_'a) + Return ((x, y), Return) (** [no_nested_borrows::id_mut_pair2]: Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 *) @@ -434,9 +433,7 @@ let id_mut_pair2 (t1 t2 : Type0) (p : (t1 & t2)) : result ((t1 & t2) & ((t1 & t2) -> result (t1 & t2))) = - let (x, x1) = p in - let back_'a = fun ret -> let (x2, x3) = ret in Return (x2, x3) in - Return ((x, x1), back_'a) + let (x, x1) = p in Return ((x, x1), Return) (** [no_nested_borrows::id_mut_pair3]: Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 *) diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst index cf4dc454..ddc5e7a8 100644 --- a/tests/fstar/misc/Paper.fst +++ b/tests/fstar/misc/Paper.fst @@ -13,7 +13,7 @@ let ref_incr (x : i32) : result i32 = (** [paper::test_incr]: Source: 'src/paper.rs', lines 8:0-8:18 *) let test_incr : result unit = - let* i = ref_incr 0 in if not (i = 1) then Fail Failure else Return () + let* x = ref_incr 0 in if not (x = 1) then Fail Failure else Return () (** Unit test for [paper::test_incr] *) let _ = assert_norm (test_incr = Return ()) |