Merge pull request #822 from viperproject/meilers_mce_definite_alias_fix

Only considering definite aliases with non-zero permission

Author: marcoeilers

src/main/scala/rules/MoreCompleteExhaleSupporter.scala

@@ -87,7 +87,8 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
                 case None =>
                   // We have not yet checked for a definite alias
                   val id = ChunkIdentifier(resource, s.program)
-                  chunkSupporter.findChunk[NonQuantifiedChunk](relevantChunks, id, args, v).map(_.snap)
+                  val potentialAlias = chunkSupporter.findChunk[NonQuantifiedChunk](relevantChunks, id, args, v)
+                  potentialAlias.filter(c => v.decider.check(IsPositive(c.perm), Verifier.config.checkTimeout())).map(_.snap)
                 case Some(v) =>
                   // We have checked for a definite alias and may or may not have found one.
                   v
@@ -253,7 +254,9 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules {
         val newChunks = ListBuffer[NonQuantifiedChunk]()
         var moreNeeded = true
 
-        val definiteAlias = chunkSupporter.findChunk[NonQuantifiedChunk](relevantChunks, id, args, v)
+        val definiteAlias = chunkSupporter.findChunk[NonQuantifiedChunk](relevantChunks, id, args, v).filter(c =>
+          v.decider.check(IsPositive(c.perm), Verifier.config.checkTimeout())
+        )
 
         val sortFunction: (NonQuantifiedChunk, NonQuantifiedChunk) => Boolean = (ch1, ch2) => {
           // The definitive alias and syntactic aliases should get priority, since it is always