diff options
author | Son Ho | 2022-11-09 18:04:03 +0100 |
---|---|---|
committer | Son HO | 2022-11-10 11:35:30 +0100 |
commit | 8b6f8e5fb85bcd1b3257550270c4c857d4ee7f55 (patch) | |
tree | b0090425eb850af3b5c8dc1d4f6aa1eafe2c8e1a /tests/betree_back_stateful/Makefile | |
parent | b970183881379ff676b232e47e353e924de8cfdd (diff) |
Implement the generation of stateful backward functions (controlled by an option)
Diffstat (limited to '')
-rw-r--r-- | tests/betree_back_stateful/Makefile | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/tests/betree_back_stateful/Makefile b/tests/betree_back_stateful/Makefile new file mode 100644 index 00000000..a16b0edb --- /dev/null +++ b/tests/betree_back_stateful/Makefile @@ -0,0 +1,47 @@ +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_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/* |