summaryrefslogtreecommitdiff
path: root/tests/fstar-split
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/fstar-split/betree/BetreeMain.Funs.fst17
-rw-r--r--tests/fstar-split/hashmap/Hashmap.Funs.fst6
-rw-r--r--tests/fstar-split/hashmap_on_disk/HashmapMain.Funs.fst8
-rw-r--r--tests/fstar-split/misc/External.Funs.fst4
-rw-r--r--tests/fstar-split/misc/NoNestedBorrows.fst26
-rw-r--r--tests/fstar-split/misc/Paper.fst11
-rw-r--r--tests/fstar-split/traits/Traits.fst2
7 files changed, 31 insertions, 43 deletions
diff --git a/tests/fstar-split/betree/BetreeMain.Funs.fst b/tests/fstar-split/betree/BetreeMain.Funs.fst
index 6890488a..33133236 100644
--- a/tests/fstar-split/betree/BetreeMain.Funs.fst
+++ b/tests/fstar-split/betree/BetreeMain.Funs.fst
@@ -113,8 +113,7 @@ let rec betree_List_split_at
let* i = u64_sub n 1 in
let* p = betree_List_split_at t tl i in
let (ls0, ls1) = p in
- let l = ls0 in
- Return (Betree_List_Cons hd l, ls1)
+ Return (Betree_List_Cons hd ls0, ls1)
| Betree_List_Nil -> Fail Failure
end
@@ -124,8 +123,7 @@ let rec betree_List_split_at
let betree_List_push_front
(t : Type0) (self : betree_List_t t) (x : t) : result (betree_List_t t) =
let tl = core_mem_replace (betree_List_t t) self Betree_List_Nil in
- let l = tl in
- Return (Betree_List_Cons x l)
+ Return (Betree_List_Cons x tl)
(** [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function
Source: 'src/betree.rs', lines 306:4-306:32 *)
@@ -178,8 +176,7 @@ let rec betree_ListTupleU64T_partition_at_pivot
else
let* p = betree_ListTupleU64T_partition_at_pivot t tl pivot in
let (ls0, ls1) = p in
- let l = ls0 in
- Return (Betree_List_Cons (i, x) l, ls1)
+ Return (Betree_List_Cons (i, x) ls0, ls1)
| Betree_List_Nil -> Return (Betree_List_Nil, Betree_List_Nil)
end
@@ -871,13 +868,12 @@ let betree_Node_apply
(new_msg : betree_Message_t) (st : state) :
result (state & unit)
=
- let l = Betree_List_Nil in
let* (st1, _) =
betree_Node_apply_messages self params node_id_cnt (Betree_List_Cons (key,
- new_msg) l) st in
+ new_msg) Betree_List_Nil) st in
let* _ =
betree_Node_apply_messages_back self params node_id_cnt (Betree_List_Cons
- (key, new_msg) l) st in
+ (key, new_msg) Betree_List_Nil) st in
Return (st1, ())
(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0
@@ -888,9 +884,8 @@ let betree_Node_apply_back
(new_msg : betree_Message_t) (st : state) :
result (betree_Node_t & betree_NodeIdCounter_t)
=
- let l = Betree_List_Nil in
betree_Node_apply_messages_back self params node_id_cnt (Betree_List_Cons
- (key, new_msg) l) st
+ (key, new_msg) Betree_List_Nil) st
(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function
Source: 'src/betree.rs', lines 849:4-849:60 *)
diff --git a/tests/fstar-split/hashmap/Hashmap.Funs.fst b/tests/fstar-split/hashmap/Hashmap.Funs.fst
index 79327183..290d49ee 100644
--- a/tests/fstar-split/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar-split/hashmap/Hashmap.Funs.fst
@@ -41,8 +41,8 @@ let hashMap_new_with_capacity
(max_load_divisor : usize) :
result (hashMap_t t)
=
- let v = alloc_vec_Vec_new (list_t t) in
- let* slots = hashMap_allocate_slots t v capacity in
+ let* slots = hashMap_allocate_slots t (alloc_vec_Vec_new (list_t t)) capacity
+ in
let* i = usize_mul capacity max_load_dividend in
let* i1 = usize_div i max_load_divisor in
Return
@@ -124,7 +124,7 @@ let rec hashMap_insert_in_list_loop_back
else
let* tl1 = hashMap_insert_in_list_loop_back t key value tl in
Return (List_Cons ckey cvalue tl1)
- | List_Nil -> let l = List_Nil in Return (List_Cons key value l)
+ | List_Nil -> Return (List_Cons key value List_Nil)
end
(** [hashmap::{hashmap::HashMap<T>}::insert_in_list]: backward function 0
diff --git a/tests/fstar-split/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar-split/hashmap_on_disk/HashmapMain.Funs.fst
index b2800e1e..2e2d54b8 100644
--- a/tests/fstar-split/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar-split/hashmap_on_disk/HashmapMain.Funs.fst
@@ -43,8 +43,9 @@ let hashmap_HashMap_new_with_capacity
(max_load_divisor : usize) :
result (hashmap_HashMap_t t)
=
- let v = alloc_vec_Vec_new (hashmap_List_t t) in
- let* slots = hashmap_HashMap_allocate_slots t v capacity in
+ let* slots =
+ hashmap_HashMap_allocate_slots t (alloc_vec_Vec_new (hashmap_List_t t))
+ capacity in
let* i = usize_mul capacity max_load_dividend in
let* i1 = usize_div i max_load_divisor in
Return
@@ -128,8 +129,7 @@ let rec hashmap_HashMap_insert_in_list_loop_back
else
let* tl1 = hashmap_HashMap_insert_in_list_loop_back t key value tl in
Return (Hashmap_List_Cons ckey cvalue tl1)
- | Hashmap_List_Nil ->
- let l = Hashmap_List_Nil in Return (Hashmap_List_Cons key value l)
+ | Hashmap_List_Nil -> Return (Hashmap_List_Cons key value Hashmap_List_Nil)
end
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: backward function 0
diff --git a/tests/fstar-split/misc/External.Funs.fst b/tests/fstar-split/misc/External.Funs.fst
index 3b84697e..65382549 100644
--- a/tests/fstar-split/misc/External.Funs.fst
+++ b/tests/fstar-split/misc/External.Funs.fst
@@ -36,9 +36,7 @@ let test_new_non_zero_u32
(** [external::test_vec]: forward function
Source: 'src/external.rs', lines 17:0-17:17 *)
let test_vec : result unit =
- let v = alloc_vec_Vec_new u32 in
- let* _ = alloc_vec_Vec_push u32 v 0 in
- Return ()
+ let* _ = alloc_vec_Vec_push u32 (alloc_vec_Vec_new u32) 0 in Return ()
(** Unit test for [external::test_vec] *)
let _ = assert_norm (test_vec = Return ())
diff --git a/tests/fstar-split/misc/NoNestedBorrows.fst b/tests/fstar-split/misc/NoNestedBorrows.fst
index 41bb7a06..53e1d300 100644
--- a/tests/fstar-split/misc/NoNestedBorrows.fst
+++ b/tests/fstar-split/misc/NoNestedBorrows.fst
@@ -220,9 +220,8 @@ let _ = assert_norm (test_list1 = Return ())
(** [no_nested_borrows::test_box1]: forward function
Source: 'src/no_nested_borrows.rs', lines 208:0-208:18 *)
let test_box1 : result unit =
- let b = 0 in
- let* b1 = alloc_boxed_Box_deref_mut_back i32 b 1 in
- let* x = alloc_boxed_Box_deref i32 b1 in
+ let* b = alloc_boxed_Box_deref_mut_back i32 0 1 in
+ let* x = alloc_boxed_Box_deref i32 b in
if not (x = 1) then Fail Failure else Return ()
(** Unit test for [no_nested_borrows::test_box1] *)
@@ -262,8 +261,7 @@ let is_cons (t : Type0) (l : list_t t) : result bool =
(** [no_nested_borrows::test_is_cons]: forward function
Source: 'src/no_nested_borrows.rs', lines 253:0-253:21 *)
let test_is_cons : result unit =
- let l = List_Nil in
- let* b = is_cons i32 (List_Cons 0 l) in
+ let* b = is_cons i32 (List_Cons 0 List_Nil) in
if not b then Fail Failure else Return ()
(** Unit test for [no_nested_borrows::test_is_cons] *)
@@ -280,8 +278,7 @@ let split_list (t : Type0) (l : list_t t) : result (t & (list_t t)) =
(** [no_nested_borrows::test_split_list]: forward function
Source: 'src/no_nested_borrows.rs', lines 267:0-267:24 *)
let test_split_list : result unit =
- let l = List_Nil in
- let* p = split_list i32 (List_Cons 0 l) in
+ let* p = split_list i32 (List_Cons 0 List_Nil) in
let (hd, _) = p in
if not (hd = 0) then Fail Failure else Return ()
@@ -393,26 +390,25 @@ let list_rev (t : Type0) (l : list_t t) : result (list_t t) =
(** [no_nested_borrows::test_list_functions]: forward function
Source: 'src/no_nested_borrows.rs', lines 398:0-398:28 *)
let test_list_functions : result unit =
- let l = List_Nil in
- let l1 = List_Cons 2 l in
- let l2 = List_Cons 1 l1 in
- let* i = list_length i32 (List_Cons 0 l2) in
+ let l = List_Cons 2 List_Nil in
+ let l1 = List_Cons 1 l in
+ let* i = list_length i32 (List_Cons 0 l1) in
if not (i = 3)
then Fail Failure
else
- let* i1 = list_nth_shared i32 (List_Cons 0 l2) 0 in
+ let* i1 = list_nth_shared i32 (List_Cons 0 l1) 0 in
if not (i1 = 0)
then Fail Failure
else
- let* i2 = list_nth_shared i32 (List_Cons 0 l2) 1 in
+ let* i2 = list_nth_shared i32 (List_Cons 0 l1) 1 in
if not (i2 = 1)
then Fail Failure
else
- let* i3 = list_nth_shared i32 (List_Cons 0 l2) 2 in
+ let* i3 = list_nth_shared i32 (List_Cons 0 l1) 2 in
if not (i3 = 2)
then Fail Failure
else
- let* ls = list_nth_mut_back i32 (List_Cons 0 l2) 1 3 in
+ let* ls = list_nth_mut_back i32 (List_Cons 0 l1) 1 3 in
let* i4 = list_nth_shared i32 ls 0 in
if not (i4 = 0)
then Fail Failure
diff --git a/tests/fstar-split/misc/Paper.fst b/tests/fstar-split/misc/Paper.fst
index 2dc804de..0c44d78b 100644
--- a/tests/fstar-split/misc/Paper.fst
+++ b/tests/fstar-split/misc/Paper.fst
@@ -87,13 +87,12 @@ let rec sum (l : list_t i32) : result i32 =
(** [paper::test_nth]: forward function
Source: 'src/paper.rs', lines 68:0-68:17 *)
let test_nth : result unit =
- let l = List_Nil in
- let l1 = List_Cons 3 l in
- let l2 = List_Cons 2 l1 in
- let* x = list_nth_mut i32 (List_Cons 1 l2) 2 in
+ let l = List_Cons 3 List_Nil in
+ let l1 = List_Cons 2 l in
+ let* x = list_nth_mut i32 (List_Cons 1 l1) 2 in
let* x1 = i32_add x 1 in
- let* l3 = list_nth_mut_back i32 (List_Cons 1 l2) 2 x1 in
- let* i = sum l3 in
+ let* l2 = list_nth_mut_back i32 (List_Cons 1 l1) 2 x1 in
+ let* i = sum l2 in
if not (i = 7) then Fail Failure else Return ()
(** Unit test for [paper::test_nth] *)
diff --git a/tests/fstar-split/traits/Traits.fst b/tests/fstar-split/traits/Traits.fst
index 29a001b2..d3847590 100644
--- a/tests/fstar-split/traits/Traits.fst
+++ b/tests/fstar-split/traits/Traits.fst
@@ -274,7 +274,7 @@ let use_with_const_ty1
(h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len) :
result usize
=
- let i = withConstTyHLENInst.cLEN1 in Return i
+ Return withConstTyHLENInst.cLEN1
(** [traits::use_with_const_ty2]: forward function
Source: 'src/traits.rs', lines 187:0-187:73 *)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 15:59:14 +0000