diff options
| -rw-r--r-- | Makefile | 17 | ||||
| -rw-r--r-- | tests/misc/BetreePolonius.fst (renamed from tests/misc/BetreeNll.fst) | 10 |
2 files changed, 14 insertions, 13 deletions
@@ -37,7 +37,7 @@ build: tests: build trans-no_nested_borrows trans-paper \ trans-hashmap trans-hashmap_main \ trans-external trans-constants \ - trans-nll-betree_nll trans-nll-betree_main + trans-polonius-betree_polonius trans-polonius-betree_main # Verify the F* files generated by the translation .PHONY: verify @@ -60,8 +60,8 @@ trans-hashmap: SUBDIR:=hashmap trans-hashmap_main: TRANS_OPTIONS += -template-clauses trans-hashmap_main: SUBDIR:=hashmap_on_disk -trans-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses -trans-nll-betree_nll: SUBDIR:=misc +trans-polonius-betree_polonius: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses +trans-polonius-betree_polonius: SUBDIR:=misc trans-constants: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses trans-constants: SUBDIR:=misc @@ -69,8 +69,8 @@ trans-constants: SUBDIR:=misc trans-external: TRANS_OPTIONS += trans-external: SUBDIR:=misc -trans-nll-betree_main: TRANS_OPTIONS += -template-clauses -trans-nll-betree_main: SUBDIR:=betree +trans-polonius-betree_main: TRANS_OPTIONS += -template-clauses +trans-polonius-betree_main: SUBDIR:=betree # Generic rules to extract the LLBC from a rust file # We use the rules in Charon's Makefile to generate the .llbc files: the options @@ -80,15 +80,16 @@ gen-llbc-%: build cd $(CHARON_HOME) && $(MAKE) test-$* # Generic rule to test the translation of an LLBC file. -# Note that the non-linear lifetime files are generated in the tests-nll subdirectory. +# Note that the files requiring the Polonius borrow-checker are generated +# in the tests-polonius subdirectory. .PHONY: trans-% trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc -trans-nll-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-nll/llbc +trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc trans-%: gen-llbc-% dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) -trans-nll-%: gen-llbc-nll-% +trans-polonius-%: gen-llbc-polonius-% dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.llbc -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) .PHONY: doc diff --git a/tests/misc/BetreeNll.fst b/tests/misc/BetreePolonius.fst index b548a18b..2bac07b6 100644 --- a/tests/misc/BetreeNll.fst +++ b/tests/misc/BetreePolonius.fst @@ -1,16 +1,16 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_nll] *) -module BetreeNll +(** [betree_polonius] *) +module BetreePolonius open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_nll::List] *) +(** [betree_polonius::List] *) type list_t (t : Type0) = | ListCons : t -> list_t t -> list_t t | ListNil : list_t t -(** [betree_nll::get_list_at_x] *) +(** [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 -> @@ -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_nll::get_list_at_x] *) +(** [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 |