diff options
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | tests/misc/NoNestedBorrows.fst | 20 | ||||
| -rw-r--r-- | tests/misc/PoloniusList.fst (renamed from tests/misc/BetreePolonius.fst) | 10 |
3 files changed, 19 insertions, 19 deletions
@@ -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 |