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 --- Makefile | 8 ++++---- tests/misc/BetreePolonius.fst | 41 ----------------------------------------- tests/misc/NoNestedBorrows.fst | 20 ++++++++++---------- tests/misc/PoloniusList.fst | 41 +++++++++++++++++++++++++++++++++++++++++ 4 files changed, 55 insertions(+), 55 deletions(-) delete mode 100644 tests/misc/BetreePolonius.fst create mode 100644 tests/misc/PoloniusList.fst 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/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