From 7b25a2ea118454e10b73d58d97c2c16de4959a3e Mon Sep 17 00:00:00 2001
From: 7i6ht <ruhstals@student.ethz.ch>
Date: Wed, 5 Feb 2025 15:34:33 +0100
Subject: [PATCH] Add tests

---
 .../branchTreeTests/allPathsCorrect.vpr       | 10 ++++
 .../branchTreeTests/allPathsCorrect_expected  |  1 +
 .../branchTreeTests/firstPathFails.vpr        | 19 +++++++
 .../branchTreeTests/firstPathFails_expected   | 10 ++++
 .../branchTreeTests/lastPathFails.vpr         | 19 +++++++
 .../branchTreeTests/lastPathFails_expected    | 10 ++++
 .../resources/branchTreeTests/noBranches.vpr  |  6 +++
 .../branchTreeTests/noBranches_expected       |  1 +
 src/test/resources/branchTreeTests/onlyIf.vpr | 14 ++++++
 .../resources/branchTreeTests/onlyIf_expected |  6 +++
 src/test/resources/branchTreeTests/while.vpr  | 13 +++++
 .../resources/branchTreeTests/while_expected  |  6 +++
 src/test/scala/BranchTreeTests.scala          | 49 +++++++++++++++++++
 13 files changed, 164 insertions(+)
 create mode 100644 src/test/resources/branchTreeTests/allPathsCorrect.vpr
 create mode 100644 src/test/resources/branchTreeTests/allPathsCorrect_expected
 create mode 100644 src/test/resources/branchTreeTests/firstPathFails.vpr
 create mode 100644 src/test/resources/branchTreeTests/firstPathFails_expected
 create mode 100644 src/test/resources/branchTreeTests/lastPathFails.vpr
 create mode 100644 src/test/resources/branchTreeTests/lastPathFails_expected
 create mode 100644 src/test/resources/branchTreeTests/noBranches.vpr
 create mode 100644 src/test/resources/branchTreeTests/noBranches_expected
 create mode 100644 src/test/resources/branchTreeTests/onlyIf.vpr
 create mode 100644 src/test/resources/branchTreeTests/onlyIf_expected
 create mode 100644 src/test/resources/branchTreeTests/while.vpr
 create mode 100644 src/test/resources/branchTreeTests/while_expected
 create mode 100644 src/test/scala/BranchTreeTests.scala

diff --git a/src/test/resources/branchTreeTests/allPathsCorrect.vpr b/src/test/resources/branchTreeTests/allPathsCorrect.vpr
new file mode 100644
index 000000000..f00c6ff1a
--- /dev/null
+++ b/src/test/resources/branchTreeTests/allPathsCorrect.vpr
@@ -0,0 +1,10 @@
+define P(z) z == true
+
+method foo(b: Bool) returns (z: Bool)
+ensures P(z) {
+    if (b) {
+        z := true
+    } else {
+        z := true
+    }
+}
\ No newline at end of file
diff --git a/src/test/resources/branchTreeTests/allPathsCorrect_expected b/src/test/resources/branchTreeTests/allPathsCorrect_expected
new file mode 100644
index 000000000..49263a9ec
--- /dev/null
+++ b/src/test/resources/branchTreeTests/allPathsCorrect_expected
@@ -0,0 +1 @@
+Verification successful.
\ No newline at end of file
diff --git a/src/test/resources/branchTreeTests/firstPathFails.vpr b/src/test/resources/branchTreeTests/firstPathFails.vpr
new file mode 100644
index 000000000..e896a90ff
--- /dev/null
+++ b/src/test/resources/branchTreeTests/firstPathFails.vpr
@@ -0,0 +1,19 @@
+define P(z) z == true
+
+method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool)
+requires a ==> c
+ensures P(z) {
+    if (a) {
+       if (bcde) {
+            z := !(bcde && a) // failure
+       } else {
+            z := (bcde && !a)
+       }
+    } else {
+        if (c) {
+            z := !(c && a)
+        } else {
+            z := !(!c && !a)
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/test/resources/branchTreeTests/firstPathFails_expected b/src/test/resources/branchTreeTests/firstPathFails_expected
new file mode 100644
index 000000000..3261bfed6
--- /dev/null
+++ b/src/test/resources/branchTreeTests/firstPathFails_expected
@@ -0,0 +1,10 @@
+Branch fails.
+┌─┴─┐
+│ a │
+└─┬─┘
+F┌┴────┐T
+ ? ┌───┴───┐
+   │ bcde  │
+   └───┬───┘
+     F┌┴──┐T
+      ? Error
\ No newline at end of file
diff --git a/src/test/resources/branchTreeTests/lastPathFails.vpr b/src/test/resources/branchTreeTests/lastPathFails.vpr
new file mode 100644
index 000000000..a1618e5d3
--- /dev/null
+++ b/src/test/resources/branchTreeTests/lastPathFails.vpr
@@ -0,0 +1,19 @@
+define P(z) z == true
+
+method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool)
+requires a ==> c
+ensures P(z) {
+    if (a) {
+       if (bcde) {
+            z := (bcde && a)
+       } else {
+            z := !(bcde && !a)
+       }
+    } else {
+        if (c) {
+            z := !(c && a)
+        } else {
+            z := !(!c && !a) // failure
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/test/resources/branchTreeTests/lastPathFails_expected b/src/test/resources/branchTreeTests/lastPathFails_expected
new file mode 100644
index 000000000..2a2b9156f
--- /dev/null
+++ b/src/test/resources/branchTreeTests/lastPathFails_expected
@@ -0,0 +1,10 @@
+ Branch fails. 
+      ┌─┴─┐       
+      │ a │       
+      └─┬─┘       
+    F┌──┴────┐T   
+   ┌─┴─┐ ┌───┴───┐
+   │ c │ │ bcde  │
+   └─┬─┘ └───┬───┘
+ F┌──┴┐T   F┌┴┐T  
+Error ✔     ✔ ✔ 
\ No newline at end of file
diff --git a/src/test/resources/branchTreeTests/noBranches.vpr b/src/test/resources/branchTreeTests/noBranches.vpr
new file mode 100644
index 000000000..7ae9e52e8
--- /dev/null
+++ b/src/test/resources/branchTreeTests/noBranches.vpr
@@ -0,0 +1,6 @@
+define P(z) z == true
+
+method foo(b: Bool) returns (z: Bool)
+ensures P(z) {
+   z := true
+}
\ No newline at end of file
diff --git a/src/test/resources/branchTreeTests/noBranches_expected b/src/test/resources/branchTreeTests/noBranches_expected
new file mode 100644
index 000000000..49263a9ec
--- /dev/null
+++ b/src/test/resources/branchTreeTests/noBranches_expected
@@ -0,0 +1 @@
+Verification successful.
\ No newline at end of file
diff --git a/src/test/resources/branchTreeTests/onlyIf.vpr b/src/test/resources/branchTreeTests/onlyIf.vpr
new file mode 100644
index 000000000..6f8c13eb9
--- /dev/null
+++ b/src/test/resources/branchTreeTests/onlyIf.vpr
@@ -0,0 +1,14 @@
+define P(z) z == true
+
+method foo(a: Int, b: Int, d: Bool) returns (z: Bool)
+ensures P(z) {
+    var a_ : Int := a
+    var b_ : Int := b
+    if (d) {
+        a_ := 3
+        b_ := 3
+    }
+    var c: Int
+    c := a_ / b_
+    z := c > 1
+}
\ No newline at end of file
diff --git a/src/test/resources/branchTreeTests/onlyIf_expected b/src/test/resources/branchTreeTests/onlyIf_expected
new file mode 100644
index 000000000..195808129
--- /dev/null
+++ b/src/test/resources/branchTreeTests/onlyIf_expected
@@ -0,0 +1,6 @@
+Branch fails. 
+┌─┴─┐
+│ d │
+└─┬─┘
+F┌┴──┐T
+? Error
\ No newline at end of file
diff --git a/src/test/resources/branchTreeTests/while.vpr b/src/test/resources/branchTreeTests/while.vpr
new file mode 100644
index 000000000..307ed3214
--- /dev/null
+++ b/src/test/resources/branchTreeTests/while.vpr
@@ -0,0 +1,13 @@
+define P(z) z == true
+
+method foo(a: Bool, bcde: Bool, c: Bool) returns (z: Bool)
+requires a ==> c
+ensures P(z) {
+    while (a) {
+       if (bcde) {
+            z := !(bcde && a)
+        } else {
+            z := !(bcde && !a)
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/test/resources/branchTreeTests/while_expected b/src/test/resources/branchTreeTests/while_expected
new file mode 100644
index 000000000..f6ae05ac2
--- /dev/null
+++ b/src/test/resources/branchTreeTests/while_expected
@@ -0,0 +1,6 @@
+Branch fails. 
+  ┌─┴─┐
+  │ a │
+  └─┬─┘
+F┌──┴┐T
+Error ?
\ No newline at end of file
diff --git a/src/test/scala/BranchTreeTests.scala b/src/test/scala/BranchTreeTests.scala
new file mode 100644
index 000000000..5af7a5879
--- /dev/null
+++ b/src/test/scala/BranchTreeTests.scala
@@ -0,0 +1,49 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distrcibuted with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2019 ETH Zurich.
+
+import org.scalatest.funsuite.AnyFunSuite
+import viper.silver.ast.utility.DiskLoader
+
+import java.nio.file.{Files, Paths}
+
+class BranchTreeTests extends AnyFunSuite {
+  val frontend = tests.instantiateFrontend()
+
+  test("FirstPathFails") {
+    executeTest("firstPathFails")
+  }
+
+  test("LastPathFails") {
+    executeTest("lastPathFails")
+  }
+
+  test("While") {
+    executeTest("while")
+  }
+
+  test("OnlyIf") {
+    executeTest("onlyIf")
+  }
+
+  test("AllPathsCorrect") {
+    executeTest("allPathsCorrect")
+  }
+
+  test("NoBranches") {
+    executeTest("noBranches")
+  }
+
+  def executeTest(fileName: String)
+  : Unit = {
+    val expectedFile = getClass.getClassLoader.getResource(s"branchTreeTests/"+fileName+"_expected")
+    val expected = DiskLoader.loadContent(Paths.get(expectedFile.toURI)).get
+    val program = tests.loadProgram("branchTreeTests/",fileName, frontend)
+    val actual = frontend.verifier.verify(program)
+    assert(actual.toString.contains(expected))
+  }
+}
+
+