diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala index d384fbaf6..e4722936b 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala +++ b/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 } } diff --git a/src/test/resources/regressions/issues/001029.gobra b/src/test/resources/regressions/issues/001029.gobra new file mode 100644 index 000000000..7d6de6560 --- /dev/null +++ b/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 +}