diff options
Diffstat (limited to 'tests/fstar')
| -rw-r--r-- | tests/fstar/Makefile | 10 | ||||
| -rw-r--r-- | tests/fstar/Makefile.template | 3 | ||||
| -rw-r--r-- | tests/fstar/betree/Makefile | 1 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/Makefile | 1 | ||||
| -rw-r--r-- | tests/fstar/hashmap/Makefile | 1 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/Makefile | 1 | ||||
| -rw-r--r-- | tests/fstar/misc/Makefile | 1 |
7 files changed, 16 insertions, 2 deletions
diff --git a/tests/fstar/Makefile b/tests/fstar/Makefile index a9c170f7..aad3354e 100644 --- a/tests/fstar/Makefile +++ b/tests/fstar/Makefile @@ -4,8 +4,10 @@ VERIFY_DIRS = $(addprefix verif-,$(ALL_DIRS)) CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS)) +COPY_MAKEFILES = $(addprefix copy-makefile-,$(ALL_DIRS)) + .PHONY: all -all: $(VERIFY_DIRS) +all: $(COPY_MAKEFILES) $(VERIFY_DIRS) .PHONY: clean clean: $(CLEAN_DIRS) @@ -14,6 +16,12 @@ clean: $(CLEAN_DIRS) verif-%: cd $* && make all +.PHONY: copy-makefile-% +copy-makefile-%: + rm -f $*/Makefile + echo "# This file was automatically generated - modify ../Makefile.template instead" >> $*/Makefile + cat Makefile.template >> $*/Makefile + .PHONY: clean-% clean-%: cd $* && make clean diff --git a/tests/fstar/Makefile.template b/tests/fstar/Makefile.template index a16b0edb..14790d6d 100644 --- a/tests/fstar/Makefile.template +++ b/tests/fstar/Makefile.template @@ -8,7 +8,8 @@ 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_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) diff --git a/tests/fstar/betree/Makefile b/tests/fstar/betree/Makefile index 14790d6d..fa7d1f36 100644 --- a/tests/fstar/betree/Makefile +++ b/tests/fstar/betree/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead INCLUDE_DIRS = . FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) diff --git a/tests/fstar/betree_back_stateful/Makefile b/tests/fstar/betree_back_stateful/Makefile index 14790d6d..fa7d1f36 100644 --- a/tests/fstar/betree_back_stateful/Makefile +++ b/tests/fstar/betree_back_stateful/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead INCLUDE_DIRS = . FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) diff --git a/tests/fstar/hashmap/Makefile b/tests/fstar/hashmap/Makefile index 14790d6d..fa7d1f36 100644 --- a/tests/fstar/hashmap/Makefile +++ b/tests/fstar/hashmap/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead INCLUDE_DIRS = . FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) diff --git a/tests/fstar/hashmap_on_disk/Makefile b/tests/fstar/hashmap_on_disk/Makefile index 14790d6d..fa7d1f36 100644 --- a/tests/fstar/hashmap_on_disk/Makefile +++ b/tests/fstar/hashmap_on_disk/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead INCLUDE_DIRS = . FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) diff --git a/tests/fstar/misc/Makefile b/tests/fstar/misc/Makefile index 14790d6d..fa7d1f36 100644 --- a/tests/fstar/misc/Makefile +++ b/tests/fstar/misc/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead INCLUDE_DIRS = . FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) |