Refactor well-definedness of field acesses and permission division

src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala

@@ -391,9 +391,10 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
         def translate(e: sil.Exp): Seqn = {
           val checks = components map (_.partialCheckDefinedness(e, error, makeChecks = makeChecks))
           val stmt = checks map (_._1())
+
           // AS: note that some implementations of the definedness checks rely on the order of these calls (i.e. parent nodes are checked before children, and children *are* always checked after parents.
-          val stmt2 = for (sub <- e.subnodes if sub.isInstanceOf[sil.Exp]) yield {
-            checkDefinednessImpl(sub.asInstanceOf[sil.Exp], error, makeChecks = makeChecks)
+          val stmt2 = for (sub <- subexpressionsForDefinedness(e)) yield {
+            checkDefinednessImpl(sub, error, makeChecks = makeChecks)
           }
           val stmt3 = checks map (_._2())
 
@@ -457,6 +458,17 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
     }
   }
 
+  /***
+    * Returns subexpressions that are relevant for definedness checks
+    */
+  private def subexpressionsForDefinedness(e: sil.Exp) : Seq[sil.Exp] = {
+    e match {
+      case sil.AccessPredicate(res : sil.LocationAccess, perm) => res.subExps ++ Seq(perm)
+      case sil.CurrentPerm(res: sil.LocationAccess) => res.subExps
+      case _ => e.subExps
+    }
+  }
+
   /**
     * checks self-framedness of both sides of wand
     * GP: maybe should "MagicWandNotWellFormed" error

src/main/scala/viper/carbon/modules/impls/QuantifiedPermModule.scala

@@ -259,7 +259,6 @@ class QuantifiedPermModule(val verifier: Verifier)
 
   override def reset = {
     mask = originalMask
-    allowLocationAccessWithoutPerm = false
     qpId = 0
     inverseFuncs = new ListBuffer[Func]();
     rangeFuncs = new ListBuffer[Func]();
@@ -1527,28 +1526,14 @@ class QuantifiedPermModule(val verifier: Verifier)
     permLe(b, a, forField)
   }
 
-  // AS: this is a trick to avoid well-definedness checks for the outermost heap dereference in an AccessPredicate node (since it describes the location to which permission is provided).
-  // The trick is somewhat fragile, in that it relies on the ordering of the calls to this method (but generally works out because of the recursive traversal of the assertion).
-  private var allowLocationAccessWithoutPerm = false
-  override def simplePartialCheckDefinednessBefore(e: sil.Exp, error: PartialVerificationError, makeChecks: Boolean): Stmt = {
+  override def simplePartialCheckDefinednessAfter(e: sil.Exp, error: PartialVerificationError, makeChecks: Boolean): Stmt = {
 
     val stmt: Stmt = if(makeChecks) (
       e match {
-        case sil.CurrentPerm(loc) =>
-          allowLocationAccessWithoutPerm = true
-          Nil
-        case sil.AccessPredicate(loc, perm) =>
-          allowLocationAccessWithoutPerm = true
-          Nil
         case fa@sil.LocationAccess(_) =>
-          if (allowLocationAccessWithoutPerm) {
-            allowLocationAccessWithoutPerm = false
-            Nil
-          } else {
-              Assert(hasDirectPerm(fa), error.dueTo(reasons.InsufficientPermission(fa)))
-          }
+          Assert(hasDirectPerm(fa), error.dueTo(reasons.InsufficientPermission(fa)))
         case sil.PermDiv(a, b) =>
-            Assert(translateExp(b) !== IntLit(0), error.dueTo(reasons.DivisionByZero(b)))
+          Assert(translateExp(b) !== IntLit(0), error.dueTo(reasons.DivisionByZero(b)))
         case sil.PermPermDiv(a, b) =>
           Assert(translatePerm(b) !== RealLit(0.0), error.dueTo(reasons.DivisionByZero(b)))
         case _ => Nil