Fix issue 573

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -162,13 +162,17 @@ sealed trait PFunctionOrClosureDecl extends PScope {
   def body: Option[(PBodyParameterInfo, PBlock)]
 }
 
+sealed trait PFunctionOrMethodDecl extends PNode with PScope {
+  def id: PIdnDef
+}
+
 case class PFunctionDecl(
                           id: PIdnDef,
                           args: Vector[PParameter],
                           result: PResult,
                           spec: PFunctionSpec,
                           body: Option[(PBodyParameterInfo, PBlock)]
-                        ) extends PFunctionOrClosureDecl with PActualMember with PCodeRootWithResult with PWithBody with PGhostifiableMember
+                        ) extends PFunctionOrClosureDecl with PActualMember with PCodeRootWithResult with PWithBody with PGhostifiableMember with PFunctionOrMethodDecl
 
 case class PMethodDecl(
                         id: PIdnDef,
@@ -177,7 +181,7 @@ case class PMethodDecl(
                         result: PResult,
                         spec: PFunctionSpec,
                         body: Option[(PBodyParameterInfo, PBlock)]
-                      ) extends PActualMember with PDependentDef with PScope with PCodeRootWithResult with PWithBody with PGhostifiableMember
+                      ) extends PActualMember with PDependentDef with PScope with PCodeRootWithResult with PWithBody with PGhostifiableMember with PFunctionOrMethodDecl
 
 sealed trait PTypeDecl extends PActualMember with PActualStatement with PGhostifiableStatement with PGhostifiableMember with PDeclaration {
 

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

@@ -246,7 +246,7 @@ object Desugar {
 
     def functionLitProxyD(lit: PFunctionLit, context: TypeInfo): in.FunctionLitProxy = {
       // If the literal is nameless, generate a unique name
-      val name = if (lit.id.isEmpty) nm.anonFuncLit(context.enclosingFunction(lit).get, context) else idName(lit.id.get, context)
+      val name = if (lit.id.isEmpty) nm.anonFuncLit(context.enclosingFunctionOrMethod(lit).get, context) else idName(lit.id.get, context)
       val info = if (lit.id.isEmpty) meta(lit, context) else meta(lit.id.get, context)
       in.FunctionLitProxy(name)(info)
     }
@@ -3653,7 +3653,7 @@ object Desugar {
         case _: st.GlobalVariable => nm.global(id.name, v.context)
         case _ => nm.variable(id.name, context.scope(id), v.context)
       }
-      case c: st.Closure => nm.funcLit(id.name, context.enclosingFunction(id).get, c.context)
+      case c: st.Closure => nm.funcLit(id.name, context.enclosingFunctionOrMethod(id).get, c.context)
       case sc: st.SingleConstant => nm.global(id.name, sc.context)
       case st.Embbed(_, _, _) | st.Field(_, _, _) => violation(s"expected that fields and embedded field are desugared by using embeddedDeclD resp. fieldDeclD but idName was called with $id")
       case n: st.NamedType => nm.typ(id.name, n.context)
@@ -4582,7 +4582,7 @@ object Desugar {
       s"${n}_$postfix${scopeMap(s)}" // deterministic
     }
 
-    private def nameWithEnclosingFunction(postfix: String)(n: String, enclosing: PFunctionDecl, context: ExternalTypeInfo): String = {
+    private def nameWithEnclosingFunction(postfix: String)(n: String, enclosing: PFunctionOrMethodDecl, context: ExternalTypeInfo): String = {
       maybeRegister(enclosing, context)
       s"${n}_${enclosing.id.name}_${context.pkgInfo.viperId}_$postfix${scopeMap(enclosing)}" // deterministic
     }
@@ -4608,8 +4608,8 @@ object Desugar {
     def mainFuncProofObligation(context: ExternalTypeInfo): String =
       topLevelName(MAIN_FUNC_OBLIGATIONS_PREFIX)(Constants.MAIN_FUNC_NAME, context)
     def variable(n: String, s: PScope, context: ExternalTypeInfo): String = name(VARIABLE_PREFIX)(n, s, context)
-    def funcLit(n: String, enclosing: PFunctionDecl, context: ExternalTypeInfo): String = nameWithEnclosingFunction(FUNCTION_PREFIX)(n, enclosing, context)
-    def anonFuncLit(enclosing: PFunctionDecl, context: ExternalTypeInfo): String = nameWithEnclosingFunction(FUNCTION_PREFIX)("func", enclosing, context) ++ s"_${fresh(enclosing, context)}"
+    def funcLit(n: String, enclosing: PFunctionOrMethodDecl, context: ExternalTypeInfo): String = nameWithEnclosingFunction(FUNCTION_PREFIX)(n, enclosing, context)
+    def anonFuncLit(enclosing: PFunctionOrMethodDecl, context: ExternalTypeInfo): String = nameWithEnclosingFunction(FUNCTION_PREFIX)("func", enclosing, context) ++ s"_${fresh(enclosing, context)}"
     def global  (n: String, context: ExternalTypeInfo): String = topLevelName(GLOBAL_PREFIX)(n, context)
     def typ     (n: String, context: ExternalTypeInfo): String = topLevelName(TYPE_PREFIX)(n, context)
     def field   (n: String, @unused s: StructT): String = s"$n$FIELD_PREFIX" // Field names must preserve their equality from the Go level

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

@@ -135,8 +135,6 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
   // They generate a unique PIdnNode whose name starts with "_" to not overlap any other identifiers
   private val goIdnDef = PIdnNodeEx(PIdnDef, term => Some(uniqueWildcard(PIdnDef, term).at(term)))
   private val goIdnDefList = PIdnNodeListEx(goIdnDef)
-  private val goIdnUnk = PIdnNodeEx(PIdnUnk, term => Some(uniqueWildcard(PIdnUnk, term).at(term)))
-  private val goIdnUnkList = PIdnNodeListEx(goIdnUnk)
 
   def uniqueWildcard[N](constructor : String => N, term : TerminalNode) : N = constructor("_"+term.getSymbol.getTokenIndex)
   //endregion

src/main/scala/viper/gobra/frontend/info/ExternalTypeInfo.scala

@@ -6,7 +6,7 @@
 
 package viper.gobra.frontend.info
 
-import viper.gobra.ast.frontend.{PCodeRoot, PEmbeddedDecl, PExpression, PFieldDecl, PGeneralForStmt, PFunctionDecl, PIdnNode, PIdnUse, PKeyedElement, PLabelUse, PMPredicateDecl, PMPredicateSig, PMember, PMethodDecl, PMethodSig, PMisc, PNode, PParameter, PPkgDef, PScope, PType}
+import viper.gobra.ast.frontend.{PCodeRoot, PEmbeddedDecl, PExpression, PFieldDecl, PFunctionDecl, PFunctionOrMethodDecl, PGeneralForStmt, PIdnNode, PIdnUse, PKeyedElement, PLabelUse, PMPredicateDecl, PMPredicateSig, PMember, PMethodDecl, PMethodSig, PMisc, PNode, PParameter, PPkgDef, PScope, PType}
 import viper.gobra.frontend.PackageInfo
 import viper.gobra.frontend.info.base.BuiltInMemberTag.BuiltInMemberTag
 import viper.gobra.frontend.info.base.Type.{AbstractType, InterfaceT, StructT, Type}
@@ -104,6 +104,9 @@ trait ExternalTypeInfo {
   /** if it exists, it returns the function that contains n */
   def enclosingFunction(n: PNode): Option[PFunctionDecl]
 
+  /** if it exists, it returns the function or method that contains n */
+  def enclosingFunctionOrMethod(n: PNode): Option[PFunctionOrMethodDecl]
+
   /** if it exists, it returns the for loop node that contains 'n' with label 'label' */
   def enclosingLabeledLoopNode(label: PLabelUse, n: PNode) : Option[PGeneralForStmt]
 

src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala

@@ -87,6 +87,8 @@ class TypeInfoImpl(final val tree: Info.GoTree, final val context: Info.Context,
 
   override def enclosingFunction(n: PNode): Option[PFunctionDecl] = tryEnclosingFunction(n)
 
+  override def enclosingFunctionOrMethod(n: PNode): Option[PFunctionOrMethodDecl] = tryEnclosingFunctionOrMethod(n)
+
   override def enclosingLabeledLoopNode(label: PLabelUse, n: PNode) : Option[PGeneralForStmt] = enclosingLabeledLoop(label, n).toOption
 
   override def enclosingLoopNode(n: PNode) : Option[PGeneralForStmt] = enclosingLoopUntilOutline(n).toOption

src/main/scala/viper/gobra/frontend/info/implementation/resolution/Enclosing.scala

@@ -72,6 +72,9 @@ trait Enclosing { this: TypeInfoImpl =>
   lazy val tryEnclosingFunction: PNode => Option[PFunctionDecl] =
     down[Option[PFunctionDecl]](None) { case m: PFunctionDecl => Some(m) }
 
+  lazy val tryEnclosingFunctionOrMethod: PNode => Option[PFunctionOrMethodDecl] =
+    down[Option[PFunctionOrMethodDecl]](None) { case f: PFunctionOrMethodDecl => Some(f) }
+
   lazy val tryEnclosingClosureImplementationProof: PNode => Option[PClosureImplProof] =
     down[Option[PClosureImplProof]](None) { case m: PClosureImplProof => Some(m) }
 

src/main/scala/viper/gobra/reporting/StatsCollector.scala

@@ -374,7 +374,7 @@ case class StatsCollector(reporter: GobraReporter) extends GobraReporter {
           isImported = isImported,
           isBuiltIn = isBuiltIn)
       // Consider the enclosing function, for closure declarations
-      case p: PClosureDecl => getMemberInformation(nodeTypeInfo.enclosingFunction(p).get, typeInfo, viperMember)
+      case p: PClosureDecl => getMemberInformation(nodeTypeInfo.enclosingFunctionOrMethod(p).get, typeInfo, viperMember)
       // Fallback to the node's code root if we can't match the node
       case p: PNode => getMemberInformation(nodeTypeInfo.codeRoot(p), typeInfo, viperMember)
     }

src/test/resources/regressions/issues/000573.go

@@ -0,0 +1,12 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+type X int
+
+func (s X) f() {
+	x := func /*@ g @*/ () {
+		return
+	}
+}