diff options
author | Son HO | 2024-03-08 16:51:40 +0100 |
---|---|---|
committer | GitHub | 2024-03-08 16:51:40 +0100 |
commit | 169d011cbfa83d853d0148bbf6b946e6ccbe4c4c (patch) | |
tree | ed8953634d14313d5b7d6ad204343d64eb990baf /backends/fstar/Makefile | |
parent | b604bb9935007a1f0e9c7f556f8196f0e14c85ce (diff) | |
parent | 873deb005b394aca3090497e6c21ab9f8c2676be (diff) |
Merge pull request #83 from AeneasVerif/son/backs
Remove the option to split the forward/backward functions
Diffstat (limited to 'backends/fstar/Makefile')
-rw-r--r-- | backends/fstar/Makefile | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/backends/fstar/Makefile b/backends/fstar/Makefile new file mode 100644 index 00000000..a16b0edb --- /dev/null +++ b/backends/fstar/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/* |