From e3b009223d0910c9e422f728ba22e5e9356f49b2 Mon Sep 17 00:00:00 2001
From: Lucas McDonald <lucasmcdonald3@gmail.com>
Date: Mon, 11 Dec 2023 16:02:54 -0800
Subject: [PATCH] bw compatible

---
 TestModels/SharedMakefile.mk | 40 +++++++++++++++++++++---------------
 1 file changed, 23 insertions(+), 17 deletions(-)

diff --git a/TestModels/SharedMakefile.mk b/TestModels/SharedMakefile.mk
index a35f114c8..4ee52c3cc 100644
--- a/TestModels/SharedMakefile.mk
+++ b/TestModels/SharedMakefile.mk
@@ -97,23 +97,26 @@ dafny-reportgenerator:
 # and can be the same for all such runtimes.
 # Since such targets are all shared,
 # this is tractable.
+transpile_implementation: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src/Index.dfy)
 transpile_implementation:
 	dafny \
-            -vcsCores:$(CORES) \
-            -compileTarget:$(TARGET) \
-            -spillTargetCode:3 \
-            -compile:0 \
-            -optimizeErasableDatatypeWrapper:0 \
-            $(COMPILE_SUFFIX_OPTION) \
-            -quantifierSyntax:3 \
-            -unicodeChar:0 \
-            -functionSyntax:3 \
-            -useRuntimeLib \
-            -out $(OUT) \
-            $(DOT_NAMESPACE_SRC_INDEX) \
-            -library:$(PROJECT_ROOT)/dafny-dependencies/StandardLibrary/src/Index.dfy \
-            $(patsubst %, -library:$(PROJECT_ROOT)/%/src/Index.dfy, $(LIBRARIES))
-
+        -vcsCores:$(CORES) \
+        -compileTarget:$(TARGET) \
+        -spillTargetCode:3 \
+        -compile:0 \
+        -optimizeErasableDatatypeWrapper:0 \
+        $(COMPILE_SUFFIX_OPTION) \
+        -quantifierSyntax:3 \
+        -unicodeChar:0 \
+        -functionSyntax:3 \
+        -useRuntimeLib \
+        -out $(OUT) \
+        $(SRC_INDEX_TRANSPILE) \
+        -library:$(PROJECT_ROOT)/dafny-dependencies/StandardLibrary/src/Index.dfy \
+        $(patsubst %, -library:$(PROJECT_ROOT)/%/src/Index.dfy, $(LIBRARIES))
+
+transpile_test: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src/Index.dfy)
+transpile_test: TEST_INDEX_TRANSPILE=$(if $(TEST_INDEX),$(TEST_INDEX),`find ./test -name '*.dfy'`)
 transpile_test:
 	dafny \
 		-vcsCores:$(CORES) \
@@ -128,8 +131,8 @@ transpile_test:
 		-functionSyntax:3 \
 		-useRuntimeLib \
 		-out $(OUT) \
-		$(DOT_NAMESPACE_TEST_INDEX) \
-		-library:$(DOT_NAMESPACE_SRC_INDEX)
+		$(TEST_INDEX_TRANSPILE) \
+		-library:$(SRC_INDEX_TRANSPILE)
 
 transpile_dependencies:
 	$(MAKE) -C $(STANDARD_LIBRARY_PATH) transpile_implementation_$(LANG)
@@ -225,10 +228,13 @@ transpile_net: | transpile_implementation_net transpile_test_net transpile_depen
 
 transpile_implementation_net: TARGET=cs
 transpile_implementation_net: OUT=runtimes/net/ImplementationFromDafny
+transpile_implementation_net: SRC_INDEX=$(DOT_NAMESPACE_SRC_INDEX)
 transpile_implementation_net: transpile_implementation
 
 transpile_test_net: TARGET=cs
 transpile_test_net: OUT=runtimes/net/tests/TestsFromDafny
+transpile_test_net: SRC_INDEX=$(DOT_NAMESPACE_SRC_INDEX)
+transpile_test_net: TEST_INDEX=$(DOT_NAMESPACE_TEST_INDEX)
 transpile_test_net: transpile_test
 
 transpile_dependencies_net: LANG=net