Report branchconditions / FailureContext

src/main/scala/viper/silver/verifier/VerificationError.scala

@@ -154,17 +154,16 @@ trait ErrorMessage {
 trait VerificationError extends AbstractError with ErrorMessage {
   def reason: ErrorReason
   def readableMessage(withId: Boolean = false, withPosition: Boolean = false): String
-  override def readableMessage : String = {
-    val rm : String = readableMessage(false, true)
-    if (counterexample.isDefined){
-      rm + "\n" + counterexample.get.toString
-    }else{
-      rm
-    }
-  }
+  override def readableMessage: String = readableMessage(false, true) + failureContexts.map(e => e.toString).mkString("\n")
   def loggableMessage: String = s"$fullId-$pos" + (if (cached) "-cached" else "")
   def fullId = s"$id:${reason.id}"
-  var counterexample : Option[Counterexample] = None
+  var failureContexts: Seq[FailureContext] = Seq() //TODO: make immutable
+
+}
+
+trait FailureContext {
+  def counterExample: Option[Counterexample]
+  def toString: String
 }
 
 /// used when an error/reason has no sensible node to use
@@ -230,8 +229,7 @@ abstract class AbstractVerificationError extends VerificationError {
     val reasonT = errorT.reason.offendingNode.transformReason(errorT.reason)
 
     val res = errorT.withReason(reasonT)
-    res.counterexample = counterexample
-    res.branchConditions = branchConditions
+    res.failureContexts = failureContexts
     res
   }
 

src/test/resources/all/issues/silicon/0083.vpr

@@ -1,37 +1,39 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
-field f: Int
-
-method test1(xs: Seq[Int])
-  //:: ExpectedOutput(not.wellformed:seq.index.negative)
-  requires xs[-1] != 0
-
-method test10(xs: Seq[Int])
-  //:: ExpectedOutput(not.wellformed:seq.index.length)
-  ensures xs[1] != 0
-
-method test2(xs: Seq[Int], n: Int)
-  requires 5 < n
-  //:: ExpectedOutput(not.wellformed:seq.index.length)
-  requires forall i: Int :: i in [0..n) ==> xs[i] != 0
-{
-  //:: UnexpectedOutput(assert.failed:seq.index.length, /Carbon/issue/388/)
-  assert xs[3] != 0
-}
-
-method test3(xs: Seq[Ref], n: Int)
-  requires 5 < n && n < |xs|
-  requires xs[0] != null
-  requires forall i: Int :: i in [0..n) ==> acc(xs[i].f)
-{
-  var y: Int := xs[3].f
-}
-
-function fun(i: Int): Bool
-
-method test20(xs: Seq[Int], i: Int) {
-  //:: ExpectedOutput(assignment.failed:seq.index.negative)
-  //:: ExpectedOutput(assignment.failed:seq.index.length)
-  var b: Bool := fun(xs[i])
-}
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+field f: Int
+
+method test1(xs: Seq[Int])
+  //:: ExpectedOutput(not.wellformed:seq.index.negative)
+  requires xs[-1] != 0
+
+method test10(xs: Seq[Int])
+  //:: ExpectedOutput(not.wellformed:seq.index.length)
+  ensures xs[1] != 0
+
+method test2(xs: Seq[Int], n: Int)
+  requires 5 < n
+  //:: ExpectedOutput(not.wellformed:seq.index.length)
+  requires forall i: Int :: i in [0..n) ==> xs[i] != 0
+{
+  //:: ExpectedOutput(assert.failed:seq.index.length)
+  //:: MissingOutput(assert.failed:seq.index.length, /silicon/issue/34/)
+  assert xs[3] != 0
+}
+
+method test3(xs: Seq[Ref], n: Int)
+  requires 5 < n && n < |xs|
+  requires xs[0] != null
+  requires forall i: Int :: i in [0..n) ==> acc(xs[i].f)
+{
+  var y: Int := xs[3].f
+}
+
+function fun(i: Int): Bool
+
+method test20(xs: Seq[Int], i: Int) {
+  //:: ExpectedOutput(assignment.failed:seq.index.negative)
+  //:: ExpectedOutput(assignment.failed:seq.index.length)
+  //:: MissingOutput(assignment.failed:seq.index.length, /silicon/issue/34/)
+  var b: Bool := fun(xs[i])
+}

src/test/resources/quantifiedpermissions/sequences/bsearch.vpr

@@ -12,6 +12,7 @@ method bfind_orig(S: Seq[Ref], x: Int, p: Perm) returns (index: Int)
   ensures forall i: Int :: {S[i].f} i in [0..|S|) ==> acc(S[i].f, p)
   ensures index in [-1..|S|)
   //:: ExpectedOutput(postcondition.violated:assertion.false)
+  //:: MissingOutput(postcondition.violated:assertion.false, /silicon/issue/34/)
   ensures index in [0..|S|) ==> S[index].f == x
   //:: ExpectedOutput(postcondition.violated:assertion.false)
   ensures index == -1 ==> (forall i: Int :: {S[i].f} i in [0..|S|) ==> S[i].f != x)

src/test/resources/wands/examples/list_insert_tmp.vpr

@@ -129,7 +129,6 @@ method insert(xs: Ref, x: Int) returns (i: Int)
     acc(List(xs)) && elems(xs) == old(elems(xs))[0..i] ++ (Seq(x) ++ crtElems)
 
   //:: UnexpectedOutput(assert.failed:assertion.false, /carbon/issue/290/)
-  //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/550/)
   assert acc(List(crt))&& elems(crt) == Seq(x) ++ crtElems
 
   apply

src/test/resources/wands/new_syntax/QPWands.vpr

@@ -1,112 +1,111 @@
 // Any copyright is dedicated to the Public Domain.
 // http://creativecommons.org/publicdomain/zero/1.0/
 
-//:: IgnoreFile(/carbon/issue/216/)
-field f: Int
-
-define injectiveSeq(xs) forall i: Int, j: Int :: 0 <= i && 0 <= j && i < |xs| && j < |xs| && i != j ==> xs[i] != xs[j]
-
-method test0(xs: Seq[Ref], y: Ref)
-requires forall x: Ref :: x in xs ==> acc(x.f)
-requires injectiveSeq(xs)
-requires |xs| >= 1
-requires acc(y.f) {
-    xs[0].f := 0
-    y.f := 1
-    label setupComplete
-    var toGo: Seq[Ref] := xs
-    var completed: Seq[Ref] := Seq()
-    while (|toGo| != 0) 
-    invariant forall x: Ref :: x in completed ==> acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f)
-    invariant forall i: Int, j: Int :: 0 <= i && 0 <= j && i < |toGo| && j < |toGo| && i != j ==> toGo[i] != toGo[j]
-    invariant forall x: Ref :: x in toGo ==> acc(x.f)
-    invariant xs == completed ++ toGo
-    invariant forall x: Ref :: x in toGo ==> x.f == old[setupComplete](x.f)
-    invariant acc(y.f) && y.f == 1
-    //:: UnexpectedOutput(invariant.not.preserved:assertion.false, /silicon/issue/311/)
-    invariant forall x: Ref :: x in completed ==>
-      applying (acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f)) in
-      x.f == old[setupComplete](x.f) {
-        var localX: Ref := toGo[0]
-        package acc(y.f) --* acc(localX.f) && acc(y.f) && y.f == old[lhs](y.f)
-        completed := completed ++ Seq(localX)
-        toGo := toGo[1..]
-    }
-    assert forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f)
-    var some: Ref := xs[0]
-    apply acc(y.f) --* acc(some.f) && acc(y.f) && y.f == old[lhs](y.f)
-    //:: UnexpectedOutput(assert.failed:assertion.false, /silicon/issue/551/)
-    assert some.f == 0 //This shouldn't throw an error
-    assert y.f == 1
-}
-
-method test1(x: Ref)
-requires forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f) {
-    exhale forall i: Int :: true ==> acc(x.f) && x.f == i-1 --* acc(x.f)
-
-    //:: ExpectedOutput(assert.failed:wand.not.found)
-    assert forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f)
-}
-
-method test2(xs: Seq[Ref], y: Ref)
-requires forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f) {
-
-    //:: ExpectedOutput(assert.failed:wand.not.found)
-    assert forall x: Ref :: x in xs ==> acc(y.f) --* acc(y.f) && acc(x.f)
-}
-
-method test3(xs: Seq[Ref], y: Ref)
-requires forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f)
-requires injectiveSeq(xs)
-requires |xs| > 0
-requires acc(y.f) {
-    var some: Ref := xs[0]
-    package true --* acc(some.f) && acc(y.f) {
-        apply acc(y.f) --* acc(some.f) && acc(y.f)
-    }
-    assert forall x: Ref :: x in xs[1..] ==> acc(y.f) --* acc(x.f) && acc(y.f)
-
-    //:: ExpectedOutput(assert.failed:wand.not.found)
-    assert forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f)
-}
-
-method test4(x: Ref)
-requires forall i: Int, j: Int :: true ==> acc(x.f) && x.f == i + j --* acc(x.f) {
-    exhale acc(x.f) && x.f == 5 --* acc(x.f)
-    assert forall i: Int :: i != 5 ==> acc(x.f) && x.f == i --* acc(x.f)
-
-    //:: ExpectedOutput(assert.failed:wand.not.found)
-    assert forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f)
-}
-
-method test5(xs: Seq[Ref], y: Ref)
-requires forall x: Ref :: x in xs ==> acc(x.f)
-requires injectiveSeq(xs)
-requires |xs| >= 1
-requires acc(y.f) {
-    xs[0].f := 0
-    y.f := 1
-    var some: Ref := xs[0]
-    package acc(y.f) --* acc(some.f) && acc(y.f)
-    var completed: Seq[Ref] := Seq(some)
-    assert forall x: Ref :: x in completed ==> acc(y.f) --* acc(x.f) && acc(y.f)
-    assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in some.f == 0
-    assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in y.f == 1
-    assert forall x: Ref :: x in xs[1..] ==> acc(x.f)
-
-    //:: ExpectedOutput(assert.failed:insufficient.permission)
-    assert forall x: Ref :: x in xs ==> acc(x.f)
-}
-
-method test6(xs: Seq[Ref])
-requires forall x: Ref :: x in xs ==> true --* acc(x.f)
-requires |xs| > 0 {
-    assume applying (true --* acc(xs[0].f)) in xs[0].f == 0
-    package true --* (forall x: Ref :: x in xs ==> true --* acc(x.f))
-    apply true --* (forall x: Ref :: x in xs ==> true --* acc(x.f))
-    apply true --* acc(xs[0].f)
-    assert xs[0].f == 0
-
-    //:: ExpectedOutput(assert.failed:assertion.false)
-    assert false
-}
+//:: IgnoreFile(/carbon/issue/216/)
+field f: Int
+
+define injectiveSeq(xs) forall i: Int, j: Int :: 0 <= i && 0 <= j && i < |xs| && j < |xs| && i != j ==> xs[i] != xs[j]
+
+method test0(xs: Seq[Ref], y: Ref)
+requires forall x: Ref :: x in xs ==> acc(x.f)
+requires injectiveSeq(xs)
+requires |xs| >= 1
+requires acc(y.f) {
+    xs[0].f := 0
+    y.f := 1
+    label setupComplete
+    var toGo: Seq[Ref] := xs
+    var completed: Seq[Ref] := Seq()
+    while (|toGo| != 0) 
+    invariant forall x: Ref :: x in completed ==> acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f)
+    invariant forall i: Int, j: Int :: 0 <= i && 0 <= j && i < |toGo| && j < |toGo| && i != j ==> toGo[i] != toGo[j]
+    invariant forall x: Ref :: x in toGo ==> acc(x.f)
+    invariant xs == completed ++ toGo
+    invariant forall x: Ref :: x in toGo ==> x.f == old[setupComplete](x.f)
+    invariant acc(y.f) && y.f == 1
+    //:: UnexpectedOutput(invariant.not.preserved:assertion.false, /silicon/issue/311/)
+    invariant forall x: Ref :: x in completed ==>
+      applying (acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f)) in
+      x.f == old[setupComplete](x.f) {
+        var localX: Ref := toGo[0]
+        package acc(y.f) --* acc(localX.f) && acc(y.f) && y.f == old[lhs](y.f)
+        completed := completed ++ Seq(localX)
+        toGo := toGo[1..]
+    }
+    assert forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f) && y.f == old[lhs](y.f)
+    var some: Ref := xs[0]
+    apply acc(y.f) --* acc(some.f) && acc(y.f) && y.f == old[lhs](y.f)
+    assert some.f == 0
+    assert y.f == 1
+}
+
+method test1(x: Ref)
+requires forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f) {
+    exhale forall i: Int :: true ==> acc(x.f) && x.f == i-1 --* acc(x.f)
+
+    //:: ExpectedOutput(assert.failed:wand.not.found)
+    assert forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f)
+}
+
+method test2(xs: Seq[Ref], y: Ref)
+requires forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f) {
+
+    //:: ExpectedOutput(assert.failed:wand.not.found)
+    assert forall x: Ref :: x in xs ==> acc(y.f) --* acc(y.f) && acc(x.f)
+}
+
+method test3(xs: Seq[Ref], y: Ref)
+requires forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f)
+requires injectiveSeq(xs)
+requires |xs| > 0
+requires acc(y.f) {
+    var some: Ref := xs[0]
+    package true --* acc(some.f) && acc(y.f) {
+        apply acc(y.f) --* acc(some.f) && acc(y.f)
+    }
+    assert forall x: Ref :: x in xs[1..] ==> acc(y.f) --* acc(x.f) && acc(y.f)
+
+    //:: ExpectedOutput(assert.failed:wand.not.found)
+    assert forall x: Ref :: x in xs ==> acc(y.f) --* acc(x.f) && acc(y.f)
+}
+
+method test4(x: Ref)
+requires forall i: Int, j: Int :: true ==> acc(x.f) && x.f == i + j --* acc(x.f) {
+    exhale acc(x.f) && x.f == 5 --* acc(x.f)
+    assert forall i: Int :: i != 5 ==> acc(x.f) && x.f == i --* acc(x.f)
+
+    //:: ExpectedOutput(assert.failed:wand.not.found)
+    assert forall i: Int :: true ==> acc(x.f) && x.f == i --* acc(x.f)
+}
+
+method test5(xs: Seq[Ref], y: Ref)
+requires forall x: Ref :: x in xs ==> acc(x.f)
+requires injectiveSeq(xs)
+requires |xs| >= 1
+requires acc(y.f) {
+    xs[0].f := 0
+    y.f := 1
+    var some: Ref := xs[0]
+    package acc(y.f) --* acc(some.f) && acc(y.f)
+    var completed: Seq[Ref] := Seq(some)
+    assert forall x: Ref :: x in completed ==> acc(y.f) --* acc(x.f) && acc(y.f)
+    assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in some.f == 0
+    assert applying (acc(y.f) --* acc(some.f) && acc(y.f)) in y.f == 1
+    assert forall x: Ref :: x in xs[1..] ==> acc(x.f)
+
+    //:: ExpectedOutput(assert.failed:insufficient.permission)
+    assert forall x: Ref :: x in xs ==> acc(x.f)
+}
+
+method test6(xs: Seq[Ref])
+requires forall x: Ref :: x in xs ==> true --* acc(x.f)
+requires |xs| > 0 {
+    assume applying (true --* acc(xs[0].f)) in xs[0].f == 0
+    package true --* (forall x: Ref :: x in xs ==> true --* acc(x.f))
+    apply true --* (forall x: Ref :: x in xs ==> true --* acc(x.f))
+    apply true --* acc(xs[0].f)
+    assert xs[0].f == 0
+
+    //:: ExpectedOutput(assert.failed:assertion.false)
+    assert false
+}