From cc8cd4b9d55e21dd50fac7714203ab8a8f06242b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 16 Nov 2022 14:10:44 +0100
Subject: Add the aeneas-verify-fstar derivation

---
 tests/fstar/betree/Makefile               | 3 ++-
 tests/fstar/betree_back_stateful/Makefile | 3 ++-
 tests/fstar/hashmap/Makefile              | 3 ++-
 tests/fstar/hashmap_on_disk/Makefile      | 3 ++-
 tests/fstar/misc/Makefile                 | 3 ++-
 5 files changed, 10 insertions(+), 5 deletions(-)

(limited to 'tests/fstar')

diff --git a/tests/fstar/betree/Makefile b/tests/fstar/betree/Makefile
index a16b0edb..14790d6d 100644
--- a/tests/fstar/betree/Makefile
+++ b/tests/fstar/betree/Makefile
@@ -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_back_stateful/Makefile b/tests/fstar/betree_back_stateful/Makefile
index a16b0edb..14790d6d 100644
--- a/tests/fstar/betree_back_stateful/Makefile
+++ b/tests/fstar/betree_back_stateful/Makefile
@@ -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/hashmap/Makefile b/tests/fstar/hashmap/Makefile
index a16b0edb..14790d6d 100644
--- a/tests/fstar/hashmap/Makefile
+++ b/tests/fstar/hashmap/Makefile
@@ -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/hashmap_on_disk/Makefile b/tests/fstar/hashmap_on_disk/Makefile
index a16b0edb..14790d6d 100644
--- a/tests/fstar/hashmap_on_disk/Makefile
+++ b/tests/fstar/hashmap_on_disk/Makefile
@@ -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/misc/Makefile b/tests/fstar/misc/Makefile
index a16b0edb..14790d6d 100644
--- a/tests/fstar/misc/Makefile
+++ b/tests/fstar/misc/Makefile
@@ -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)
 
-- 
cgit v1.2.3