Allow outer function outputs in outline preconditions (Fix issue #1029)

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

@@ -152,9 +152,20 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl =>
 
   implicit lazy val wellDefSpec: WellDefinedness[PSpecification] = createWellDef {
     case n@ PFunctionSpec(pres, preserves, posts, terminationMeasures, _, isPure, _, isOpaque, _) =>
+      // Collect the named output parameters of the spec's owner so that we only
+      // reject references to those (and not to outputs of an enclosing function,
+      // method, or closure - which is relevant for outline statements and nested
+      // closure literals).
+      val ownOutParams: Vector[PNamedParameter] = tree.parent(n).head match {
+        case p: PCodeRootWithResult => p.result.outs.collect {
+          case np: PNamedParameter => np
+          case PExplicitGhostParameter(np: PNamedParameter) => np
+        }
+        case _ => Vector.empty
+      }
       pres.flatMap(assignableToSpec) ++ preserves.flatMap(assignableToSpec) ++ posts.flatMap(assignableToSpec) ++
-      preserves.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++
-      pres.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++
+      preserves.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode(_, ownOutParams))) ++
+      pres.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode(_, ownOutParams))) ++
       terminationMeasures.flatMap(wellDefTerminationMeasure) ++
       // if has conditional clause, all clauses must be conditional
       // can only have one non-conditional clause
@@ -229,13 +240,16 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl =>
     isExpr(e).out ++ assignableTo.errors(exprType(e), AssertionT, mayInit)(e) ++ isWeaklyPureExpr(e)
   }
 
-  private def illegalPreconditionNode(n: PNode): Messages = {
+  private def illegalPreconditionNode(n: PNode, ownOutParams: Vector[PNamedParameter]): Messages = {
     n match {
       case PLabeledOld(PLabelUse(PLabelNode.lhsLabel), _) => noMessages
       case n@ (_: POld | _: PLabeledOld) => message(n, s"old not permitted in precondition")
       case n@ (_: PBefore) => message(n, s"old not permitted in precondition")
-      case id: PIdnUse if entity(id).isInstanceOf[SymbolTable.OutParameter] =>
-        message(id, s"output parameter '${id.name}' cannot be referenced in a precondition")
+      case id: PIdnUse => entity(id) match {
+        case op: SymbolTable.OutParameter if ownOutParams.exists(_ eq op.decl) =>
+          message(id, s"output parameter '${id.name}' cannot be referenced in a precondition")
+        case _ => noMessages
+      }
       case _ => noMessages
     }
   }

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

@@ -0,0 +1,60 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+package issue001029
+
+// Output parameters of the surrounding function may be referenced in the
+// precondition of an outline statement and closures.
+
+ensures acc(r) && *r == 42
+func foo() (r *int) {
+	i@ := 0
+	r = &i
+
+	requires acc(r)
+	ensures  acc(r) && *r == 42
+	outline (
+		*r = 42
+	)
+	return
+}
+
+// The outer function's output is also accepted in `preserves` clauses of an
+// outline statement.
+ensures acc(r) && *r == 42
+func foo2() (r *int) {
+	i@ := 42
+	r = &i
+
+	preserves acc(r) && *r == 42
+	outline (
+		// nothing
+	)
+	return
+}
+
+// A closure literal declared inside a function may reference the outer
+// function's named output parameter in its precondition.
+ensures acc(r) && *r == 42
+func foo3() (r *int) {
+	i@ := 42
+	r = &i
+
+	c := requires acc(r) && *r == 42
+	     func nested() {
+		// nothing
+	}
+	return
+}
+
+// The check still rejects references to a closure's own output parameter in
+// the closure's own precondition.
+func bad() {
+	//:: ExpectedOutput(type_error)
+	c := requires s == 0
+	     ensures  s == 1
+	     func nested() (s int) {
+		return 1
+	}
+	return
+}