summaryrefslogtreecommitdiff
path: root/tests/fstar/hashmap_main/Makefile
diff options
context:
space:
mode:
authorGuillaume Boisseau2024-05-28 11:56:39 +0200
committerGitHub2024-05-28 11:56:39 +0200
commitef7792c106a1f33397c206fcb5124b5ddfe64378 (patch)
treea72fae46702fc4c2eb32e1361a2538eb7a5f5545 /tests/fstar/hashmap_main/Makefile
parent4f26c7f6f1e554d8ec2f46e868d5dc66c4160d16 (diff)
parentc4d2af051c18c4c81b1e57a45210c37c89c8330f (diff)
Merge pull request #213 from AeneasVerif/cleanup-tests
Diffstat (limited to 'tests/fstar/hashmap_main/Makefile')
-rw-r--r--tests/fstar/hashmap_main/Makefile49
1 files changed, 0 insertions, 49 deletions
diff --git a/tests/fstar/hashmap_main/Makefile b/tests/fstar/hashmap_main/Makefile
deleted file mode 100644
index fa7d1f36..00000000
--- a/tests/fstar/hashmap_main/Makefile
+++ /dev/null
@@ -1,49 +0,0 @@
-# This file was automatically generated - modify ../Makefile.template instead
-INCLUDE_DIRS = .
-
-FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
-
-FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
-
-FSTAR_OPTIONS = $(FSTAR_HINTS) \
- --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
- --warn_error '+241@247+285-274' \
-
-FSTAR_EXE ?= fstar.exe
-FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj
-
-FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
-
-# The F* roots are used to compute the dependency graph, and generate the .depend file
-FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
-
-# Build all the files
-all: $(addprefix obj/,$(addsuffix .checked,$(FSTAR_ROOTS)))
-
-# This is the right way to ensure the .depend file always gets re-built.
-ifeq (,$(filter %-in,$(MAKECMDGOALS)))
-ifndef NODEPEND
-ifndef MAKE_RESTARTS
-.depend: .FORCE
- $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) > $@
-
-.PHONY: .FORCE
-.FORCE:
-endif
-endif
-
-include .depend
-endif
-
-# For the interactive mode
-%.fst-in %.fsti-in:
- @echo $(FSTAR_OPTIONS)
-
-# Generete the .checked files in batch mode
-%.checked:
- $(FSTAR) $(FSTAR_OPTIONS) $< && \
- touch -c $@
-
-.PHONY: clean
-clean:
- rm -f obj/*