summaryrefslogtreecommitdiff
path: root/tests/fstar-split/arrays/Makefile
diff options
context:
space:
mode:
authorSon Ho2024-02-02 23:33:20 +0100
committerSon Ho2024-02-02 23:33:20 +0100
commit7ecf28dc36f724a4ab4b3b4976421e4e4c397f3b (patch)
treead9f8cfb3c035fb86623d83d24e5590bb7bbd8a4 /tests/fstar-split/arrays/Makefile
parent5cf7d9c0d6b0bc77f2219e7b8b29badce26d51e8 (diff)
Rename and regenerate some files
Diffstat (limited to 'tests/fstar-split/arrays/Makefile')
-rw-r--r--tests/fstar-split/arrays/Makefile49
1 files changed, 49 insertions, 0 deletions
diff --git a/tests/fstar-split/arrays/Makefile b/tests/fstar-split/arrays/Makefile
new file mode 100644
index 00000000..fa7d1f36
--- /dev/null
+++ b/tests/fstar-split/arrays/Makefile
@@ -0,0 +1,49 @@
+# 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/*