From b6676f6dc3b1471317cce8e04e9cb7203168f75c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 11 Nov 2022 16:05:56 +0100
Subject: Make minor modifications to the tests and regenerate the .fst files

---
 tests/misc/BetreePolonius.fst  | 41 -----------------------------------------
 tests/misc/NoNestedBorrows.fst | 20 ++++++++++----------
 tests/misc/PoloniusList.fst    | 41 +++++++++++++++++++++++++++++++++++++++++
 3 files changed, 51 insertions(+), 51 deletions(-)
 delete mode 100644 tests/misc/BetreePolonius.fst
 create mode 100644 tests/misc/PoloniusList.fst

(limited to 'tests')

diff --git a/tests/misc/BetreePolonius.fst b/tests/misc/BetreePolonius.fst
deleted file mode 100644
index 2bac07b6..00000000
--- a/tests/misc/BetreePolonius.fst
+++ /dev/null
@@ -1,41 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_polonius] *)
-module BetreePolonius
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [betree_polonius::List] *)
-type list_t (t : Type0) =
-| ListCons : t -> list_t t -> list_t t
-| ListNil : list_t t
-
-(** [betree_polonius::get_list_at_x] *)
-let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
-  begin match ls with
-  | ListCons hd tl ->
-    if hd = x
-    then Return (ListCons hd tl)
-    else
-      begin match get_list_at_x_fwd tl x with
-      | Fail -> Fail
-      | Return l -> Return l
-      end
-  | ListNil -> Return ListNil
-  end
-
-(** [betree_polonius::get_list_at_x] *)
-let rec get_list_at_x_back
-  (ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) =
-  begin match ls with
-  | ListCons hd tl ->
-    if hd = x
-    then Return ret
-    else
-      begin match get_list_at_x_back tl x ret with
-      | Fail -> Fail
-      | Return tl0 -> Return (ListCons hd tl0)
-      end
-  | ListNil -> Return ret
-  end
-
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index a694cff1..8161e7cd 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -184,18 +184,18 @@ let test_split_list_fwd : result unit =
 (** Unit test for [no_nested_borrows::test_split_list] *)
 let _ = assert_norm (test_split_list_fwd = Return ())
 
-(** [no_nested_borrows::get_elem] *)
-let get_elem_fwd (t : Type0) (b : bool) (x : t) (y : t) : result t =
+(** [no_nested_borrows::choose] *)
+let choose_fwd (t : Type0) (b : bool) (x : t) (y : t) : result t =
   if b then Return x else Return y
 
-(** [no_nested_borrows::get_elem] *)
-let get_elem_back
+(** [no_nested_borrows::choose] *)
+let choose_back
   (t : Type0) (b : bool) (x : t) (y : t) (ret : t) : result (t & t) =
   if b then Return (ret, y) else Return (x, ret)
 
-(** [no_nested_borrows::get_elem_test] *)
-let get_elem_test_fwd : result unit =
-  begin match get_elem_fwd i32 true 0 0 with
+(** [no_nested_borrows::choose_test] *)
+let choose_test_fwd : result unit =
+  begin match choose_fwd i32 true 0 0 with
   | Fail -> Fail
   | Return z ->
     begin match i32_add z 1 with
@@ -204,7 +204,7 @@ let get_elem_test_fwd : result unit =
       if not (z0 = 1)
       then Fail
       else
-        begin match get_elem_back i32 true 0 0 z0 with
+        begin match choose_back i32 true 0 0 z0 with
         | Fail -> Fail
         | Return (x, y) ->
           if not (x = 1) then Fail else if not (y = 0) then Fail else Return ()
@@ -212,8 +212,8 @@ let get_elem_test_fwd : result unit =
     end
   end
 
-(** Unit test for [no_nested_borrows::get_elem_test] *)
-let _ = assert_norm (get_elem_test_fwd = Return ())
+(** Unit test for [no_nested_borrows::choose_test] *)
+let _ = assert_norm (choose_test_fwd = Return ())
 
 (** [no_nested_borrows::test_char] *)
 let test_char_fwd : result char = Return 'a'
diff --git a/tests/misc/PoloniusList.fst b/tests/misc/PoloniusList.fst
new file mode 100644
index 00000000..73e98884
--- /dev/null
+++ b/tests/misc/PoloniusList.fst
@@ -0,0 +1,41 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [polonius_list] *)
+module PoloniusList
+open Primitives
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [polonius_list::List] *)
+type list_t (t : Type0) =
+| ListCons : t -> list_t t -> list_t t
+| ListNil : list_t t
+
+(** [polonius_list::get_list_at_x] *)
+let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
+  begin match ls with
+  | ListCons hd tl ->
+    if hd = x
+    then Return (ListCons hd tl)
+    else
+      begin match get_list_at_x_fwd tl x with
+      | Fail -> Fail
+      | Return l -> Return l
+      end
+  | ListNil -> Return ListNil
+  end
+
+(** [polonius_list::get_list_at_x] *)
+let rec get_list_at_x_back
+  (ls : list_t u32) (x : u32) (ret : list_t u32) : result (list_t u32) =
+  begin match ls with
+  | ListCons hd tl ->
+    if hd = x
+    then Return ret
+    else
+      begin match get_list_at_x_back tl x ret with
+      | Fail -> Fail
+      | Return tl0 -> Return (ListCons hd tl0)
+      end
+  | ListNil -> Return ret
+  end
+
-- 
cgit v1.2.3