Regroup and sort makefile test entries

1 files changed, 85 insertions, 95 deletions

diff --git a/Makefile b/Makefile
index 32388a5e..c2f42c75 100644
--- a/Makefile
+++ b/Makefile
@@ -108,13 +108,21 @@ clean: clean-generated
 test: build-dev test-all
 
 .PHONY: test-all
-test-all: test-no_nested_borrows test-paper \
-	test-hashmap test-hashmap_main \
-	test-external test-constants \
-	test-polonius_list test-betree_main \
+test-all: \
+	test-arrays \
+	test-betree_main \
 	ctest-test-betree_main \
+	test-bitwise \
+	test-constants \
+	test-demo \
+	test-external \
+	test-hashmap \
+	test-hashmap_main \
 	test-loops \
-	test-arrays test-traits test-bitwise test-demo
+	test-no_nested_borrows \
+	test-paper \
+	test-polonius_list \
+	test-traits
 
 .PHONY: clean-generated
 clean-generated:
@@ -142,120 +150,95 @@ endif
 # The command to run Aeneas on the proper llbc file
 AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BACKEND)/$(SUBDIR) -backend $(BACKEND) $(OPTIONS)
 
+# Subdirs
+test-arrays: SUBDIR := arrays
+tlean-arrays: SUBDIR :=
 
-# Add specific options to some tests
-test-no_nested_borrows test-paper: \
-	OPTIONS += -test-trans-units
-test-no_nested_borrows test-paper: SUBDIR := misc
-tfstar-no_nested_borrows tfstar-paper:
+test-betree_main: SUBDIR := betree
+tlean-betree_main: SUBDIR :=
+
+ctest-test-betree_main: SUBDIR := betree_back_stateful
+
+test-bitwise: SUBDIR := misc
+tlean-bitwise: SUBDIR :=
+thol4-bitwise: SUBDIR := misc-bitwise
+
+test-constants: SUBDIR := misc
+tlean-constants: SUBDIR :=
+thol4-constants: SUBDIR := misc-constants
+
+test-demo: SUBDIR := demo
+tlean-demo: SUBDIR := Demo
+
+test-external: SUBDIR := misc
+tlean-external: SUBDIR :=
+thol4-external: SUBDIR := misc-external
+
+test-hashmap: SUBDIR := hashmap
+tlean-hashmap: SUBDIR :=
+
+test-hashmap_main: SUBDIR := hashmap_on_disk
+tlean-hashmap_main: SUBDIR :=
+
+test-loops: SUBDIR := misc
+tlean-loops: SUBDIR :=
+thol4-loops: SUBDIR := misc-loops
+
+test-no_nested_borrows: SUBDIR := misc
 tlean-no_nested_borrows: SUBDIR :=
-tlean-paper: SUBDIR :=
 thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows
+
+test-paper: SUBDIR := misc
+tlean-paper: SUBDIR :=
 thol4-paper: SUBDIR := misc-paper
 
-test-arrays: OPTIONS +=
-test-arrays: SUBDIR := arrays
-tfstar-arrays: OPTIONS += -decreases-clauses -template-clauses -split-files
-tcoq-arrays: OPTIONS += -use-fuel
-tlean-arrays: SUBDIR :=
-tlean-arrays: OPTIONS +=
-thol4-arrays: OPTIONS +=
+test-polonius_list: SUBDIR := misc
+tlean-polonius_list: SUBDIR :=
+thol4-polonius_list: SUBDIR := misc-polonius_list
 
-test-traits: OPTIONS +=
 test-traits: SUBDIR := traits
-tfstar-traits: OPTIONS += -decreases-clauses -template-clauses
-tcoq-traits: OPTIONS +=
 tlean-traits: SUBDIR :=
-tlean-traits: OPTIONS +=
-thol4-traits: OPTIONS +=
 
-test-loops: OPTIONS +=
-test-loops: SUBDIR := misc
-tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files
-tcoq-loops: OPTIONS += -use-fuel
-tlean-loops: SUBDIR :=
-thol4-loops: SUBDIR := misc-loops
+# Add specific options to some tests
+# TODO: reactivate -test-trans-units for hashmap and hashmap_main
+tfstar-arrays: OPTIONS += -decreases-clauses -template-clauses -split-files
+tcoq-arrays: OPTIONS += -use-fuel
+
+test-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
+tfstar-betree_main: OPTIONS += -decreases-clauses -template-clauses
+tcoq-betree_main: OPTIONS += -use-fuel
+
+ctest-test-betree_main: OPTIONS += -test-trans-units -state -split-files
+ctest-test-betree_main: OPTIONS += -decreases-clauses -template-clauses
+
+test-bitwise: OPTIONS += -test-trans-units
+
+test-constants: OPTIONS += -test-trans-units
 
-test-demo: OPTIONS +=
-test-demo: SUBDIR := demo
 tfstar-demo: OPTIONS += -use-fuel
 tcoq-demo: OPTIONS += -use-fuel
-tlean-demo: SUBDIR := Demo
-thol4-demo: OPTIONS +=
 
-# TODO: reactivate -test-trans-units
+test-external: OPTIONS += -test-trans-units -state -split-files
+
 test-hashmap: OPTIONS += -split-files
-test-hashmap: SUBDIR := hashmap
 tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
 tcoq-hashmap: OPTIONS += -use-fuel
-tlean-hashmap: SUBDIR :=
 tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hashmap.lean file: we do not want to overwrite it
-thol4-hashmap: OPTIONS +=
 
-# TODO: reactivate -test-trans-units
 test-hashmap_main: OPTIONS += -state -split-files
-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 +=
 
-test-polonius_list: OPTIONS += -test-trans-units
-test-polonius_list: SUBDIR := misc
-tfstar-polonius_list: OPTIONS +=
-tcoq-polonius_list: OPTIONS +=
-tlean-polonius_list: SUBDIR :=
-tlean-polonius_list: OPTIONS +=
-thol4-polonius_list: SUBDIR := misc-polonius_list
-thol4-polonius_list: OPTIONS +=
+tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files
+tcoq-loops: OPTIONS += -use-fuel
 
-test-constants: OPTIONS += -test-trans-units
-test-constants: SUBDIR := misc
-tfstar-constants: OPTIONS +=
-tcoq-constants: OPTIONS +=
-tlean-constants: SUBDIR :=
-tlean-constants: OPTIONS +=
-thol4-constants: SUBDIR := misc-constants
-thol4-constants: OPTIONS +=
+test-no_nested_borrows: OPTIONS += -test-trans-units
 
-test-external: OPTIONS += -test-trans-units -state -split-files
-test-external: SUBDIR := misc
-tfstar-external: OPTIONS +=
-tcoq-external: OPTIONS +=
-tlean-external: SUBDIR :=
-tlean-external: OPTIONS +=
-thol4-external: SUBDIR := misc-external
-thol4-external: OPTIONS +=
+test-paper: OPTIONS += -test-trans-units
 
-test-bitwise: OPTIONS += -test-trans-units
-test-bitwise: SUBDIR := misc
-tfstar-bitwise: OPTIONS +=
-tcoq-bitwise: OPTIONS +=
-tlean-bitwise: SUBDIR :=
-tlean-bitwise: OPTIONS +=
-thol4-bitwise: SUBDIR := misc-bitwise
-thol4-bitwise: OPTIONS +=
-
-BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
-test-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
-test-betree_main: SUBDIR:=betree
-tfstar-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
-tcoq-betree_main: OPTIONS += -use-fuel
-tlean-betree_main: SUBDIR :=
-tlean-betree_main: OPTIONS +=
-thol4-betree_main: OPTIONS +=
+test-polonius_list: OPTIONS += -test-trans-units
 
-# 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: ctest-test-betree_main
-ctest-test-betree_main: test-betree_main
-ctest-test-betree_main: OPTIONS += -test-trans-units -state -split-files
-ctest-test-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
-ctest-test-betree_main: BACKEND := fstar
-ctest-test-betree_main: SUBDIR:=betree_back_stateful
-ctest-test-betree_main: FILE = betree_main
-ctest-test-betree_main:
-	$(AENEAS_CMD)
+tfstar-traits: OPTIONS += -decreases-clauses -template-clauses
 
 # 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
@@ -290,10 +273,17 @@ tlean-%:
 thol4-%: BACKEND := hol4
 thol4-%:
 	echo Ignoring the $* test for HOL4
-
-#thol4-%:
 #	$(AENEAS_CMD)
 
+# 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: ctest-test-betree_main
+ctest-test-betree_main: test-betree_main
+ctest-test-betree_main: FILE = betree_main
+ctest-test-betree_main: BACKEND := fstar
+ctest-test-betree_main:
+	$(AENEAS_CMD)
+
 # Nix - TODO: add the lean tests
 .PHONY: nix
 nix: