Fix 576

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

@@ -552,7 +552,7 @@ object Desugar {
       val (args, argSubs) = argsWithSubs.unzip
 
       val captured = decl match {
-        case d: PClosureDecl => info.capturedVariables(d)
+        case d: PClosureDecl => info.capturedLocalVariables(d)
         case _ => Vector.empty
       }
       val capturedWithSubs = captured map capturedVarD
@@ -684,7 +684,7 @@ object Desugar {
       val (args, _) = argsWithSubs.unzip
 
       val captured = decl match {
-        case d: PClosureDecl => info.capturedVariables(d)
+        case d: PClosureDecl => info.capturedLocalVariables(d)
         case _ => Vector.empty
       }
       val capturedWithSubs = captured map capturedVarD

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

@@ -42,5 +42,5 @@ trait TypeInfo extends ExternalTypeInfo {
   def freeModified(n: PNode): Vector[PIdnNode]
   def freeDeclared(n: PNode): Vector[PIdnNode]
 
-  def capturedVariables(decl: PClosureDecl): Vector[PIdnNode]
+  def capturedLocalVariables(decl: PClosureDecl): Vector[PIdnNode]
 }

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

@@ -266,10 +266,11 @@ trait Enclosing { this: TypeInfoImpl =>
     }
   }
 
-  override def capturedVariables(decl: PClosureDecl): Vector[PIdnNode] =
+  override def capturedLocalVariables(decl: PClosureDecl): Vector[PIdnNode] =
     capturedVariablesAttr(tree.parent(decl).head.asInstanceOf[PFunctionLit])
   private lazy val capturedVariablesAttr: PFunctionLit => Vector[PIdnNode] = {
     def capturedVar(x: PIdnNode, lit: PFunctionLit): Boolean = entity(x) match {
+      case _: SymbolTable.GlobalVariable => false
       case r: SymbolTable.Variable => !containedIn(enclosingScope(r.rep), lit)
       case _ => false
     }

src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala

@@ -218,7 +218,7 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
       literalAssignableTo.errors(lit, simplifiedT)(n)
 
     case f: PFunctionLit =>
-      capturedVariables(f.decl).flatMap(v => addressable.errors(enclosingExpr(v).get)(v)) ++
+      capturedLocalVariables(f.decl).flatMap(v => addressable.errors(enclosingExpr(v).get)(v)) ++
         wellDefVariadicArgs(f.args) ++
         f.id.fold(noMessages)(id => wellDefID(id).out)
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala

@@ -22,7 +22,7 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl =>
   private[typing] def wellDefGhostMisc(misc: PGhostMisc) = misc match {
     case c@PClosureSpecInstance(id, _) => resolve(id) match {
       case Some(ap.Function(_, f)) => wellDefClosureSpecInstanceParams(c, f.args zip exprOrTypeType(id).asInstanceOf[FunctionT].args)
-      case Some(ap.Closure(_, l)) => if (c.params.isEmpty || capturedVariables(l.lit.decl).isEmpty)
+      case Some(ap.Closure(_, l)) => if (c.params.isEmpty || capturedLocalVariables(l.lit.decl).isEmpty)
         wellDefClosureSpecInstanceParams(c, l.args zip exprOrTypeType(id).asInstanceOf[FunctionT].args)
         else error(c, s"function literal ${l.lit.id.get} captures variables, so it cannot be used to derive a parametrized spec instance")
       case _ => error(id, s"identifier $id does not identify a user-defined function or function literal")

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

@@ -0,0 +1,14 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package main
+
+var x /*@@@*/ int = 1
+
+func test() {
+	f :=
+		// @ requires acc(&x, _)
+		func /*@ g @*/ () int {
+			return x
+		}
+}