Update the Makefile to rename the "trans-" rules to "test-"

1 files changed, 46 insertions, 46 deletions

diff --git a/Makefile b/Makefile
index 486ba40e..bdabe878 100644
--- a/Makefile
+++ b/Makefile
@@ -85,13 +85,13 @@ clean:
 
 # Test the project by translating test files to F*
 .PHONY: tests
-tests: trans-no_nested_borrows trans-paper \
-	trans-hashmap trans-hashmap_main \
-	trans-external trans-constants \
-	transp-polonius_list transp-betree_main \
-	test-transp-betree_main \
-	trans-loops \
-	trans-array trans-traits # TODO: generalize to all backends
+tests: test-no_nested_borrows test-paper \
+	test-hashmap test-hashmap_main \
+	test-external test-constants \
+	testp-polonius_list testp-betree_main \
+	ctest-testp-betree_main \
+	test-loops \
+	test-array test-traits # TODO: generalize to all backends
 
 # Verify the F* files generated by the translation
 .PHONY: verify
@@ -114,25 +114,25 @@ AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BA
 
 
 # Add specific options to some tests
-trans-no_nested_borrows trans-paper: \
+test-no_nested_borrows test-paper: \
 	OPTIONS += -test-trans-units -no-split-files -no-state
-trans-no_nested_borrows trans-paper: SUBDIR := misc
+test-no_nested_borrows test-paper: SUBDIR := misc
 tfstar-no_nested_borrows tfstar-paper:
 tlean-no_nested_borrows: SUBDIR :=
 tlean-paper: SUBDIR :=
 thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows
 thol4-paper: SUBDIR := misc-paper
 
-trans-array: OPTIONS += -no-state
-trans-array: SUBDIR := array
+test-array: OPTIONS += -no-state
+test-array: SUBDIR := array
 tfstar-array: OPTIONS += -decreases-clauses -template-clauses
 tcoq-array: OPTIONS += -use-fuel
 tlean-array: SUBDIR :=
 tlean-array: OPTIONS +=
 thol4-array: OPTIONS +=
 
-trans-traits: OPTIONS += -no-state
-trans-traits: SUBDIR := traits
+test-traits: OPTIONS += -no-state
+test-traits: SUBDIR := traits
 tfstar-traits: OPTIONS += -decreases-clauses -template-clauses
 tcoq-traits: OPTIONS += -use-fuel
 tlean-traits: SUBDIR :=
@@ -147,16 +147,16 @@ thol4-array:
 thol4-traits:
 	echo "Ignoring the traits test for HOL4"
 
-trans-loops: OPTIONS += -no-state
-trans-loops: SUBDIR := misc
+test-loops: OPTIONS += -no-state
+test-loops: SUBDIR := misc
 tfstar-loops: OPTIONS += -decreases-clauses -template-clauses
 tcoq-loops: OPTIONS += -use-fuel -no-split-files
 tlean-loops: SUBDIR :=
 thol4-loops: SUBDIR := misc-loops
 
 # TODO: reactivate -test-trans-units
-trans-hashmap: OPTIONS += -no-state
-trans-hashmap: SUBDIR := hashmap
+test-hashmap: OPTIONS += -no-state
+test-hashmap: SUBDIR := hashmap
 tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap: OPTIONS += -use-fuel
 tlean-hashmap: SUBDIR :=
@@ -164,15 +164,15 @@ tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hash
 thol4-hashmap: OPTIONS +=
 
 # TODO: reactivate -test-trans-units
-trans-hashmap_main: OPTIONS +=
-trans-hashmap_main: SUBDIR := hashmap_on_disk
+test-hashmap_main: OPTIONS +=
+test-hashmap_main: SUBDIR := hashmap_on_disk
 tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap_main: OPTIONS += -use-fuel
 tlean-hashmap_main: SUBDIR :=
 thol4-hashmap_main: OPTIONS +=
 
-transp-polonius_list: OPTIONS += -test-trans-units -no-split-files -no-state
-transp-polonius_list: SUBDIR := misc
+testp-polonius_list: OPTIONS += -test-trans-units -no-split-files -no-state
+testp-polonius_list: SUBDIR := misc
 tfstarp-polonius_list: OPTIONS +=
 tcoqp-polonius_list: OPTIONS +=
 tleanp-polonius_list: SUBDIR :=
@@ -180,8 +180,8 @@ tleanp-polonius_list: OPTIONS +=
 thol4p-polonius_list: SUBDIR := misc-polonius_list
 thol4p-polonius_list: OPTIONS +=
 
-trans-constants: OPTIONS += -test-trans-units -no-split-files -no-state
-trans-constants: SUBDIR := misc
+test-constants: OPTIONS += -test-trans-units -no-split-files -no-state
+test-constants: SUBDIR := misc
 tfstar-constants: OPTIONS +=
 tcoq-constants: OPTIONS +=
 tlean-constants: SUBDIR :=
@@ -189,8 +189,8 @@ tlean-constants: OPTIONS +=
 thol4-constants: SUBDIR := misc-constants
 thol4-constants: OPTIONS +=
 
-trans-external: OPTIONS += -test-trans-units
-trans-external: SUBDIR := misc
+test-external: OPTIONS += -test-trans-units
+test-external: SUBDIR := misc
 tfstar-external: OPTIONS +=
 tcoq-external: OPTIONS +=
 tlean-external: SUBDIR :=
@@ -199,25 +199,25 @@ thol4-external: SUBDIR := misc-external
 thol4-external: OPTIONS +=
 
 BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
-transp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units
-transp-betree_main: SUBDIR:=betree
+testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units
+testp-betree_main: SUBDIR:=betree
 tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
 tcoqp-betree_main: OPTIONS += -use-fuel
 tleanp-betree_main: SUBDIR :=
 tleanp-betree_main: OPTIONS +=
 thol4-betree_main: OPTIONS +=
 
-# Additional test on the betree: translate it without `-backward-no-state-update`.
+# Additional, *c*ustom test on the betree: translate it without `-backward-no-state-update`.
 # This generates very ugly code, but is good to test the translation.
-.PHONY: test-transp-betree_main
-test-transp-betree_main: transp-betree_main
-test-transp-betree_main: OPTIONS += -backend fstar -test-trans-units
-test-transp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
-test-transp-betree_main: BACKEND_SUBDIR := "fstar"
-test-transp-betree_main: SUBDIR:=betree_back_stateful
-test-transp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-test-transp-betree_main: FILE = betree_main
-test-transp-betree_main:
+.PHONY: ctest-testp-betree_main
+ctest-testp-betree_main: testp-betree_main
+ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units
+ctest-testp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
+ctest-testp-betree_main: BACKEND_SUBDIR := "fstar"
+ctest-testp-betree_main: SUBDIR:=betree_back_stateful
+ctest-testp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
+ctest-testp-betree_main: FILE = betree_main
+ctest-testp-betree_main:
 	$(AENEAS_CMD)
 
 # Generic rules to extract the LLBC from a rust file
@@ -234,20 +234,20 @@ gen-llbcp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
 gen-llbcp-%:
 	$(CHARON_CMD)
 
-# Generic rules to test the translation of an LLBC file.
+# Generic rules to test the testlation of an LLBC file.
 # Note that the files requiring the Polonius borrow-checker are generated
 # in the tests-polonius subdirectory.
-.PHONY: trans-%
-trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
-trans-%: FILE = $*
-trans-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-%
+.PHONY: test-%
+test-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
+test-%: FILE = $*
+test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-%
 	echo "# Test $* done"
 
 # "p" stands for "Polonius"
-.PHONY: transp-%
-transp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
-transp-%: FILE = $*
-transp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
+.PHONY: testp-%
+testp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
+testp-%: FILE = $*
+testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-%
 	echo "# Test $* done"
 
 .PHONY: tfstar-%