diff options
| author | Son Ho | 2022-06-20 06:21:57 +0200 |
|---|---|---|
| committer | Son Ho | 2022-06-20 06:21:57 +0200 |
| commit | 4c3a164ed570ecfa721255519554911754913271 (patch) | |
| tree | ebb622998a13f79662f92b02c5f2600c928e7f62 /tests/Makefile | |
| parent | f51f4c5d883691ef73094a79b4316255191627b0 (diff) | |
Add makefiles to test the F* files
Diffstat (limited to '')
| -rw-r--r-- | tests/Makefile | 19 | ||||
| -rw-r--r-- | tests/Makefile.template | 51 |
2 files changed, 70 insertions, 0 deletions
diff --git a/tests/Makefile b/tests/Makefile new file mode 100644 index 00000000..a9c170f7 --- /dev/null +++ b/tests/Makefile @@ -0,0 +1,19 @@ +ALL_DIRS ?= $(filter-out Makefile%, $(wildcard *)) + +VERIFY_DIRS = $(addprefix verif-,$(ALL_DIRS)) + +CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS)) + +.PHONY: all +all: $(VERIFY_DIRS) + +.PHONY: clean +clean: $(CLEAN_DIRS) + +.PHONY: verif-% +verif-%: + cd $* && make all + +.PHONY: clean-% +clean-%: + cd $* && make clean diff --git a/tests/Makefile.template b/tests/Makefile.template new file mode 100644 index 00000000..fed1a280 --- /dev/null +++ b/tests/Makefile.template @@ -0,0 +1,51 @@ +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)) \ + --extract 'krml:*' \ + --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \ + > $@ + +.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/* |