diff options
| author | Nadrieril | 2024-05-23 14:06:51 +0200 |
|---|---|---|
| committer | Guillaume Boisseau | 2024-05-24 14:24:38 +0200 |
| commit | b8bdf14f3e4b25578d107160161f5bd2b548a113 (patch) | |
| tree | fb5c3fa7e377655bdfbb9859b612f2d413907013 /tests/fstar/betree_back_stateful/Makefile | |
| parent | b953b89f9739c6703c49667781f5509b1b2a3898 (diff) | |
Remove secondary betree test
Opened https://github.com/AeneasVerif/aeneas/issues/196 to remember to
add a more adequate replacement test.
Diffstat (limited to 'tests/fstar/betree_back_stateful/Makefile')
| -rw-r--r-- | tests/fstar/betree_back_stateful/Makefile | 49 |
1 files changed, 0 insertions, 49 deletions
diff --git a/tests/fstar/betree_back_stateful/Makefile b/tests/fstar/betree_back_stateful/Makefile deleted file mode 100644 index fa7d1f36..00000000 --- a/tests/fstar/betree_back_stateful/Makefile +++ /dev/null @@ -1,49 +0,0 @@ -# This file was automatically generated - modify ../Makefile.template instead -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_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) - -# 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/* |