summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2022-04-20 09:30:30 +0200
committerSon Ho2022-04-20 09:30:30 +0200
commita5f685ae8d5f5ce5f6052b13bad2208364e003c5 (patch)
tree06eb7873e5110ed458a741d24688f1e1b1aa613c /tests
parente0545a9e5e7ba939a1d4d1c05fcfa52d6c9912d3 (diff)
Regenerate a test file
Diffstat (limited to 'tests')
-rw-r--r--tests/misc/NoNestedBorrows.fst20
1 files changed, 20 insertions, 0 deletions
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index fa7ad990..48186932 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -341,6 +341,26 @@ let rec list_nth_mut_back
| ListNil -> Fail
end
+(** [no_nested_borrows::list_rev_aux] *)
+let rec list_rev_aux_fwd
+ (t : Type0) (lo : list_t t) (li : list_t t) : result (list_t t) =
+ begin match li with
+ | ListCons hd tl ->
+ begin match list_rev_aux_fwd t (ListCons hd lo) tl with
+ | Fail -> Fail
+ | Return l -> Return l
+ end
+ | ListNil -> Return lo
+ end
+
+(** [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
+ | Fail -> Fail
+ | Return l1 -> Return l1
+ end
+
(** [no_nested_borrows::test_list_functions] *)
let test_list_functions_fwd : result unit =
let l = ListNil in