Merge pull request #698 from viperproject/issue-697

Fixes #697

src/main/scala/viper/gobra/frontend/Desugar.scala

@@ -4532,10 +4532,10 @@ object Desugar extends LazyLogging {
 
         case n: PInvoke =>
           // a predicate invocation corresponds to a predicate access with full permissions
-          // register the full permission AST node in the position manager such that its meta information
+          // register the full permission AST node in `info`'s position manager such that its meta information
           // is retrievable in predicateCallD
           val perm = PFullPerm()
-          pom.positions.dupPos(n, perm)
+          info.tree.root.positions.positions.dupPos(n, perm)
           predicateCallD(ctx, info)(n, perm)
 
         case PForall(vars, triggers, body) =>

src/test/resources/regressions/issues/000697.gobra

@@ -0,0 +1,35 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue000697
+
+// ##(-I ./000697/)
+import pkg "pkg"
+
+type Impl struct{
+    x *int
+}
+
+pred (impl Impl) inv() {
+    acc(impl.x)
+}
+
+func main() {
+    x@ := 0
+
+    cl :=   preserves acc(&x)
+            func closureImpl() int {
+                x += 42
+                return x
+            }
+
+    proof cl implements pkg.ClosureSpec{Impl{&x}} {
+        unfold Impl{&x}.inv()
+        res = cl() as closureImpl
+        fold Impl{&x}.inv()
+    }
+
+    impl := Impl{&x}
+    fold impl.inv()
+    pkg.Invoke(cl, impl)
+}

src/test/resources/regressions/issues/000697/pkg/pkg.gobra

@@ -0,0 +1,20 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package pkg
+
+type Calls interface {
+	pred inv()
+}
+
+ghost
+requires cs != nil
+preserves cs.inv()
+func ClosureSpec(ghost cs Calls) (res int)
+
+requires fn implements ClosureSpec{cs}
+requires cs != nil && cs.inv()
+ensures  cs.inv()
+func Invoke(fn func () (int), ghost cs Calls) int {
+    return fn() as ClosureSpec{cs}
+}