From 8624061f1c6dc9ff1f1ece05f16d09e59a825325 Mon Sep 17 00:00:00 2001
From: Alistair Michael <alistair.michael@uq.edu.au>
Date: Mon, 4 Dec 2023 16:01:00 +1000
Subject: [PATCH] Support extra boogie files in tests

---
 src/main/scala/Main.scala        |  2 +-
 src/test/scala/SystemTests.scala | 19 ++++++++++---------
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/main/scala/Main.scala b/src/main/scala/Main.scala
index 3fb3f0139..c26c789bb 100644
--- a/src/main/scala/Main.scala
+++ b/src/main/scala/Main.scala
@@ -42,7 +42,7 @@ object Main {
       analysisResultsDot: Option[String]
   )
 
-  def main(args: Array[String]): Unit = {
+  def main(args: Iterable[String]): Unit = {
     val parser = ParserForClass[Config]
     val parsed = parser.constructEither(args.toSeq)
 
diff --git a/src/test/scala/SystemTests.scala b/src/test/scala/SystemTests.scala
index 8525be73b..33880c406 100644
--- a/src/test/scala/SystemTests.scala
+++ b/src/test/scala/SystemTests.scala
@@ -33,7 +33,7 @@ class SystemTests extends AnyFunSuite {
     val path = correctPath + "/" + p
     val variations = getSubdirectories(path)
     variations.foreach(t =>
-      test(p + "/" + t) {
+      test("correct/" + p + "/" + t) {
         runTest(correctPath, p, t, true)
       }
     )
@@ -43,7 +43,7 @@ class SystemTests extends AnyFunSuite {
     val path = incorrectPath + "/" + p
     val variations = getSubdirectories(path)
     variations.foreach(t =>
-      test(p + "/" + t) {
+      test("incorrect/" + p + "/" + t) {
         runTest(incorrectPath, p, t, false)
       }
     )
@@ -78,18 +78,19 @@ class SystemTests extends AnyFunSuite {
     val variationPath = directoryPath + variation + "/" + name
     val specPath = directoryPath + name + ".spec"
     val outPath = variationPath + ".bpl"
-    val ADTPath = variationPath + ".adt"
+        val ADTPath = variationPath + ".adt"
     val RELFPath = variationPath + ".relf"
     Logger.info(outPath)
     val timer = PerformanceTimer(s"test $name/$variation")
-    if (File(specPath).exists) {
-      Main.main(Array("--adt", ADTPath, "--relf", RELFPath, "--spec", specPath, "--output", outPath))
-    } else {
-      Main.main(Array("--adt", ADTPath, "--relf", RELFPath, "--output", outPath))
-    }
+
+    val args = mutable.ArrayBuffer("--adt", ADTPath, "--relf", RELFPath, "--output", outPath)
+    if (File(specPath).exists) args ++= Seq("--spec", specPath)
+
+    Main.main(args)
     val translateTime = timer.checkPoint("translate-boogie")
     Logger.info(outPath + " done")
-    val boogieResult = Seq("boogie", "/timeLimit:10", "/printVerifiedProceduresCount:0", "/useArrayAxioms", outPath).!!
+    val extraSpec = List.from(File(directoryPath).listFiles()).map(_.toString).filter(_.endsWith(".bpl")).filterNot(_.endsWith(outPath))
+    val boogieResult = (Seq("boogie", "/timeLimit:10", "/printVerifiedProceduresCount:0", "/useArrayAxioms", outPath) ++ extraSpec).!!
     val verifyTime = timer.checkPoint("verify")
     val resultPath = variationPath + "_result.txt"
     log(boogieResult, resultPath)