Merge pull request #684 from viperproject/meilers_issue_205

Fixing issue #205

Author: marcoeilers

silver

@@ -116,7 +116,16 @@ object chunkSupporter extends ChunkSupportRules {
         } else {
           consumeGreedy(s1, s1.h, id, args, perms, v1) match {
             case (Complete(), s2, h2, optCh2) =>
-              QS(s2.copy(h = s.h), h2, optCh2.map(_.snap), v1)
+              val snap = optCh2 match {
+                case None => None
+                case Some(ch) =>
+                  if (v1.decider.check(Greater(perms, NoPerm()), Verifier.config.checkTimeout())) {
+                    Some(ch.snap)
+                  } else {
+                    Some(Ite(Greater(perms, NoPerm()), ch.snap.convert(sorts.Snap), Unit))
+                  }
+              }
+              QS(s2.copy(h = s.h), h2, snap, v1)
             case _ if v1.decider.checkSmoke() =>
               Success() // TODO: Mark branch as dead?
             case _ =>

src/main/scala/rules/ChunkSupporter.scala

@@ -947,6 +947,7 @@ class Less(val p0: Term, val p1: Term) extends ComparisonTerm
 object Less extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) {
   def apply(e0: Term, e1: Term) = (e0, e1) match {
     case (IntLiteral(n0), IntLiteral(n1)) => if (n0 < n1) True() else False()
+    case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal < pl1.literal) True() else False()
     case (t0, t1) if t0 == t1 => False()
     case _ => new Less(e0, e1)
   }
@@ -963,6 +964,7 @@ class AtMost(val p0: Term, val p1: Term) extends ComparisonTerm
 object AtMost extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) {
   def apply(e0: Term, e1: Term) = (e0, e1) match {
     case (IntLiteral(n0), IntLiteral(n1)) => if (n0 <= n1) True() else False()
+    case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal <= pl1.literal) True() else False()
     case (t0, t1) if t0 == t1 => True()
     case _ => new AtMost(e0, e1)
   }
@@ -979,6 +981,7 @@ class Greater(val p0: Term, val p1: Term) extends ComparisonTerm
 object Greater extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) {
   def apply(e0: Term, e1: Term) = (e0, e1) match {
     case (IntLiteral(n0), IntLiteral(n1)) => if (n0 > n1) True() else False()
+    case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal > pl1.literal) True() else False()
     case (t0, t1) if t0 == t1 => False()
     case _ => new Greater(e0, e1)
   }
@@ -995,6 +998,7 @@ class AtLeast(val p0: Term, val p1: Term) extends ComparisonTerm
 object AtLeast extends /* OptimisingBinaryArithmeticOperation with */ ((Term, Term) => Term) {
   def apply(e0: Term, e1: Term) = (e0, e1) match {
     case (IntLiteral(n0), IntLiteral(n1)) => if (n0 >= n1) True() else False()
+    case (pl0: PermLiteral, pl1: PermLiteral) => if (pl0.literal >= pl1.literal) True() else False()
     case (t0, t1) if t0 == t1 => True()
     case _ => new AtLeast(e0, e1)
   }