summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2022-11-11 16:05:56 +0100
committerSon Ho2022-11-11 16:05:56 +0100
commitb6676f6dc3b1471317cce8e04e9cb7203168f75c (patch)
tree29954f1730a9bf2a4dfda30f32c7291383815a67 /tests
parent61740913f8af53f0c1054375482b980ccb12f089 (diff)
Make minor modifications to the tests and regenerate the .fst files
Diffstat (limited to 'tests')
-rw-r--r--tests/misc/NoNestedBorrows.fst20
-rw-r--r--tests/misc/PoloniusList.fst (renamed from tests/misc/BetreePolonius.fst)10
2 files changed, 15 insertions, 15 deletions
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