Support outlines in closures

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

@@ -1808,7 +1808,7 @@ object Desugar {
             } yield in.Seqn(Vector(dPre, exprAss, clauseBody))(src)
 
           case n: POutline =>
-            val name = s"${rootName(n, info)}$$${nm.relativeId(n, info)}"
+            val name = s"${rootName(n, info)}$$${nm.relativeIdEnclosingFuncOrMethodDecl(n, info)}"
             val pres = (n.spec.pres ++ n.spec.preserves) map preconditionD(ctx, info)
             val posts = (n.spec.preserves ++ n.spec.posts) map postconditionD(ctx, info)
             val terminationMeasures = sequence(n.spec.terminationMeasures map terminationMeasureD(ctx, info)).res
@@ -3808,6 +3808,13 @@ object Desugar {
         case decl: PMethodSig      => idName(decl.id, context)
         case decl: PMPredicateSig  => idName(decl.id, context)
         case decl: PDomainFunction => idName(decl.id, context)
+        case decl: PClosureDecl =>
+          // closure declarations do not have an associated name and may be arbitrarily nested.
+          // to simplify, we just return the enclosing function or method's name
+          info.enclosingFunctionOrMethod(decl) match {
+            case Some(d) => idName(d.id, context)
+            case None => violation(s"Could not find a function or method declaration enclosing the closure declaration.")
+          }
         case _ => ??? // axiom and method-implementation-proof
       }
     }
@@ -4852,7 +4859,7 @@ object Desugar {
       * The id is of the form 'L$<a>$<b>' where a is the difference of the lines
       * of the node with the code root and b is the difference of the columns
       * of the node with the code root.
-      * If a differce is negative, the '-' character is replaced with '_'.
+      * If the difference is negative, the '-' character is replaced with '_'.
       *
       * @param node the node we are interested in
       * @param info type info to get position information
@@ -4865,6 +4872,25 @@ object Desugar {
       ("L$" + (lpos.line - rpos.line) + "$" + (lpos.column - rpos.column)).replace("-", "_")
     }
 
+    /**
+      * Returns an id for a node with respect to its enclosing function or method declaration.
+      * The id is of the form 'L$<a>$<b>' where a is the difference of the lines
+      * of the node with the enclosing declaration and b is the difference of the columns
+      * of the node with the enclosing declaration.
+      * If the difference is negative, the '-' character is replaced with '_'.
+      *
+      * @param node the node we are interested in
+      * @param info type info to get position information
+      * @return     string
+      */
+    def relativeIdEnclosingFuncOrMethodDecl(node: PNode, info: TypeInfo) : String = {
+      val pom = info.getTypeInfo.tree.originalRoot.positions
+      val lpos = pom.positions.getStart(node).get
+      val enclosingMember = info.enclosingFunctionOrMethod(node).get
+      val rpos = pom.positions.getStart(enclosingMember).get
+      ("L$" + (lpos.line - rpos.line) + "$" + (lpos.column - rpos.column)).replace("-", "_")
+    }
+
     /** returns the relativeId with the CONTINUE_LABEL_SUFFIX appended */
     def continueLabel(loop: PGeneralForStmt, info: TypeInfo) : String = relativeId(loop, info) + CONTINUE_LABEL_SUFFIX
 

src/test/resources/regressions/features/outline/outline-simple2.gobra

@@ -93,4 +93,16 @@ func test6() {
 
     //:: ExpectedOutput(assert_error:assertion_error)
     assert x == 11
-}
+}
+
+func test7() {
+    f :=
+        ensures acc(y) && *y >= 5
+        func fspec() (y *int) {
+            ensures acc(&x) && x >= 5
+            outline (
+                x@ := 10
+            )
+            return &x
+        }
+}