diff options
Diffstat (limited to '')
| -rw-r--r-- | Makefile | 9 | ||||
| -rw-r--r-- | tests/Makefile.template | 21 | ||||
| -rw-r--r-- | tests/betree/Makefile | 21 | ||||
| -rw-r--r-- | tests/hashmap/Makefile | 21 | ||||
| -rw-r--r-- | tests/hashmap_on_disk/Makefile | 21 | ||||
| -rw-r--r-- | tests/misc/Makefile | 21 |
6 files changed, 57 insertions, 57 deletions
@@ -1,3 +1,8 @@ +ifeq (3.81,$(MAKE_VERSION)) + $(error You seem to be using the OSX antiquated Make version. Hint: brew \ + install make, then invoke gmake instead of make) +endif + all: build-test-verify CHARON_HOME = ../charon @@ -37,7 +42,7 @@ test: build trans-no_nested_borrows trans-paper \ # Verify the F* files generated by the translation .PHONY: verify verify: build test - cd tests && make all + cd tests && $(MAKE) all # Reformat the project .PHONY: format @@ -72,7 +77,7 @@ trans-nll-betree_main: SUBDIR:=betree # vary with the test files. .PHONY: gen-llbc-% gen-llbc-%: build - cd $(CHARON_HOME) && make test-$* + cd $(CHARON_HOME) && $(MAKE) test-$* # Generic rule to test the translation of an LLBC file. # Note that the non-linear lifetime files are generated in the tests-nll subdirectory. diff --git a/tests/Makefile.template b/tests/Makefile.template index ea838d2d..a16b0edb 100644 --- a/tests/Makefile.template +++ b/tests/Makefile.template @@ -5,17 +5,19 @@ 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 \ + --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ --warn_error '+241@247+285-274' \ - --cache_dir obj -FSTAR_NO_FLAGS = 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 @@ -32,16 +34,13 @@ include .depend endif # For the interactive mode -%.fst %.fsti: - $(FSTAR) $@ +%.fst-in %.fsti-in: + @echo $(FSTAR_OPTIONS) -# Generete the .checked files in bash mode +# Generete the .checked files in batch mode %.checked: - $(FSTAR) $(FSTAR_FLAGS) $* && \ - touch -c $* - -# Build all the files -all: $(ALL_CHECKED_FILES) + $(FSTAR) $(FSTAR_OPTIONS) $< && \ + touch -c $@ .PHONY: clean clean: diff --git a/tests/betree/Makefile b/tests/betree/Makefile index ea838d2d..a16b0edb 100644 --- a/tests/betree/Makefile +++ b/tests/betree/Makefile @@ -5,17 +5,19 @@ 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 \ + --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ --warn_error '+241@247+285-274' \ - --cache_dir obj -FSTAR_NO_FLAGS = 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 @@ -32,16 +34,13 @@ include .depend endif # For the interactive mode -%.fst %.fsti: - $(FSTAR) $@ +%.fst-in %.fsti-in: + @echo $(FSTAR_OPTIONS) -# Generete the .checked files in bash mode +# Generete the .checked files in batch mode %.checked: - $(FSTAR) $(FSTAR_FLAGS) $* && \ - touch -c $* - -# Build all the files -all: $(ALL_CHECKED_FILES) + $(FSTAR) $(FSTAR_OPTIONS) $< && \ + touch -c $@ .PHONY: clean clean: diff --git a/tests/hashmap/Makefile b/tests/hashmap/Makefile index ea838d2d..a16b0edb 100644 --- a/tests/hashmap/Makefile +++ b/tests/hashmap/Makefile @@ -5,17 +5,19 @@ 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 \ + --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ --warn_error '+241@247+285-274' \ - --cache_dir obj -FSTAR_NO_FLAGS = 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 @@ -32,16 +34,13 @@ include .depend endif # For the interactive mode -%.fst %.fsti: - $(FSTAR) $@ +%.fst-in %.fsti-in: + @echo $(FSTAR_OPTIONS) -# Generete the .checked files in bash mode +# Generete the .checked files in batch mode %.checked: - $(FSTAR) $(FSTAR_FLAGS) $* && \ - touch -c $* - -# Build all the files -all: $(ALL_CHECKED_FILES) + $(FSTAR) $(FSTAR_OPTIONS) $< && \ + touch -c $@ .PHONY: clean clean: diff --git a/tests/hashmap_on_disk/Makefile b/tests/hashmap_on_disk/Makefile index ea838d2d..a16b0edb 100644 --- a/tests/hashmap_on_disk/Makefile +++ b/tests/hashmap_on_disk/Makefile @@ -5,17 +5,19 @@ 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 \ + --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ --warn_error '+241@247+285-274' \ - --cache_dir obj -FSTAR_NO_FLAGS = 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 @@ -32,16 +34,13 @@ include .depend endif # For the interactive mode -%.fst %.fsti: - $(FSTAR) $@ +%.fst-in %.fsti-in: + @echo $(FSTAR_OPTIONS) -# Generete the .checked files in bash mode +# Generete the .checked files in batch mode %.checked: - $(FSTAR) $(FSTAR_FLAGS) $* && \ - touch -c $* - -# Build all the files -all: $(ALL_CHECKED_FILES) + $(FSTAR) $(FSTAR_OPTIONS) $< && \ + touch -c $@ .PHONY: clean clean: diff --git a/tests/misc/Makefile b/tests/misc/Makefile index ea838d2d..a16b0edb 100644 --- a/tests/misc/Makefile +++ b/tests/misc/Makefile @@ -5,17 +5,19 @@ 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 \ + --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ --warn_error '+241@247+285-274' \ - --cache_dir obj -FSTAR_NO_FLAGS = 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 @@ -32,16 +34,13 @@ include .depend endif # For the interactive mode -%.fst %.fsti: - $(FSTAR) $@ +%.fst-in %.fsti-in: + @echo $(FSTAR_OPTIONS) -# Generete the .checked files in bash mode +# Generete the .checked files in batch mode %.checked: - $(FSTAR) $(FSTAR_FLAGS) $* && \ - touch -c $* - -# Build all the files -all: $(ALL_CHECKED_FILES) + $(FSTAR) $(FSTAR_OPTIONS) $< && \ + touch -c $@ .PHONY: clean clean: |