summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Makefile5
-rw-r--r--tests/hashmap/Hashmap.Clauses.fst (renamed from tests/Hashmap.Clauses.fst)0
2 files changed, 4 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 3d318ebc..afbdd832 100644
--- a/Makefile
+++ b/Makefile
@@ -8,6 +8,7 @@ DEST_DIR=tests/
# - insert calls to the normalizer in the translated code to test the
# generated unit functions
TRANS_OPTIONS:=-test-trans-units
+SUBDIR:=
# Build the project and test it
.PHONY: build-test
@@ -24,7 +25,9 @@ test: build translate-no_nested_borrows translate-hashmap
# Add specific options to some tests
translate-no_nested_borrows: TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split -no-decreases-clauses
+translate-no_nested_borrows: SUBDIR:=misc
translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses
+translate-hashmap: SUBDIR:=hashmap
# Generic rule to extract the CFIM from a rust file
.PHONY: gen-cfim-%
@@ -34,7 +37,7 @@ gen-cfim-%: build
# Generic rule to test the translation on a CFIM file
.PHONY: translate-%
translate-%: gen-cfim-%
- dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.cfim -dest $(DEST_DIR) $(TRANS_OPTIONS)
+ dune exec -- src/main.exe $(CHARON_TESTS_DIR)/$*.cfim -dest $(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
.PHONY: doc
doc:
diff --git a/tests/Hashmap.Clauses.fst b/tests/hashmap/Hashmap.Clauses.fst
index ef7793f1..ef7793f1 100644
--- a/tests/Hashmap.Clauses.fst
+++ b/tests/hashmap/Hashmap.Clauses.fst