Merge pull request #744 from viperproject/meilers_unfold_none

New error reason for unfolding or folding with non-positive permission amount.

Author: marcoeilers

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

@@ -650,6 +650,14 @@ object reasons {
     def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = NegativePermission(offendingNode.asInstanceOf[Exp])
   }
 
+  case class NonPositivePermission(offendingNode: Exp) extends AbstractErrorReason {
+    val id = "permission.not.positive"
+
+    def readableMessage = s"Fraction $offendingNode might not be positive."
+
+    def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = NonPositivePermission(offendingNode.asInstanceOf[Exp])
+  }
+
   case class InsufficientPermission(offendingNode: LocationAccess) extends AbstractErrorReason {
     val id = "insufficient.permission"
     def readableMessage = s"There might be insufficient permission to access $offendingNode"

src/test/resources/all/issues/carbon/0125.vpr

@@ -1,13 +1,13 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 
 predicate P(x: Ref) { acc(x.f) }
 
 method test1(x: Ref) {
   inhale P(x)
-  //:: ExpectedOutput(unfold.failed:negative.permission)
+  //:: ExpectedOutput(unfold.failed:permission.not.positive)
   unfold acc(P(x), -(1/2))
 }
 
@@ -16,7 +16,7 @@ method test2(x: Ref) {
   assume p == -(1/2)
 
   inhale P(x)
-  //:: ExpectedOutput(unfold.failed:negative.permission)
+  //:: ExpectedOutput(unfold.failed:permission.not.positive)
   unfold acc(P(x), p)
 }
 

src/test/resources/all/issues/silver/0072.vpr

@@ -1,6 +1,6 @@
-// Any copyright is dedicated to the Public Domain.
-// http://creativecommons.org/publicdomain/zero/1.0/
-
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
 field f: Int
 
 predicate token(x: Ref) {
@@ -16,14 +16,14 @@ method t_plus(x: Ref)
 method t_minus_1(x: Ref)
     requires acc(x.f)
 {
-    //:: ExpectedOutput(fold.failed:negative.permission)
+    //:: ExpectedOutput(fold.failed:permission.not.positive)
     fold acc(token(x), (-1/1))
 }
 
 method t_minus_2(x: Ref)
     requires acc(x.f)
 {
-    //:: ExpectedOutput(fold.failed:negative.permission)
+    //:: ExpectedOutput(fold.failed:permission.not.positive)
     fold acc(token(x), -(1/1))
 }
 

src/test/resources/all/issues/silver/0444.vpr

@@ -0,0 +1,52 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+
+predicate falze()
+{
+    false
+}
+
+predicate tru()
+{
+    true
+}
+
+method test_unfold(){
+    //:: ExpectedOutput(unfold.failed:permission.not.positive)
+    unfold acc(falze(), none)
+    assert false
+}
+
+method test_unfold_unknown(p: Perm){
+    assume p >= none
+    //:: ExpectedOutput(unfold.failed:permission.not.positive)
+    //:: ExpectedOutput(unfold.failed:insufficient.permission)
+    //:: MissingOutput(unfold.failed:insufficient.permission, /Silicon/issue/34/)
+    unfold acc(falze(), p)
+    assert false
+}
+
+method test_unfolding(){
+    //:: ExpectedOutput(assert.failed:permission.not.positive)
+    assert unfolding acc(falze(), none) in false
+}
+
+method test_unfolding_unknown(p: Perm){
+    assume p >= none
+    //:: ExpectedOutput(assert.failed:permission.not.positive)
+    //:: ExpectedOutput(assert.failed:insufficient.permission)
+    //:: MissingOutput(assert.failed:insufficient.permission, /Silicon/issue/34/)
+    assert unfolding acc(falze(), p) in false
+}
+
+method test_fold(){
+    //:: ExpectedOutput(fold.failed:permission.not.positive)
+    fold acc(tru(), none)
+}
+
+method test_fold_unknown(p: Perm){
+    assume p >= none
+    //:: ExpectedOutput(fold.failed:permission.not.positive)
+    fold acc(tru(), p)
+}

src/test/resources/all/issues/silver/0522.vpr

@@ -27,7 +27,7 @@ method test3b(x: Ref, p: Perm) {
 
 method test4(x: Ref, p: Perm) {
   inhale P(x)
-  //:: ExpectedOutput(unfold.failed:negative.permission)
+  //:: ExpectedOutput(unfold.failed:permission.not.positive)
   //:: ExpectedOutput(unfold.failed:insufficient.permission)
   //:: MissingOutput(unfold.failed:insufficient.permission, /Silicon/issue/34/)
   unfold acc(P(x), p)