Fixed crash in type checker (#817) (#873)

Author: marcoeilers

src/main/scala/viper/silver/parser/Resolver.scala

@@ -833,7 +833,7 @@ case class TypeChecker(names: NameAnalyser) {
         permBan = Some("forperm quantifier bodies")
         check(pq.body, Bool)
         permBan = oldPermBan
-        checkInternal(pq.accessRes)
+        checkTopTyped(pq.accessRes, None)
         pq.triggers foreach (_.exp.inner.toSeq foreach (tpe => checkTopTyped(tpe, None)))
         pq._typeSubstitutions = pq.body.typeSubstitutions.toList.distinct
         pq.typ = Bool

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

@@ -0,0 +1,18 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+domain Pointer[]  {
+}
+
+domain F  {
+  function foo(bar: F): Ref
+}
+
+field int: Int
+field f: F
+
+function ptrDeref(p: Pointer[]): Ref
+
+method baz()
+  //:: ExpectedOutput(typechecker.error)
+  ensures [true, (forperm this: Pointer[] [foo(ptrDeref(this).f).int] :: false)]