Make minor modifications to the tests and regenerate the .fst files

3 files changed, 19 insertions, 19 deletions

diff --git a/Makefile b/Makefile
index 2c324a41..3f04ff09 100644
--- a/Makefile
+++ b/Makefile
@@ -86,7 +86,7 @@ clean:
 tests: trans-no_nested_borrows trans-paper \
 	trans-hashmap trans-hashmap_main \
 	trans-external trans-constants \
-	trans-polonius-betree_polonius trans-polonius-betree_main \
+	trans-polonius-polonius_list trans-polonius-betree_main \
 	test-trans-polonius-betree_main
 
 # Verify the F* files generated by the translation
@@ -106,7 +106,7 @@ CHARON_CMD = cd $(CHARON_TEST_DIR) && NOT_ALL_TESTS=1 $(MAKE) test-$*
 endif
 
 # The command to run Aeneas on the proper llbc file
-AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest ../tests/$(SUBDIR) $(OPTIONS)
+AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(SUBDIR) $(OPTIONS)
 
 
 # Add specific options to some tests
@@ -120,8 +120,8 @@ trans-hashmap: SUBDIR:=hashmap
 trans-hashmap_main: OPTIONS += -template-clauses
 trans-hashmap_main: SUBDIR:=hashmap_on_disk
 
-trans-polonius-betree_polonius: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
-trans-polonius-betree_polonius: SUBDIR:=misc
+trans-polonius-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
+trans-polonius-polonius_list: SUBDIR:=misc
 
 trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
 trans-constants: SUBDIR:=misc
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/BetreePolonius.fst b/tests/misc/PoloniusList.fst
index 2bac07b6..73e98884 100644
--- a/tests/misc/BetreePolonius.fst
+++ b/tests/misc/PoloniusList.fst
@@ -1,16 +1,16 @@
 (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [betree_polonius] *)
-module BetreePolonius
+(** [polonius_list] *)
+module PoloniusList
 open Primitives
 
 #set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
 
-(** [betree_polonius::List] *)
+(** [polonius_list::List] *)
 type list_t (t : Type0) =
 | ListCons : t -> list_t t -> list_t t
 | ListNil : list_t t
 
-(** [betree_polonius::get_list_at_x] *)
+(** [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 ->
@@ -24,7 +24,7 @@ let rec get_list_at_x_fwd (ls : list_t u32) (x : u32) : result (list_t u32) =
   | ListNil -> Return ListNil
   end
 
-(** [betree_polonius::get_list_at_x] *)
+(** [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