diff options
| author | Sidney Congard | 2022-06-30 14:54:15 +0200 |
|---|---|---|
| committer | Sidney Congard | 2022-06-30 14:54:15 +0200 |
| commit | fdbbb82ff89b1d5141ec63bc2385936da3de3616 (patch) | |
| tree | d48e3fa933280e8a275d2cfdab8f126e920e5f13 /tests/hashmap/Makefile | |
| parent | 47691de8fe3dc32a29663d4d8343eb415ce1d81e (diff) | |
| parent | 4f33892c81cdaf6aefaad9b7cef1456dcfead67c (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/Makefile | 48 |
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/* |