summaryrefslogtreecommitdiff
path: root/tests/hashmap/Makefile
diff options
context:
space:
mode:
authorSidney Congard2022-06-30 14:54:15 +0200
committerSidney Congard2022-06-30 14:54:15 +0200
commitfdbbb82ff89b1d5141ec63bc2385936da3de3616 (patch)
treed48e3fa933280e8a275d2cfdab8f126e920e5f13 /tests/hashmap/Makefile
parent47691de8fe3dc32a29663d4d8343eb415ce1d81e (diff)
parent4f33892c81cdaf6aefaad9b7cef1456dcfead67c (diff)
Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2
Complete the constants extraction by making all functions fail
Diffstat (limited to '')
-rw-r--r--tests/hashmap/Makefile48
1 files changed, 48 insertions, 0 deletions
diff --git a/tests/hashmap/Makefile b/tests/hashmap/Makefile
new file mode 100644
index 00000000..ea838d2d
--- /dev/null
+++ b/tests/hashmap/Makefile
@@ -0,0 +1,48 @@
+INCLUDE_DIRS = .
+
+FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
+
+FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
+
+FSTAR_OPTIONS = $(FSTAR_HINTS) \
+ --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+ --warn_error '+241@247+285-274' \
+ --cache_dir obj
+
+FSTAR_NO_FLAGS = fstar.exe
+
+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)
+
+# 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 %.fsti:
+ $(FSTAR) $@
+
+# Generete the .checked files in bash mode
+%.checked:
+ $(FSTAR) $(FSTAR_FLAGS) $* && \
+ touch -c $*
+
+# Build all the files
+all: $(ALL_CHECKED_FILES)
+
+.PHONY: clean
+clean:
+ rm -f obj/*