Add tests

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
+    }
+}

src/test/resources/branchTreeTests/allPathsCorrect_expected

@@ -0,0 +1 @@
+Verification successful.

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)
+        }
+    }
+}

src/test/resources/branchTreeTests/firstPathFails_expected

@@ -0,0 +1,10 @@
+Branch fails.
+┌─┴─┐
+│ a │
+└─┬─┘
+F┌┴────┐T
+ ? ┌───┴───┐
+   │ bcde  │
+   └───┬───┘
+     F┌┴──┐T
+      ? Error

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
+        }
+    }
+}

src/test/resources/branchTreeTests/lastPathFails_expected

@@ -0,0 +1,10 @@
+ Branch fails. 
+      ┌─┴─┐       
+      │ a │       
+      └─┬─┘       
+    F┌──┴────┐T   
+   ┌─┴─┐ ┌───┴───┐
+   │ c │ │ bcde  │
+   └─┬─┘ └───┬───┘
+ F┌──┴┐T   F┌┴┐T  
+Error ✔     ✔ ✔ 

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
+}

src/test/resources/branchTreeTests/noBranches_expected

@@ -0,0 +1 @@
+Verification successful.

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
+}

src/test/resources/branchTreeTests/onlyIf_expected

@@ -0,0 +1,6 @@
+Branch fails. 
+┌─┴─┐
+│ d │
+└─┬─┘
+F┌┴──┐T
+? Error

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)
+        }
+    }
+}

src/test/resources/branchTreeTests/while_expected

@@ -0,0 +1,6 @@
+Branch fails. 
+  ┌─┴─┐
+  │ a │
+  └─┬─┘
+F┌──┴┐T
+Error ?

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))
+  }
+}
+
+