From 035413f42b3ca5639747d4560ef2f81d795bef1a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 22 Apr 2025 16:38:15 +0200 Subject: [PATCH 01/16] Revert "Revert commits accidentally pushed to master" This reverts commit 0b571feceb840e373299760cf063056bdf5e0253. --- .../scala/viper/gobra/ast/frontend/Ast.scala | 12 ++- .../gobra/frontend/ParseTreeTranslator.scala | 2 +- .../implementation/typing/MemberTyping.scala | 6 +- .../implementation/typing/TypeTyping.scala | 2 + .../typing/ghost/GhostMemberTyping.scala | 75 ++++++++++++------- .../resources/regressions/issues/000841.gobra | 18 +++++ 6 files changed, 81 insertions(+), 34 deletions(-) create mode 100644 src/test/resources/regressions/issues/000841.gobra diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala index 1e83156a9..59a326cb9 100644 --- a/src/main/scala/viper/gobra/ast/frontend/Ast.scala +++ b/src/main/scala/viper/gobra/ast/frontend/Ast.scala @@ -874,9 +874,15 @@ object PGhostifier { * Termination Measures */ -sealed trait PTerminationMeasure extends PNode -case class PWildcardMeasure(cond: Option[PExpression]) extends PTerminationMeasure -case class PTupleTerminationMeasure(tuple: Vector[PExpression], cond: Option[PExpression]) extends PTerminationMeasure +sealed trait PTerminationMeasure extends PNode { + val isConditional: Boolean +} +case class PWildcardMeasure(cond: Option[PExpression]) extends PTerminationMeasure { + override val isConditional: Boolean = cond.nonEmpty +} +case class PTupleTerminationMeasure(tuple: Vector[PExpression], cond: Option[PExpression]) extends PTerminationMeasure { + override val isConditional: Boolean = cond.nonEmpty +} /** * Specification diff --git a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala index f38cd8aef..d45d71a7b 100644 --- a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala +++ b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala @@ -428,7 +428,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole override def visitMethodSpec(ctx: GobraParser.MethodSpecContext): PMethodSig = { val ghost = has(ctx.GHOST()) val spec = if (ctx.specification() != null) - visitSpecification(ctx.specification()) + visitSpecification(ctx.specification()).at(ctx) else PFunctionSpec(Vector.empty,Vector.empty,Vector.empty, Vector.empty, Vector.empty).at(ctx) // The name of each explicitly specified method must be unique and not blank. diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala index d7c03e0f6..96573ae7f 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala @@ -26,13 +26,11 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl => wellDefVariadicArgs(n.args) ++ wellDefIfPureFunction(n) ++ wellDefIfInitBlock(n) ++ - wellDefIfMain(n) ++ - wellFoundedIfNeeded(n) + wellDefIfMain(n) case m: PMethodDecl => wellDefVariadicArgs(m.args) ++ isReceiverType.errors(miscType(m.receiver))(member) ++ - wellDefIfPureMethod(m) ++ - wellFoundedIfNeeded(m) + wellDefIfPureMethod(m) case b: PConstDecl => b.specs.flatMap(wellDefConstSpec) case g: PVarDecl if isGlobalVarDeclaration(g) => diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala index 50631f6f9..504d5b1c6 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala @@ -66,7 +66,9 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => case t: PInterfaceType => val isRecursiveInterface = error(t, "invalid recursive interface", cyclicInterfaceDef(t)) if (isRecursiveInterface.isEmpty) { + val wellDefIfPureSig = t.methSpecs.flatMap { sig => wellDefIfPureSpec(sig.spec, sig.args, sig.result) } addressableMethodSet(InterfaceT(t, this)).errors(t) ++ + wellDefIfPureSig ++ containsRedeclarations(t) // temporary check } else { isRecursiveInterface diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala index d25b98706..bfaa8526b 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala @@ -7,17 +7,20 @@ package viper.gobra.frontend.info.implementation.typing.ghost import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages} -import viper.gobra.ast.frontend.{PBlock, PCodeRootWithResult, PExplicitGhostMember, PFPredicateDecl, PFunctionDecl, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMember, PMPredicateDecl, PMethodDecl, PMethodImplementationProof, PParameter, PReturn, PVariadicType, PWithBody} +import viper.gobra.ast.frontend._ import viper.gobra.frontend.info.base.SymbolTable.{MPredicateSpec, MethodImpl, MethodSpec} import viper.gobra.frontend.info.base.Type.{InterfaceT, Type, UnknownType} import viper.gobra.frontend.info.implementation.TypeInfoImpl import viper.gobra.frontend.info.implementation.typing.BaseTyping -import viper.gobra.util.Violation trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => private[typing] def wellDefGhostMember(member: PGhostMember): Messages = member match { - case PExplicitGhostMember(_) => noMessages + case PExplicitGhostMember(m) => m match { + case f: PFunctionDecl => wellFoundedIfNeeded(f.spec) + case m: PMethodDecl => wellFoundedIfNeeded(m.spec) + case _ => noMessages + } case PFPredicateDecl(_, args, body) => body.fold(noMessages)(assignableToSpec) ++ nonVariadicArguments(args) @@ -28,28 +31,38 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => nonVariadicArguments(args) } - private[typing] def wellFoundedIfNeeded(member: PMember): Messages = { - val spec = member match { - case m: PMethodDecl => m.spec - case f: PFunctionDecl => f.spec - case _ => Violation.violation("Unexpected member type") + // spec must come from a ghost or pure function + private[typing] def wellFoundedIfNeeded(spec: PFunctionSpec): Messages = { + val needsMeasure = !config.disableCheckTerminationPureFns + if (needsMeasure) { + isValidMeasureForGhostOrPure(spec) + } else noMessages + } + + private def isValidMeasureForGhostOrPure(spec: PFunctionSpec): Messages = { + // TODO: eventually, we should deprecate the flag `config.disableCheckTerminationPureFns` + val hasTerminationMeasureErrors = + error(spec, s"Pure and ghost functions and methods must have termination measures.", + spec.terminationMeasures.isEmpty) + // (João) Conditional termination measures are a very rarely used feature. They allow defining termination measures + // case-per-case. However, for pure or ghost functions and methods, we need to show that all conditions provided + // do cover all possible inputs, otherwise the function is not guaranteed to terminate. Implementing such a + // check would not be hard, but it would be more cumbersome (and in general, less efficient) than this syntactic check. + // If this feature is requested, I am happy to implement the more complete check, but for now, I will stick to + // this syntactic check. + val hasConditionalTerminationMeasureErrors = { + val conditionalMeasure = spec.terminationMeasures.find(_.isConditional) + conditionalMeasure match { + case Some(n) => error(n, "Conditional termination measures are not allowed in pure members.") + case None => noMessages + } } - val hasMeasureIfNeeded = - if (spec.isPure || isEnclosingGhost(member)) - config.disableCheckTerminationPureFns || spec.terminationMeasures.nonEmpty - else - true - val needsMeasureError = - error(member, "All pure or ghost functions and methods must have termination measures, but none was found for this member.", !hasMeasureIfNeeded) - needsMeasureError + hasTerminationMeasureErrors ++ hasConditionalTerminationMeasureErrors } private[typing] def wellDefIfPureMethod(member: PMethodDecl): Messages = { if (member.spec.isPure) { - isSingleResultArg(member) ++ - isSinglePureReturnExpr(member) ++ - isPurePostcondition(member.spec) ++ - nonVariadicArguments(member.args) + wellDefIfPureSpec(member.spec, member.args, member.result) ++ isSinglePureReturnExpr(member) } else noMessages } @@ -61,15 +74,23 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => private[typing] def wellDefIfPureFunction(member: PFunctionDecl): Messages = { if (member.spec.isPure) { - isSingleResultArg(member) ++ - isSinglePureReturnExpr(member) ++ - isPurePostcondition(member.spec) ++ - nonVariadicArguments(member.args) + wellDefIfPureSpec(member.spec, member.args, member.result) ++ isSinglePureReturnExpr(member) } else noMessages } - private def isSingleResultArg(member: PCodeRootWithResult): Messages = { - error(member, "For now, pure methods and pure functions must have exactly one result argument", member.result.outs.size != 1) + // This implements checks that are common to pure functions and pure methods. Checks that are specific to either + // (e.g., checks that may depend on the receiver of a method) should be implemented elsewhere. + private[typing] def wellDefIfPureSpec(spec: PFunctionSpec, args: Vector[PParameter], result: PResult) : Messages = { + if (spec.isPure) { + isSingleResultArg(result) ++ + isPurePostcondition(spec) ++ + nonVariadicArguments(args) ++ + wellFoundedIfNeeded(spec) + } else noMessages + } + + private def isSingleResultArg(result: PResult): Messages = { + error(result, "For now, pure methods and pure functions must have exactly one result argument", result.outs.size != 1) } private def isSinglePureReturnExpr(member: PWithBody): Messages = { @@ -93,6 +114,8 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => p: PParameter => error(p, s"Pure members cannot have variadic arguments, but got $p", p.typ.isInstanceOf[PVariadicType]) } + + override lazy val localImplementationProofs: Vector[(Type, InterfaceT, Vector[String], Vector[String])] = { val implementationProofs = tree.root.programs.flatMap(_.declarations.collect{ case m: PImplementationProof => m}) implementationProofs.flatMap { ip => diff --git a/src/test/resources/regressions/issues/000841.gobra b/src/test/resources/regressions/issues/000841.gobra new file mode 100644 index 000000000..d67371613 --- /dev/null +++ b/src/test/resources/regressions/issues/000841.gobra @@ -0,0 +1,18 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package issue000841 + +type J interface { + // Type error, pure function does not have termination measures. + //:: ExpectedOutput(type_error) + pure + // Type error, pure function cannot have variadic parameters. + //:: ExpectedOutput(type_error) + M(a ...int) int +} + +pure +//:: ExpectedOutput(type_error) +decreases _ if b +func f(b bool) bool \ No newline at end of file From 4db912e3235ca4a5c9fdb6038cb13909a1005a42 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 22 Apr 2025 16:44:47 +0200 Subject: [PATCH 02/16] add missing termination measures --- src/main/resources/stubs/encoding/binary/binary.gobra | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/main/resources/stubs/encoding/binary/binary.gobra b/src/main/resources/stubs/encoding/binary/binary.gobra index b5c63d26b..8cf68c97e 100644 --- a/src/main/resources/stubs/encoding/binary/binary.gobra +++ b/src/main/resources/stubs/encoding/binary/binary.gobra @@ -11,13 +11,16 @@ package binary // 16-, 32-, or 64-bit unsigned integers. type ByteOrder interface { requires acc(&b[0], _) && acc(&b[1], _) + decreases pure Uint16(b []byte) uint16 requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _) + decreases pure Uint32(b []byte) uint32 requires acc(&b[0], _) && acc(&b[1], _) && acc(&b[2], _) && acc(&b[3], _) requires acc(&b[4], _) && acc(&b[5], _) && acc(&b[6], _) && acc(&b[7], _) + decreases pure Uint64(b []byte) uint64 requires acc(&b[0]) && acc(&b[1]) @@ -250,6 +253,4 @@ pure func (b bigEndian) GoString() (res string) { return "binary.BigEndian" } // If v is neither of these, Size returns -1. // (joao) requires support for the reflect package decreases -func Size(v interface{}) int /*{ - return dataSize(reflect.Indirect(reflect.ValueOf(v))) -}*/ +func Size(v interface{}) int \ No newline at end of file From fa08b49fdbf9844ba8d9e1e248ef2ada4a4a3f52 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Tue, 22 Apr 2025 21:02:59 +0200 Subject: [PATCH 03/16] add more termination measures to stdlib packages --- src/main/resources/stubs/encoding/binary/binary.gobra | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main/resources/stubs/encoding/binary/binary.gobra b/src/main/resources/stubs/encoding/binary/binary.gobra index 8cf68c97e..542c6e5d2 100644 --- a/src/main/resources/stubs/encoding/binary/binary.gobra +++ b/src/main/resources/stubs/encoding/binary/binary.gobra @@ -40,6 +40,7 @@ type ByteOrder interface { decreases PutUint64(b []byte, uint64) + decreases pure String() string } From 83074a89a6d957bb4aa9a48be5f4f2de0940c254 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 17 Jul 2026 00:29:15 +0000 Subject: [PATCH 04/16] Restrict issue #841 regression test to always-checked rules; fix embeddedInterfaces-fail3 The requirement that pure members carry a termination measure is gated behind 'disableCheckTerminationPureFns', which the regression test suite disables, so that case cannot be exercised here. The test now covers the checks that always apply to pure interface method signatures: exactly one result, non-variadic parameters, and rejection of conditional termination measures. embeddedInterfaces-fail3 declared 'pure g()' with no result, which is now rejected at the interface itself (issue #841). Give it a result so the test keeps exercising its intended error: a non-pure method implementing a pure interface method. --- .../interfaces/embeddedInterfaces-fail3.gobra | 4 ++-- .../resources/regressions/issues/000841.gobra | 24 +++++++++++-------- 2 files changed, 16 insertions(+), 12 deletions(-) diff --git a/src/test/resources/regressions/features/interfaces/embeddedInterfaces-fail3.gobra b/src/test/resources/regressions/features/interfaces/embeddedInterfaces-fail3.gobra index a77a57d60..056c91cbc 100644 --- a/src/test/resources/regressions/features/interfaces/embeddedInterfaces-fail3.gobra +++ b/src/test/resources/regressions/features/interfaces/embeddedInterfaces-fail3.gobra @@ -10,14 +10,14 @@ type foo interface { } type bar interface { - pure g() + pure g() int } type test int func (x test) f() -func (x test) g() +func (x test) g() int //:: ExpectedOutput(type_error) test implements foo diff --git a/src/test/resources/regressions/issues/000841.gobra b/src/test/resources/regressions/issues/000841.gobra index 3f1a71d98..f0495c845 100644 --- a/src/test/resources/regressions/issues/000841.gobra +++ b/src/test/resources/regressions/issues/000841.gobra @@ -3,11 +3,21 @@ package issue000841 +// Issue #841: pure method signatures in an interface must satisfy the same +// requirements as pure implementations. Requiring a termination measure is +// gated behind the same flag as for pure functions and methods +// (`disableCheckTerminationPureFns`), which the regression test suite disables; +// hence this file exercises the requirements that are always checked: exactly +// one result parameter, non-variadic parameters, and the rejection of +// conditional termination measures. + type J interface { - // Type error, pure interface method does not have a termination measure. + // Type error, a pure interface method must have exactly one result parameter. + // The error is reported at the start of the method specification. //:: ExpectedOutput(type_error) + decreases pure - M1(a int) int + M1(a int) // Type error, we do not permit conditional termination measures for members that must terminate. //:: ExpectedOutput(type_error) @@ -15,20 +25,14 @@ type J interface { pure M2(a int) int + // Type error, a pure interface method cannot have variadic parameters. decreases pure - // Type error, pure interface method cannot have variadic parameters. //:: ExpectedOutput(type_error) M3(a ...int) int - - // Type error, pure interface method must have exactly one result parameter. - // The error is reported at the start of the method specification. - //:: ExpectedOutput(type_error) - decreases - pure - M4(a int) } +// Conditional termination measures are likewise rejected for top-level pure functions. pure //:: ExpectedOutput(type_error) decreases _ if b // we syntactically disallow conditional termination measures for members that must terminate From d1bda4f90102c7dad78dca6e60b0829e031e97c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 17 Jul 2026 04:46:37 +0000 Subject: [PATCH 05/16] Add unit tests for the termination-measure requirement on pure interface methods The regression-test suite runs with disableCheckTerminationPureFns = true, so the requirement that a pure interface method carry a termination measure cannot be exercised there. The type-checking unit tests, however, use the default Config() in which the check is enabled, so we add two tests: a pure interface method without a termination measure is rejected, and one with a measure is accepted. Addresses ArquintL's review comment on issue #841. --- .../gobra/typing/TypeTypingUnitTests.scala | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala index 270560fc5..a21cfcd69 100644 --- a/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala +++ b/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala @@ -343,6 +343,32 @@ class TypeTypingUnitTests extends AnyFunSuite with Matchers with Inside { assert (!frontend.areComparable(t1, t2)) } + // Regression tests for issue #841: pure method signatures declared in an interface must satisfy the same + // requirements as pure functions and methods, in particular they must carry a termination measure. This + // requirement is gated behind `disableCheckTerminationPureFns`, which the regression-test suite disables but + // the default `Config()` used by `TestFrontend` keeps enabled, so it can be exercised here. + private def pureInterfaceType(measures: Vector[PTerminationMeasure]): PInterfaceType = + PInterfaceType( + Vector.empty, + Vector(PMethodSig( + PIdnDef("M"), + Vector.empty, + PResult(Vector(PUnnamedParameter(PIntType()))), + PFunctionSpec(Vector.empty, measures, Vector.empty, isPure = true), + isGhost = false + )), + Vector.empty + ) + + test("Typing: a pure interface method without a termination measure is not well-defined") { + assert (!frontend.isWellDef(pureInterfaceType(Vector.empty)).valid) + } + + test("Typing: a pure interface method with a termination measure is well-defined") { + val measure = PTupleTerminationMeasure(Vector.empty, None) + assert (frontend.isWellDef(pureInterfaceType(Vector(measure))).valid) + } + /* ** Stubs, mocks, and other test setup */ From e14daf01047eb304397dbb6297144e67ac8b1cc8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 17 Jul 2026 09:07:24 +0000 Subject: [PATCH 06/16] Check pure-member termination measures uniformly in wellDefIfPureSpec Address review feedback on the scattered measure checks for pure interface methods: - wellDefIfPureSpec now validates the termination measure of every pure member (function, method, and interface method signature): it must be present (unless disableCheckTerminationPureFns) and non-conditional. It also asserts its precondition that the spec is pure. - wellFoundedIfNeeded / noConditionalMeasureIfGhostOrPure are renamed to wellFoundedIfGhost / noConditionalMeasureIfGhost and restricted to ghost (non-pure) members, since pure members are now handled uniformly; this avoids double-reporting. - The interface handling in wellDefType delegates pure-signature checks entirely to wellDefIfPureSpec and only rejects conditional measures for ghost (non-pure) signatures; wildcard measures remain rejected for all interface signatures. - Restructure the 000841 regression test into one-liner method signatures. Removes the TypeTypingUnitTests cases added earlier: the anonymous-interface harness does not exercise interface method-signature checks, so they did not test the intended behaviour. --- .../implementation/typing/MemberTyping.scala | 8 ++-- .../implementation/typing/TypeTyping.scala | 14 +++---- .../typing/ghost/GhostMemberTyping.scala | 38 +++++++++++++------ .../resources/regressions/issues/000841.gobra | 14 ++----- .../gobra/typing/TypeTypingUnitTests.scala | 26 ------------- 5 files changed, 40 insertions(+), 60 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala index edba1d39e..7a93c634d 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/MemberTyping.scala @@ -26,14 +26,14 @@ trait MemberTyping extends BaseTyping { this: TypeInfoImpl => wellDefIfPureFunction(n) ++ wellDefIfInitBlock(n) ++ wellDefIfMain(n) ++ - wellFoundedIfNeeded(n) ++ - noConditionalMeasureIfGhostOrPure(n) + wellFoundedIfGhost(n) ++ + noConditionalMeasureIfGhost(n) case m: PMethodDecl => wellDefVariadicArgs(m.args) ++ isReceiverType.errors(miscType(m.receiver))(member) ++ wellDefIfPureMethod(m) ++ - wellFoundedIfNeeded(m) ++ - noConditionalMeasureIfGhostOrPure(m) + wellFoundedIfGhost(m) ++ + noConditionalMeasureIfGhost(m) case b: PConstDecl => b.specs.flatMap(wellDefConstSpec) case g: PVarDecl if isGlobalVarDeclaration(g) => diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala index 7718b731f..b651eb48d 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala @@ -84,19 +84,17 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => case _ => noMessages } } + // Pure method signatures are checked uniformly in `wellDefIfPureSpec` (see `pureSigErrors`); here we only + // reject conditional termination measures for ghost (non-pure) method signatures. val sigsWithConditionalMeasuresErrors = t.methSpecs.flatMap { sig => - if (sig.isGhost || sig.spec.isPure) + if (sig.isGhost && !sig.spec.isPure) noConditionalMeasureErrors(sig.spec.terminationMeasures) else noMessages } - // Pure method signatures in an interface must satisfy the same requirements as pure implementations. - // This reuses the shared `wellDefIfPureSpec` checks and, as for pure functions and methods, requires a - // termination measure to be provided (unless termination checking of pure members is disabled). + // Pure method signatures in an interface must satisfy the same requirements as pure implementations, + // including having a meaningful termination measure. This is checked uniformly in `wellDefIfPureSpec`. val pureSigErrors = t.methSpecs.flatMap { sig => - if (sig.spec.isPure) - wellDefIfPureSpec(sig, sig.args, sig.spec) ++ - error(sig, "Pure interface methods must have termination measures, but none was found.", - !config.disableCheckTerminationPureFns && sig.spec.terminationMeasures.isEmpty) + if (sig.spec.isPure) wellDefIfPureSpec(sig, sig.args, sig.spec) else noMessages } methodSet.errors(t) ++ diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala index ff4039d56..9464299ab 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala @@ -28,29 +28,31 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => nonVariadicArguments(args) } - private[typing] def wellFoundedIfNeeded(member: PMember): Messages = { + // Pure members are checked uniformly in `wellDefIfPureSpec`; this only requires a termination measure for + // ghost (non-pure) functions and methods. + private[typing] def wellFoundedIfGhost(member: PMember): Messages = { val spec = member match { case m: PMethodDecl => m.spec case f: PFunctionDecl => f.spec case _ => Violation.violation("Unexpected member type") } val hasMeasureIfNeeded = - if (spec.isPure || isEnclosingGhost(member)) + if (isEnclosingGhost(member) && !spec.isPure) config.disableCheckTerminationPureFns || spec.terminationMeasures.nonEmpty else true - val needsMeasureError = - error(member, "All pure or ghost functions and methods must have termination measures, but none was found for this member.", !hasMeasureIfNeeded) - needsMeasureError + error(member, "All pure or ghost functions and methods must have termination measures, but none was found for this member.", !hasMeasureIfNeeded) } - private[typing] def noConditionalMeasureIfGhostOrPure(member: PMember): Messages = { + // Pure members are checked uniformly in `wellDefIfPureSpec`; this only rejects conditional termination + // measures for ghost (non-pure) functions and methods. + private[typing] def noConditionalMeasureIfGhost(member: PMember): Messages = { val spec = member match { case m: PMethodDecl => m.spec case f: PFunctionDecl => f.spec case _ => return noMessages } - if (spec.isPure || isEnclosingGhost(member)) + if (isEnclosingGhost(member) && !spec.isPure) noConditionalMeasureErrors(spec.terminationMeasures) else noMessages } @@ -91,15 +93,27 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => } // Well-definedness checks shared by pure functions, pure methods, and pure interface method signatures: - // exactly one result, pure postconditions, no `preserves` clauses, and non-variadic arguments. Checks that are - // specific to members with a body (e.g., a single pure return expression) or to a particular kind of member - // (e.g., `mayInit`, or the requirement to have a termination measure) are added by the callers. - // Precondition: `spec.isPure`. + // exactly one result, pure postconditions, no `preserves` clauses, non-variadic arguments, and a meaningful + // termination measure. Checks specific to members with a body (e.g., a single pure return expression) or to a + // particular kind of member (e.g., `mayInit`) are added by the callers. private[typing] def wellDefIfPureSpec(node: PCodeRootWithResult, args: Vector[PParameter], spec: PFunctionSpec): Messages = { + Violation.violation(spec.isPure, "wellDefIfPureSpec may only be called for the specification of a pure member.") isSingleResultArg(node) ++ isPurePostcondition(spec) ++ pureMembersCannotHavePreserves(spec) ++ - nonVariadicArguments(args) + nonVariadicArguments(args) ++ + wellFoundedMeasure(spec) + } + + // A pure member must have a meaningful termination measure: one must be provided (unless termination checking of + // pure members is disabled) and it must not be conditional, since we do not check that the conditions are + // exhaustive. Wildcard measures are additionally rejected for interface method signatures (see `wellDefType`), + // where their semantics is unclear; they remain allowed for pure functions and methods. + private def wellFoundedMeasure(spec: PFunctionSpec): Messages = { + val missingMeasureError = + error(spec, "Pure functions, methods, and interface methods must have termination measures, but none was found.", + !config.disableCheckTerminationPureFns && spec.terminationMeasures.isEmpty) + missingMeasureError ++ noConditionalMeasureErrors(spec.terminationMeasures) } private def isSingleResultArg(member: PCodeRootWithResult): Messages = { diff --git a/src/test/resources/regressions/issues/000841.gobra b/src/test/resources/regressions/issues/000841.gobra index f0495c845..978897808 100644 --- a/src/test/resources/regressions/issues/000841.gobra +++ b/src/test/resources/regressions/issues/000841.gobra @@ -13,27 +13,21 @@ package issue000841 type J interface { // Type error, a pure interface method must have exactly one result parameter. - // The error is reported at the start of the method specification. //:: ExpectedOutput(type_error) - decreases - pure - M1(a int) + decreases pure M1(a int) // Type error, we do not permit conditional termination measures for members that must terminate. //:: ExpectedOutput(type_error) decreases if a == 42 - pure - M2(a int) int + pure M2(a int) int // Type error, a pure interface method cannot have variadic parameters. decreases - pure //:: ExpectedOutput(type_error) - M3(a ...int) int + pure M3(a ...int) int } // Conditional termination measures are likewise rejected for top-level pure functions. -pure //:: ExpectedOutput(type_error) decreases _ if b // we syntactically disallow conditional termination measures for members that must terminate -func f(b bool) bool +pure func f(b bool) bool diff --git a/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala b/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala index a21cfcd69..270560fc5 100644 --- a/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala +++ b/src/test/scala/viper/gobra/typing/TypeTypingUnitTests.scala @@ -343,32 +343,6 @@ class TypeTypingUnitTests extends AnyFunSuite with Matchers with Inside { assert (!frontend.areComparable(t1, t2)) } - // Regression tests for issue #841: pure method signatures declared in an interface must satisfy the same - // requirements as pure functions and methods, in particular they must carry a termination measure. This - // requirement is gated behind `disableCheckTerminationPureFns`, which the regression-test suite disables but - // the default `Config()` used by `TestFrontend` keeps enabled, so it can be exercised here. - private def pureInterfaceType(measures: Vector[PTerminationMeasure]): PInterfaceType = - PInterfaceType( - Vector.empty, - Vector(PMethodSig( - PIdnDef("M"), - Vector.empty, - PResult(Vector(PUnnamedParameter(PIntType()))), - PFunctionSpec(Vector.empty, measures, Vector.empty, isPure = true), - isGhost = false - )), - Vector.empty - ) - - test("Typing: a pure interface method without a termination measure is not well-defined") { - assert (!frontend.isWellDef(pureInterfaceType(Vector.empty)).valid) - } - - test("Typing: a pure interface method with a termination measure is well-defined") { - val measure = PTupleTerminationMeasure(Vector.empty, None) - assert (frontend.isWellDef(pureInterfaceType(Vector(measure))).valid) - } - /* ** Stubs, mocks, and other test setup */ From dc554ec136be37fa0419c525aeae1221a1af9c28 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 17 Jul 2026 09:29:11 +0000 Subject: [PATCH 07/16] Fix parse error in 000841 regression test 'decreases pure M1(a int)' does not parse: the decreases clause consumes the following tokens as the measure and rejects the 'pure' keyword. Put 'decreases' on its own line; 'pure' directly before the method name parses fine. --- src/test/resources/regressions/issues/000841.gobra | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/test/resources/regressions/issues/000841.gobra b/src/test/resources/regressions/issues/000841.gobra index 978897808..d8873d4c4 100644 --- a/src/test/resources/regressions/issues/000841.gobra +++ b/src/test/resources/regressions/issues/000841.gobra @@ -14,7 +14,8 @@ package issue000841 type J interface { // Type error, a pure interface method must have exactly one result parameter. //:: ExpectedOutput(type_error) - decreases pure M1(a int) + decreases + pure M1(a int) // Type error, we do not permit conditional termination measures for members that must terminate. //:: ExpectedOutput(type_error) From 02e7cdd635a969e9344d6c76b82684b61e68e897 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Wed, 2 Sep 2026 20:57:22 +0000 Subject: [PATCH 08/16] Test that pure interface methods must have termination measures The main regression test suite runs with `disableCheckTerminationPureFns` set, so it cannot exercise the requirement that a pure member carries a termination measure. An in-file configuration cannot opt out of that setting either, since boolean flags are merged by disjunction. Add `GobraCheckTerminationTests`, which runs the files in `src/test/resources/check_termination` with the flag disabled, and a test file covering pure functions, pure methods, ghost functions and, following issue #841, pure interface method signatures. Extend the `000841` regression test to the requirements on pure method signatures that are checked regardless of that flag: exactly one result parameter, non-variadic parameters, no `preserves` clauses and pure postconditions. Conditional measures on pure interface methods are already covered by `features/termination/conditional-measure-ghost-pure-fail.gobra`. Also restore the commented-out body of `binary.Size`, which was dropped by an unrelated edit. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01SBDq9vf2yu39GBS6iWDFfx --- .../stubs/encoding/binary/binary.gobra | 4 +- .../pure-members-need-measures.gobra | 48 +++++++++++++++++++ .../resources/regressions/issues/000841.gobra | 47 +++++++++++------- .../gobra/GobraCheckTerminationTests.scala | 32 +++++++++++++ 4 files changed, 112 insertions(+), 19 deletions(-) create mode 100644 src/test/resources/check_termination/pure-members-need-measures.gobra create mode 100644 src/test/scala/viper/gobra/GobraCheckTerminationTests.scala diff --git a/src/main/resources/stubs/encoding/binary/binary.gobra b/src/main/resources/stubs/encoding/binary/binary.gobra index 542c6e5d2..d3f3b15a0 100644 --- a/src/main/resources/stubs/encoding/binary/binary.gobra +++ b/src/main/resources/stubs/encoding/binary/binary.gobra @@ -254,4 +254,6 @@ pure func (b bigEndian) GoString() (res string) { return "binary.BigEndian" } // If v is neither of these, Size returns -1. // (joao) requires support for the reflect package decreases -func Size(v interface{}) int \ No newline at end of file +func Size(v interface{}) int /*{ + return dataSize(reflect.Indirect(reflect.ValueOf(v))) +}*/ diff --git a/src/test/resources/check_termination/pure-members-need-measures.gobra b/src/test/resources/check_termination/pure-members-need-measures.gobra new file mode 100644 index 000000000..056bdfb6c --- /dev/null +++ b/src/test/resources/check_termination/pure-members-need-measures.gobra @@ -0,0 +1,48 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package pure_members_need_measures + +// Issue #841: pure method signatures declared in an interface must carry a termination measure, just +// like pure functions and pure methods. Unlike the main regression test suite, the files in this +// directory are checked with `disableCheckTerminationPureFns` disabled. + +type T struct{ f int } + +// Type error, a pure function must have a termination measure. +//:: ExpectedOutput(type_error) +pure func missingMeasureFunc(a int) int { + return a +} + +// Type error, a pure method must have a termination measure. +//:: ExpectedOutput(type_error) +pure func (t T) missingMeasureMethod(a int) int { + return a +} + +// Type error, a ghost function must have a termination measure. +ghost +//:: ExpectedOutput(type_error) +func missingMeasureGhostFunc(a int) int { + return a +} + +type I interface { + // Type error, a pure interface method must have a termination measure. + //:: ExpectedOutput(type_error) + pure MissingMeasure(a int) int + + decreases + pure HasMeasure(a int) int +} + +decreases +pure func withMeasureFunc(a int) int { + return a +} + +decreases +pure func (t T) withMeasureMethod(a int) int { + return a +} diff --git a/src/test/resources/regressions/issues/000841.gobra b/src/test/resources/regressions/issues/000841.gobra index d8873d4c4..74539cd68 100644 --- a/src/test/resources/regressions/issues/000841.gobra +++ b/src/test/resources/regressions/issues/000841.gobra @@ -3,32 +3,43 @@ package issue000841 -// Issue #841: pure method signatures in an interface must satisfy the same -// requirements as pure implementations. Requiring a termination measure is -// gated behind the same flag as for pure functions and methods -// (`disableCheckTerminationPureFns`), which the regression test suite disables; -// hence this file exercises the requirements that are always checked: exactly -// one result parameter, non-variadic parameters, and the rejection of -// conditional termination measures. +// Issue #841: pure method signatures declared in an interface must satisfy the same requirements as +// pure functions and pure methods. The requirement of carrying a termination measure is gated behind +// `disableCheckTerminationPureFns`, which this test suite enables; that case is covered by the tests +// in `src/test/resources/check_termination` instead. type J interface { - // Type error, a pure interface method must have exactly one result parameter. + // Type error, a pure member must have exactly one result parameter. //:: ExpectedOutput(type_error) decreases - pure M1(a int) + pure NoResult(a int) - // Type error, we do not permit conditional termination measures for members that must terminate. + // Type error, a pure member must have exactly one result parameter. //:: ExpectedOutput(type_error) - decreases if a == 42 - pure M2(a int) int + decreases + pure TwoResults(a int) (int, int) - // Type error, a pure interface method cannot have variadic parameters. decreases + // Type error, a pure member cannot have variadic parameters. + //:: ExpectedOutput(type_error) + pure Variadic(a ...int) int + + // Type error, a pure member cannot have preserves clauses. //:: ExpectedOutput(type_error) - pure M3(a ...int) int + preserves a > 0 + decreases + pure Preserves(a int) int + + // Type error, the postconditions of a pure member must be pure. + //:: ExpectedOutput(type_error) + ensures acc(x) + decreases + pure ImpurePostcondition(x *int) int } -// Conditional termination measures are likewise rejected for top-level pure functions. -//:: ExpectedOutput(type_error) -decreases _ if b // we syntactically disallow conditional termination measures for members that must terminate -pure func f(b bool) bool +// A pure method signature that satisfies all of the requirements above is accepted. +type K interface { + ensures res >= a + decreases + pure WellFormed(a int) (res int) +} diff --git a/src/test/scala/viper/gobra/GobraCheckTerminationTests.scala b/src/test/scala/viper/gobra/GobraCheckTerminationTests.scala new file mode 100644 index 000000000..fb61b9f89 --- /dev/null +++ b/src/test/scala/viper/gobra/GobraCheckTerminationTests.scala @@ -0,0 +1,32 @@ +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. +// +// Copyright (c) 2011-2026 ETH Zurich. + +package viper.gobra + +import org.bitbucket.inkytonik.kiama.util.Source +import viper.gobra.frontend.Config + +/** + * Runs the test files in `src/test/resources/check_termination` with `disableCheckTerminationPureFns` + * disabled, i.e., with the requirement that all pure and ghost members carry a termination measure. + * + * The main regression test suite ([[GobraTests]]) sets `disableCheckTerminationPureFns` to `true`, + * because adding termination measures to all of its test files is still pending work. Note that an + * in-file configuration (`// ##(...)`) cannot be used to opt out of that setting, as configurations + * are merged by taking the disjunction of the boolean flags. This suite exists so that the + * requirement itself can be tested; test files that are unrelated to termination checking belong to + * the main regression test suite instead. + */ +class GobraCheckTerminationTests extends GobraTests { + val checkTerminationPropertyName = "GOBRATESTS_CHECK_TERMINATION_DIR" + + val checkTerminationDir: String = System.getProperty(checkTerminationPropertyName, "check_termination") + + override val testDirectories: Seq[String] = Vector(checkTerminationDir) + + override protected def getConfig(source: Source): Config = + super.getConfig(source).copy(disableCheckTerminationPureFns = false) +} From 29b75ae601627dbdca2379dc638d0145a7339bd4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 3 Sep 2026 09:50:21 +0000 Subject: [PATCH 09/16] Require termination measures for ghost interface methods Ghost functions and methods must be guaranteed to terminate, but the method signatures declared in an interface were exempt from that requirement, the same inconsistency that issue #841 reports for `pure`. Ghost method signatures are now held to the requirement too. No ghost signature in the built-in definitions or in the stdlib stubs is affected, as all of them already carry a measure. Move the check itself into `TerminationTyping`, as `mustTerminateErrors`, so that the requirement is expressed once and every member that must terminate is checked against the same rule: ghost functions and methods, ghost interface method signatures, and, via `wellDefIfPureSpec`, all pure members. This replaces the copies of the rule that lived in `wellFoundedIfGhost` and in the interface case of `wellDefType`, and gives all of them a single error message. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01SBDq9vf2yu39GBS6iWDFfx --- .../gobra/frontend/ParseTreeTranslator.scala | 9 ++- .../typing/TerminationTyping.scala | 21 +++++- .../implementation/typing/TypeTyping.scala | 13 ++-- .../typing/ghost/GhostMemberTyping.scala | 32 ++------ ...ghost-and-pure-members-need-measures.gobra | 73 +++++++++++++++++++ .../pure-members-need-measures.gobra | 48 ------------ 6 files changed, 112 insertions(+), 84 deletions(-) create mode 100644 src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra delete mode 100644 src/test/resources/check_termination/pure-members-need-measures.gobra diff --git a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala index 0dc9198a2..eb35e0c35 100644 --- a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala +++ b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala @@ -436,10 +436,11 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole override def visitMethodSpec(ctx: GobraParser.MethodSpecContext): PMethodSig = { val ghost = has(ctx.GHOST()) val spec = if (ctx.specification() != null) - // `visitSpecification` does not position the node it returns; usually, this is done by `visitChildren` of the - // enclosing context, which we bypass here. We position the spec at the `specification` context, exactly as - // `visitChildren` does for the specs of function and method declarations, such that errors reported on the - // spec of an interface method signature (e.g., a missing termination measure) have a position. + // `visitSpecification` does not position the node it returns; usually, this is done by `visitChildren` of + // the enclosing context, which we bypass here. Without this, the specification of an interface method + // signature would be the only `PFunctionSpec` in the AST without a position, so any error reported on it + // would be rendered without a source location. We position it at the `specification` context, exactly as + // `visitChildren` does for the specs of function and method declarations. visitSpecification(ctx.specification()).at(ctx.specification()) else PFunctionSpec(Vector.empty, Vector.empty, Vector.empty).at(ctx) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala index fe7cf1ee5..99f2a51a9 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala @@ -7,7 +7,7 @@ package viper.gobra.frontend.info.implementation.typing import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error} -import viper.gobra.ast.frontend.{PTerminationMeasure, PTupleTerminationMeasure, PWildcardMeasure} +import viper.gobra.ast.frontend.{PFunctionSpec, PNode, PTerminationMeasure, PTupleTerminationMeasure, PWildcardMeasure} import viper.gobra.frontend.info.implementation.TypeInfoImpl /** @@ -46,6 +46,25 @@ trait TerminationTyping extends BaseTyping { this: TypeInfoImpl => isConditional(m)) } + /** + * Checks that `spec` guarantees that the member it belongs to terminates on every call, as Gobra + * requires of all ghost and pure members: functions, methods, and interface method signatures alike. + * The missing-measure error is reported on `node`, which should be the member or signature that + * `spec` specifies. + * + * Note that this does not simply reject the specifications for which `measuresGuaranteeTermination` + * does not hold, because that would collapse two distinct problems into one message. Instead, a + * missing measure and a conditional measure are reported separately, the latter on the offending + * measure itself. Reporting a missing measure is subject to `disableCheckTerminationPureFns`, + * whereas conditional measures are always rejected. + */ + private[typing] def mustTerminateErrors(node: PNode, spec: PFunctionSpec): Messages = { + val missingMeasureError = error(node, + "Ghost and pure functions, methods, and interface methods must have termination measures, but none was found.", + !config.disableCheckTerminationPureFns && spec.terminationMeasures.isEmpty) + missingMeasureError ++ noConditionalMeasureErrors(spec.terminationMeasures) + } + private[typing] def hasSameMeasureType(measures: Vector[PTerminationMeasure]): Boolean = { val tupleMeasureTypes = measures .collect { case ttm: PTupleTerminationMeasure => ttm } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala index 81fd853f6..a91d5e848 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala @@ -84,18 +84,17 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => case _ => noMessages } } - // Pure method signatures are checked uniformly in `wellDefIfPureSpec` (see `pureSigErrors`); here we only - // reject conditional termination measures for ghost (non-pure) method signatures. - val sigsWithConditionalMeasuresErrors = t.methSpecs.flatMap { sig => - if (sig.isGhost && !sig.spec.isPure) - noConditionalMeasureErrors(sig.spec.terminationMeasures) + // Ghost method signatures must be guaranteed to terminate, exactly like ghost functions and methods. + // Pure signatures, ghost or not, are covered by `pureSigErrors` below instead. + val ghostSigsMustTerminateErrors = t.methSpecs.flatMap { sig => + if (sig.isGhost && !sig.spec.isPure) mustTerminateErrors(sig, sig.spec) else noMessages } val interfaceMethodsNotAtomic = t.methSpecs.flatMap { sig => error(sig, s"Interface methods cannot be marked as atomic.", sig.spec.isAtomic) } // Pure method signatures in an interface must satisfy the same requirements as pure implementations, - // including having a meaningful termination measure. This is checked uniformly in `wellDefIfPureSpec`. + // including being guaranteed to terminate. This is checked uniformly in `wellDefIfPureSpec`. val pureSigErrors = t.methSpecs.flatMap { sig => if (sig.spec.isPure) wellDefIfPureSpec(sig, sig.args, sig.spec) else noMessages @@ -104,7 +103,7 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => error(t, "Interface declaration contains methods annotated with 'mayInit'.", methodsContainMayInit) ++ interfaceMethodsNotAtomic ++ sigsWithWildcardMeasuresErrors ++ - sigsWithConditionalMeasuresErrors ++ + ghostSigsMustTerminateErrors ++ pureSigErrors ++ containsRedeclarations(t) // temporary check } else { diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala index 1fd6b9019..b45a38430 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala @@ -28,21 +28,16 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => nonVariadicArguments(args) } - // Ghost functions and methods must be guaranteed to terminate, i.e., they must have a termination measure and - // that measure must not be conditional. Pure members, whether ghost or not, are checked uniformly in - // `wellDefIfPureSpec`, which is why they are excluded here. + // Ghost functions and methods must be guaranteed to terminate. Pure members, whether ghost or not, are + // checked uniformly in `wellDefIfPureSpec`, which is why they are excluded here. private[typing] def wellFoundedIfGhost(member: PMember): Messages = { val spec = member match { case m: PMethodDecl => m.spec case f: PFunctionDecl => f.spec case _ => Violation.violation("Unexpected member type") } - if (isEnclosingGhost(member) && !spec.isPure) { - val missingMeasureError = error(member, - "All ghost functions and methods must have termination measures, but none was found for this member.", - !config.disableCheckTerminationPureFns && spec.terminationMeasures.isEmpty) - missingMeasureError ++ noConditionalMeasureErrors(spec.terminationMeasures) - } else noMessages + if (isEnclosingGhost(member) && !spec.isPure) mustTerminateErrors(member, spec) + else noMessages } private def pureFunctionsDoNotNeedMayInitMsg = "Pure functions and methods cannot open package invariants," + @@ -81,27 +76,16 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => } // Well-definedness checks shared by pure functions, pure methods, and pure interface method signatures: - // exactly one result, pure postconditions, no `preserves` clauses, non-variadic arguments, and a meaningful - // termination measure. Checks specific to members with a body (e.g., a single pure return expression) or to a - // particular kind of member (e.g., `mayInit`) are added by the callers. + // exactly one result, pure postconditions, no `preserves` clauses, non-variadic arguments, and a termination + // measure that guarantees termination. Checks specific to members with a body (e.g., a single pure return + // expression) or to a particular kind of member (e.g., `mayInit`) are added by the callers. private[typing] def wellDefIfPureSpec(node: PCodeRootWithResult, args: Vector[PParameter], spec: PFunctionSpec): Messages = { Violation.violation(spec.isPure, "wellDefIfPureSpec may only be called for the specification of a pure member.") isSingleResultArg(node) ++ isPurePostcondition(spec) ++ pureMembersCannotHavePreserves(spec) ++ nonVariadicArguments(args) ++ - wellFoundedMeasure(spec) - } - - // A pure member must have a meaningful termination measure: one must be provided (unless termination checking of - // pure members is disabled) and it must not be conditional, since we do not check that the conditions are - // exhaustive. Wildcard measures are additionally rejected for interface method signatures (see `wellDefType`), - // where their semantics is unclear; they remain allowed for pure functions and methods. - private def wellFoundedMeasure(spec: PFunctionSpec): Messages = { - val missingMeasureError = - error(spec, "Pure functions, methods, and interface methods must have termination measures, but none was found.", - !config.disableCheckTerminationPureFns && spec.terminationMeasures.isEmpty) - missingMeasureError ++ noConditionalMeasureErrors(spec.terminationMeasures) + mustTerminateErrors(node, spec) } private[typing] def atomicMemberIsWellFormed(member: PMember): Messages = { diff --git a/src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra b/src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra new file mode 100644 index 000000000..637f74348 --- /dev/null +++ b/src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra @@ -0,0 +1,73 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package ghost_and_pure_members_need_measures + +// Ghost and pure members must be guaranteed to terminate on every call. Following issue #841, this +// includes the method signatures declared in an interface, which used to be exempt. Unlike the main +// regression test suite, the files in this directory are checked with `disableCheckTerminationPureFns` +// disabled. + +type T struct{ f int } + +// Type error, a pure function must have a termination measure. +//:: ExpectedOutput(type_error) +pure func missingMeasureFunc(a int) int { + return a +} + +// Type error, a pure method must have a termination measure. +//:: ExpectedOutput(type_error) +pure func (t T) missingMeasureMethod(a int) int { + return a +} + +// Type error, a ghost function must have a termination measure. +ghost +//:: ExpectedOutput(type_error) +func missingMeasureGhostFunc(a int) int { + return a +} + +// Type error, a ghost method must have a termination measure. +ghost +//:: ExpectedOutput(type_error) +func (t T) missingMeasureGhostMethod(a int) int { + return a +} + +type I interface { + // Type error, a pure interface method must have a termination measure. + //:: ExpectedOutput(type_error) + pure MissingMeasurePure(a int) int + + // Type error, a ghost interface method must have a termination measure. + //:: ExpectedOutput(type_error) + ghost MissingMeasureGhost(a int) + + decreases + pure HasMeasurePure(a int) int + + ghost + decreases + HasMeasureGhost(a int) + + // An interface method that is neither ghost nor pure need not terminate. + NeedNotTerminate(a int) +} + +decreases +pure func withMeasureFunc(a int) int { + return a +} + +decreases +pure func (t T) withMeasureMethod(a int) int { + return a +} + +ghost +decreases +func withMeasureGhostFunc(a int) int { + return a +} diff --git a/src/test/resources/check_termination/pure-members-need-measures.gobra b/src/test/resources/check_termination/pure-members-need-measures.gobra deleted file mode 100644 index 056bdfb6c..000000000 --- a/src/test/resources/check_termination/pure-members-need-measures.gobra +++ /dev/null @@ -1,48 +0,0 @@ -// Any copyright is dedicated to the Public Domain. -// http://creativecommons.org/publicdomain/zero/1.0/ - -package pure_members_need_measures - -// Issue #841: pure method signatures declared in an interface must carry a termination measure, just -// like pure functions and pure methods. Unlike the main regression test suite, the files in this -// directory are checked with `disableCheckTerminationPureFns` disabled. - -type T struct{ f int } - -// Type error, a pure function must have a termination measure. -//:: ExpectedOutput(type_error) -pure func missingMeasureFunc(a int) int { - return a -} - -// Type error, a pure method must have a termination measure. -//:: ExpectedOutput(type_error) -pure func (t T) missingMeasureMethod(a int) int { - return a -} - -// Type error, a ghost function must have a termination measure. -ghost -//:: ExpectedOutput(type_error) -func missingMeasureGhostFunc(a int) int { - return a -} - -type I interface { - // Type error, a pure interface method must have a termination measure. - //:: ExpectedOutput(type_error) - pure MissingMeasure(a int) int - - decreases - pure HasMeasure(a int) int -} - -decreases -pure func withMeasureFunc(a int) int { - return a -} - -decreases -pure func (t T) withMeasureMethod(a int) int { - return a -} From 7d7b73fb44636edb34bd8d12a1f9536a573b9157 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Thu, 3 Sep 2026 13:15:53 +0000 Subject: [PATCH 10/16] Check interface method signatures in a single place Address the review feedback that the same checks are spread over too many places: - Pull `args` up into `PCodeRootWithResult` (all of its implementors already declare it) and introduce `PCodeRootWithSpec` for the code roots that carry a specification of their own. `wellDefPureSpec` (previously `wellDefIfPureSpec`) then takes the member alone, instead of taking the member, its arguments and its specification as three separate parameters. - Introduce `wellDefMethodSig`, the counterpart of `wellDefActualMember` for the members declared by an interface. The interface case of `wellDefType` now maps it over the signatures instead of iterating over them four times, once per check. - Move the rejection of wildcard measures in interface methods to `TerminationTyping`, next to the other rules about termination measures. Position the specification in `visitSpecification` rather than at the call site in `visitMethodSpec`. This is idempotent with what `visitChildren` does for all other specifications, and it is a bug fix: the specification of an interface method signature was the only `PFunctionSpec` in the AST without a position, so the well-definedness checks that `wellDefSpec` reports on it crashed the type checker with a `NoSuchElementException`. The new `features/termination/interface-sig-measures-fail.gobra` covers those checks. Also test that conditional termination measures are rejected on ghost and pure interface methods. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01SBDq9vf2yu39GBS6iWDFfx --- .../scala/viper/gobra/ast/frontend/Ast.scala | 18 ++++++-- .../gobra/frontend/ParseTreeTranslator.scala | 12 ++--- .../typing/TerminationTyping.scala | 13 +++++- .../implementation/typing/TypeTyping.scala | 29 +----------- .../typing/ghost/GhostMemberTyping.scala | 46 +++++++++++++------ ...ghost-and-pure-members-need-measures.gobra | 11 +++++ .../interface-sig-measures-fail.gobra | 31 +++++++++++++ 7 files changed, 105 insertions(+), 55 deletions(-) create mode 100644 src/test/resources/regressions/features/termination/interface-sig-measures-fail.gobra diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala index 9d3e73eec..25e65daee 100644 --- a/src/main/scala/viper/gobra/ast/frontend/Ast.scala +++ b/src/main/scala/viper/gobra/ast/frontend/Ast.scala @@ -157,9 +157,19 @@ sealed trait PDependentDef extends PNode { sealed trait PCodeRoot extends PNode sealed trait PCodeRootWithResult extends PCodeRoot { + def args: Vector[PParameter] def result: PResult } +/** + * A code root that carries a specification: a function or method declaration, a closure declaration, or the + * signature of an interface method. Notably, this excludes `PMethodImplementationProof`, which inherits the + * specification of the interface method that it proves and thus does not have one of its own. + */ +sealed trait PCodeRootWithSpec extends PCodeRootWithResult { + def spec: PFunctionSpec +} + case class PConstDecl(specs: Vector[PConstSpec]) extends PActualMember with PActualStatement with PGhostifiableStatement with PGhostifiableMember with PDeclaration case class PConstSpec(typ: Option[PType], right: Vector[PExpression], left: Vector[PDefLikeId]) extends PNode @@ -183,7 +193,7 @@ case class PFunctionDecl( result: PResult, spec: PFunctionSpec, body: Option[(PBodyParameterInfo, PBlock)] - ) extends PFunctionOrClosureDecl with PFunctionOrMethodDecl with PCodeRootWithResult with PWithBody with PGhostifiableMember + ) extends PFunctionOrClosureDecl with PFunctionOrMethodDecl with PCodeRootWithSpec with PWithBody with PGhostifiableMember case class PMethodDecl( id: PIdnDef, @@ -192,7 +202,7 @@ case class PMethodDecl( result: PResult, spec: PFunctionSpec, body: Option[(PBodyParameterInfo, PBlock)] - ) extends PFunctionOrMethodDecl with PDependentDef with PScope with PCodeRootWithResult with PWithBody with PGhostifiableMember + ) extends PFunctionOrMethodDecl with PDependentDef with PScope with PCodeRootWithSpec with PWithBody with PGhostifiableMember sealed trait PTypeDecl extends PActualMember with PActualStatement with PGhostifiableStatement with PGhostifiableMember with PDeclaration { @@ -468,7 +478,7 @@ case class PFunctionLit(id: Option[PIdnDef], decl: PClosureDecl) extends PLitera case class PClosureDecl(args: Vector[PParameter], result: PResult, spec: PFunctionSpec, - body: Option[(PBodyParameterInfo, PBlock)]) extends PFunctionOrClosureDecl with PCodeRootWithResult with PActualMisc + body: Option[(PBodyParameterInfo, PBlock)]) extends PFunctionOrClosureDecl with PCodeRootWithSpec with PActualMisc case class PClosureSpecInstance(func: PNameOrDot, params: Vector[PKeyedElement]) extends PGhostMisc { require(params.forall(p => p.exp.isInstanceOf[PExpCompositeVal])) @@ -785,7 +795,7 @@ case class PInterfaceName(typ: PTypeName) extends PInterfaceClause // Felix: I see `isGhost` as part of the declaration and not as port of the specification. // In the past, I usually created some ghost wrapper for these cases, but I wanted to get rid of them in the future. -case class PMethodSig(id: PIdnDef, args: Vector[PParameter], result: PResult, spec: PFunctionSpec, isGhost: Boolean) extends PInterfaceClause with PDependentDef with PScope with PCodeRootWithResult +case class PMethodSig(id: PIdnDef, args: Vector[PParameter], result: PResult, spec: PFunctionSpec, isGhost: Boolean) extends PInterfaceClause with PDependentDef with PScope with PCodeRootWithSpec /** * Identifiers diff --git a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala index eb35e0c35..465eaa4d2 100644 --- a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala +++ b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala @@ -436,12 +436,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole override def visitMethodSpec(ctx: GobraParser.MethodSpecContext): PMethodSig = { val ghost = has(ctx.GHOST()) val spec = if (ctx.specification() != null) - // `visitSpecification` does not position the node it returns; usually, this is done by `visitChildren` of - // the enclosing context, which we bypass here. Without this, the specification of an interface method - // signature would be the only `PFunctionSpec` in the AST without a position, so any error reported on it - // would be rendered without a source location. We position it at the `specification` context, exactly as - // `visitChildren` does for the specs of function and method declarations. - visitSpecification(ctx.specification()).at(ctx.specification()) + visitSpecification(ctx.specification()) else PFunctionSpec(Vector.empty, Vector.empty, Vector.empty).at(ctx) // The name of each explicitly specified method must be unique and not blank. @@ -907,6 +902,9 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole /** * Visits Gobra specifications * + * The returned node is positioned here rather than by `visitChildren` of the enclosing context, because + * `visitMethodSpec` calls this method directly. Positioning it twice is harmless, as `visitChildren` positions + * it at the very same `specification` context. * */ override def visitSpecification(ctx: GobraParser.SpecificationContext): PFunctionSpec = { // Get the backend options if available @@ -944,7 +942,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole isAtomic = ctx.atomic, opensInvs = ctx.opensInv, mayBeUsedInInit = ctx.mayInit, - ) + ).at(ctx) } /** diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala index 99f2a51a9..72f9403ef 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala @@ -6,7 +6,7 @@ package viper.gobra.frontend.info.implementation.typing -import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error} +import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages} import viper.gobra.ast.frontend.{PFunctionSpec, PNode, PTerminationMeasure, PTupleTerminationMeasure, PWildcardMeasure} import viper.gobra.frontend.info.implementation.TypeInfoImpl @@ -39,6 +39,17 @@ trait TerminationTyping extends BaseTyping { this: TypeInfoImpl => case _ => false } + /** + * The semantics of wildcard termination measures in interface method specifications is not clear. + * Thus, they are rejected. + */ + private[typing] def noWildcardMeasureErrors(measures: Vector[PTerminationMeasure]): Messages = + measures.flatMap { + case w: PWildcardMeasure => + error(w, "Wildcard termination measures are not allowed in the specifications of interface methods.") + case _ => noMessages + } + private[typing] def noConditionalMeasureErrors(measures: Vector[PTerminationMeasure]): Messages = measures.flatMap { m => error(m, diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala index a91d5e848..57dab73f3 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TypeTyping.scala @@ -75,36 +75,9 @@ trait TypeTyping extends BaseTyping { this: TypeInfoImpl => } } - // The semantics of wildcard termination measures in interface method specifications is not clear. - // Thus, they are rejected. - val sigsWithWildcardMeasuresErrors = t.methSpecs.flatMap { sig => - sig.spec.terminationMeasures.flatMap { - case w: PWildcardMeasure => - error(w, s"Wildcard termination measures are not allowed in the specifications of interface methods.") - case _ => noMessages - } - } - // Ghost method signatures must be guaranteed to terminate, exactly like ghost functions and methods. - // Pure signatures, ghost or not, are covered by `pureSigErrors` below instead. - val ghostSigsMustTerminateErrors = t.methSpecs.flatMap { sig => - if (sig.isGhost && !sig.spec.isPure) mustTerminateErrors(sig, sig.spec) - else noMessages - } - val interfaceMethodsNotAtomic = t.methSpecs.flatMap { sig => - error(sig, s"Interface methods cannot be marked as atomic.", sig.spec.isAtomic) - } - // Pure method signatures in an interface must satisfy the same requirements as pure implementations, - // including being guaranteed to terminate. This is checked uniformly in `wellDefIfPureSpec`. - val pureSigErrors = t.methSpecs.flatMap { sig => - if (sig.spec.isPure) wellDefIfPureSpec(sig, sig.args, sig.spec) - else noMessages - } methodSet.errors(t) ++ error(t, "Interface declaration contains methods annotated with 'mayInit'.", methodsContainMayInit) ++ - interfaceMethodsNotAtomic ++ - sigsWithWildcardMeasuresErrors ++ - ghostSigsMustTerminateErrors ++ - pureSigErrors ++ + t.methSpecs.flatMap(wellDefMethodSig) ++ containsRedeclarations(t) // temporary check } else { isRecursiveInterface diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala index b45a38430..b640fb782 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala @@ -7,7 +7,7 @@ package viper.gobra.frontend.info.implementation.typing.ghost import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages} -import viper.gobra.ast.frontend.{PBlock, PCodeRootWithResult, PExplicitGhostMember, PFPredicateDecl, PFunctionDecl, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMPredicateDecl, PMember, PMethodDecl, PMethodImplementationProof, PParameter, PPreserves, PReturn, PVariadicType, PWithBody} +import viper.gobra.ast.frontend.{PBlock, PCodeRootWithResult, PCodeRootWithSpec, PExplicitGhostMember, PFPredicateDecl, PFunctionDecl, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMPredicateDecl, PMember, PMethodDecl, PMethodImplementationProof, PMethodSig, PParameter, PPreserves, PReturn, PVariadicType, PWithBody} import viper.gobra.frontend.info.base.SymbolTable.{MPredicateSpec, MethodImpl, MethodSpec} import viper.gobra.frontend.info.base.Type.{InterfaceT, Type, UnknownType} import viper.gobra.frontend.info.implementation.TypeInfoImpl @@ -29,7 +29,7 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => } // Ghost functions and methods must be guaranteed to terminate. Pure members, whether ghost or not, are - // checked uniformly in `wellDefIfPureSpec`, which is why they are excluded here. + // checked uniformly in `wellDefPureSpec`, which is why they are excluded here. private[typing] def wellFoundedIfGhost(member: PMember): Messages = { val spec = member match { case m: PMethodDecl => m.spec @@ -45,7 +45,7 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => private[typing] def wellDefIfPureMethod(member: PMethodDecl): Messages = { if (member.spec.isPure) { - wellDefIfPureSpec(member, member.args, member.spec) ++ + wellDefPureSpec(member) ++ isSinglePureReturnExpr(member) ++ error(member, pureFunctionsDoNotNeedMayInitMsg, member.spec.mayBeUsedInInit) } else noMessages @@ -69,23 +69,39 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => private[typing] def wellDefIfPureFunction(member: PFunctionDecl): Messages = { if (member.spec.isPure) { - wellDefIfPureSpec(member, member.args, member.spec) ++ + wellDefPureSpec(member) ++ isSinglePureReturnExpr(member) ++ error(member, pureFunctionsDoNotNeedMayInitMsg, member.spec.mayBeUsedInInit) } else noMessages } - // Well-definedness checks shared by pure functions, pure methods, and pure interface method signatures: - // exactly one result, pure postconditions, no `preserves` clauses, non-variadic arguments, and a termination - // measure that guarantees termination. Checks specific to members with a body (e.g., a single pure return - // expression) or to a particular kind of member (e.g., `mayInit`) are added by the callers. - private[typing] def wellDefIfPureSpec(node: PCodeRootWithResult, args: Vector[PParameter], spec: PFunctionSpec): Messages = { - Violation.violation(spec.isPure, "wellDefIfPureSpec may only be called for the specification of a pure member.") - isSingleResultArg(node) ++ - isPurePostcondition(spec) ++ - pureMembersCannotHavePreserves(spec) ++ - nonVariadicArguments(args) ++ - mustTerminateErrors(node, spec) + /** + * Well-definedness checks that every pure member must satisfy, whether it is a pure function, a pure method + * or the signature of a pure interface method: exactly one result, pure postconditions, no `preserves` + * clauses, non-variadic arguments, and a termination measure that guarantees termination. Checks specific to + * members with a body (e.g., a single pure return expression) or to a particular kind of member (e.g., + * `mayInit`) are added by the callers. + */ + private[typing] def wellDefPureSpec(member: PCodeRootWithSpec): Messages = { + Violation.violation(member.spec.isPure, "wellDefPureSpec may only be called for a pure member.") + isSingleResultArg(member) ++ + isPurePostcondition(member.spec) ++ + pureMembersCannotHavePreserves(member.spec) ++ + nonVariadicArguments(member.args) ++ + mustTerminateErrors(member, member.spec) + } + + /** + * Well-definedness checks for the signature of an interface method. This is the counterpart of + * `wellDefActualMember` for the members declared by an interface, and imposes the same requirements on ghost + * and pure signatures as the ones imposed on ghost and pure implementations. + */ + private[typing] def wellDefMethodSig(sig: PMethodSig): Messages = { + error(sig, "Interface methods cannot be marked as atomic.", sig.spec.isAtomic) ++ + noWildcardMeasureErrors(sig.spec.terminationMeasures) ++ + (if (sig.spec.isPure) wellDefPureSpec(sig) + else if (sig.isGhost) mustTerminateErrors(sig, sig.spec) + else noMessages) } private[typing] def atomicMemberIsWellFormed(member: PMember): Messages = { diff --git a/src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra b/src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra index 637f74348..7ef2e0984 100644 --- a/src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra +++ b/src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra @@ -45,6 +45,17 @@ type I interface { //:: ExpectedOutput(type_error) ghost MissingMeasureGhost(a int) + // Type error, a conditional measure does not guarantee that a pure interface method terminates. + //:: ExpectedOutput(type_error) + decreases a if a >= 0 + pure ConditionalMeasurePure(a int) int + + // Type error, a conditional measure does not guarantee that a ghost interface method terminates. + ghost + //:: ExpectedOutput(type_error) + decreases a if a >= 0 + ConditionalMeasureGhost(a int) + decreases pure HasMeasurePure(a int) int diff --git a/src/test/resources/regressions/features/termination/interface-sig-measures-fail.gobra b/src/test/resources/regressions/features/termination/interface-sig-measures-fail.gobra new file mode 100644 index 000000000..2427a874b --- /dev/null +++ b/src/test/resources/regressions/features/termination/interface-sig-measures-fail.gobra @@ -0,0 +1,31 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package interface_sig_measures_fail + +// The well-definedness checks that Gobra performs on a specification are reported on the +// specification itself. This used to crash the type checker for the specifications of interface +// method signatures, because those were the only `PFunctionSpec` nodes without a position. + +type I interface { + // Type error, a specification can contain at most one non-conditional termination measure. + //:: ExpectedOutput(type_error) + decreases + decreases n + M(n int) +} + +type J interface { + // Type error, all termination measures of a specification must have the same type. + //:: ExpectedOutput(type_error) + decreases n if n >= 0 + decreases b if b + N(n int, b bool) +} + +type K interface { + // Type error, wildcard termination measures are not allowed on interface methods. + //:: ExpectedOutput(type_error) + decreases _ + O(n int) +} From bfbf3fa1744543021cca5b0ec1534172e2f1420f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 4 Sep 2026 07:31:11 +0000 Subject: [PATCH 11/16] Check pure closure literals like all other pure members Pure closure literals were the one kind of pure member that no well-definedness check reached. As a result, Gobra silently accepted a closure with variadic parameters, a `preserves` clause, an impure postcondition or no termination measure, and it crashed while desugaring a pure closure whose body is not a single return of a pure expression: cl := pure func g() (x int, y int) { return 1, 2 } Logic error: unexpected pure function body: Vector(return 1, 2) `wellDefIfPureClosure` now applies `wellDefPureSpec` to them, exactly as `wellDefIfPureFunction` and `wellDefIfPureMethod` do for the corresponding declarations, so all of these are reported as type errors instead. The closure in `features/opaque/opaque-closure-fail1.gobra` had a `preserves` clause and a body that assigns before returning, neither of which is allowed in a pure member. Give it a well-formed body and precondition, so that the file keeps testing what it is about, namely that closures cannot be made opaque. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01SBDq9vf2yu39GBS6iWDFfx --- .../scala/viper/gobra/ast/frontend/Ast.scala | 2 +- .../implementation/typing/ExprTyping.scala | 3 +- .../typing/ghost/GhostMemberTyping.scala | 19 ++-- ...ghost-and-pure-members-need-measures.gobra | 15 ++++ .../closures/closures-fail-pure.gobra | 86 +++++++++++++++++++ .../opaque/opaque-closure-fail1.gobra | 7 +- 6 files changed, 120 insertions(+), 12 deletions(-) create mode 100644 src/test/resources/regressions/features/closures/closures-fail-pure.gobra diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala index 25e65daee..1c6ebe75c 100644 --- a/src/main/scala/viper/gobra/ast/frontend/Ast.scala +++ b/src/main/scala/viper/gobra/ast/frontend/Ast.scala @@ -478,7 +478,7 @@ case class PFunctionLit(id: Option[PIdnDef], decl: PClosureDecl) extends PLitera case class PClosureDecl(args: Vector[PParameter], result: PResult, spec: PFunctionSpec, - body: Option[(PBodyParameterInfo, PBlock)]) extends PFunctionOrClosureDecl with PCodeRootWithSpec with PActualMisc + body: Option[(PBodyParameterInfo, PBlock)]) extends PFunctionOrClosureDecl with PCodeRootWithSpec with PWithBody with PActualMisc case class PClosureSpecInstance(func: PNameOrDot, params: Vector[PKeyedElement]) extends PGhostMisc { require(params.forall(p => p.exp.isInstanceOf[PExpCompositeVal])) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala index 65895b96e..8ab1693ad 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala @@ -247,7 +247,8 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl => capturedLocalVariables(f.decl).flatMap(v => addressable.errors(enclosingExpr(v).get)(v)) ++ wellDefVariadicArgs(f.args) ++ f.id.fold(noMessages)(id => wellDefID(id).out) ++ - error(f, "Opaque function literals are not yet supported.", f.spec.isOpaque) + error(f, "Opaque function literals are not yet supported.", f.spec.isOpaque) ++ + wellDefIfPureClosure(f) case n: PInvoke => val mayInit = isEnclosingMayInit(n) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala index b640fb782..d8b3f2ccc 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMemberTyping.scala @@ -7,7 +7,7 @@ package viper.gobra.frontend.info.implementation.typing.ghost import org.bitbucket.inkytonik.kiama.util.Messaging.{Messages, error, noMessages} -import viper.gobra.ast.frontend.{PBlock, PCodeRootWithResult, PCodeRootWithSpec, PExplicitGhostMember, PFPredicateDecl, PFunctionDecl, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMPredicateDecl, PMember, PMethodDecl, PMethodImplementationProof, PMethodSig, PParameter, PPreserves, PReturn, PVariadicType, PWithBody} +import viper.gobra.ast.frontend.{PBlock, PCodeRootWithResult, PCodeRootWithSpec, PExplicitGhostMember, PFPredicateDecl, PFunctionDecl, PFunctionLit, PFunctionSpec, PGhostMember, PIdnUse, PImplementationProof, PMPredicateDecl, PMember, PMethodDecl, PMethodImplementationProof, PMethodSig, PParameter, PPreserves, PReturn, PVariadicType, PWithBody} import viper.gobra.frontend.info.base.SymbolTable.{MPredicateSpec, MethodImpl, MethodSpec} import viper.gobra.frontend.info.base.Type.{InterfaceT, Type, UnknownType} import viper.gobra.frontend.info.implementation.TypeInfoImpl @@ -75,12 +75,19 @@ trait GhostMemberTyping extends BaseTyping { this: TypeInfoImpl => } else noMessages } + private[typing] def wellDefIfPureClosure(lit: PFunctionLit): Messages = { + if (lit.spec.isPure) { + wellDefPureSpec(lit.decl) ++ + isSinglePureReturnExpr(lit.decl) ++ + error(lit, pureFunctionsDoNotNeedMayInitMsg, lit.spec.mayBeUsedInInit) + } else noMessages + } + /** - * Well-definedness checks that every pure member must satisfy, whether it is a pure function, a pure method - * or the signature of a pure interface method: exactly one result, pure postconditions, no `preserves` - * clauses, non-variadic arguments, and a termination measure that guarantees termination. Checks specific to - * members with a body (e.g., a single pure return expression) or to a particular kind of member (e.g., - * `mayInit`) are added by the callers. + * Well-definedness checks that every pure member must satisfy, whether it is a pure function, a pure method, + * a pure closure or the signature of a pure interface method: exactly one result, pure postconditions, no + * `preserves` clauses, non-variadic arguments, and a termination measure that guarantees termination. Checks + * specific to a particular kind of member (e.g., `mayInit`) are added by the callers. */ private[typing] def wellDefPureSpec(member: PCodeRootWithSpec): Messages = { Violation.violation(member.spec.isPure, "wellDefPureSpec may only be called for a pure member.") diff --git a/src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra b/src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra index 7ef2e0984..84105060d 100644 --- a/src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra +++ b/src/test/resources/check_termination/ghost-and-pure-members-need-measures.gobra @@ -67,6 +67,21 @@ type I interface { NeedNotTerminate(a int) } +func closures() { + // Type error, a pure closure must have a termination measure. + //:: ExpectedOutput(type_error) + cl := pure func g() (x int) { + return 0 + } + _ = cl + + cl2 := decreases + pure func h() (x int) { + return 0 + } + _ = cl2 +} + decreases pure func withMeasureFunc(a int) int { return a diff --git a/src/test/resources/regressions/features/closures/closures-fail-pure.gobra b/src/test/resources/regressions/features/closures/closures-fail-pure.gobra new file mode 100644 index 000000000..40f11d8e7 --- /dev/null +++ b/src/test/resources/regressions/features/closures/closures-fail-pure.gobra @@ -0,0 +1,86 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package closures_fail_pure + +// Pure closure literals must satisfy the same requirements as pure functions and pure methods. Note +// that the requirement of carrying a termination measure is gated behind +// `disableCheckTerminationPureFns`, which this test suite enables; that case is covered by the tests +// in `src/test/resources/check_termination` instead. + +func twoResults() { + // Type error, a pure member must have exactly one result parameter. + //:: ExpectedOutput(type_error) + cl := decreases + // Type error, the body of a pure member must be a single return of a pure expression. + //:: ExpectedOutput(type_error) + pure func g() (x int, y int) { + return 1, 2 + } + _ = cl +} + +func noResult() { + // Type error, a pure member must have exactly one result parameter. + //:: ExpectedOutput(type_error) + cl := decreases + // Type error, the body of a pure member must be a single return of a pure expression. + //:: ExpectedOutput(type_error) + pure func g() { + } + _ = cl +} + +func variadicArgs() { + cl := decreases + // Type error, a pure member cannot have variadic parameters. + //:: ExpectedOutput(type_error) + pure func g(a ...int) (x int) { + return 0 + } + _ = cl +} + +func preservesClause() { + // Type error, a pure member cannot have preserves clauses. + //:: ExpectedOutput(type_error) + cl := preserves true + decreases + pure func g() (x int) { + return 0 + } + _ = cl +} + +func impurePostcondition() { + y@ := 0 + // Type error, the postconditions of a pure member must be pure. + //:: ExpectedOutput(type_error) + cl := ensures acc(&y) + decreases + pure func g() (x int) { + return 0 + } + _ = cl +} + +func statementInBody() { + cl := decreases + // Type error, the body of a pure member must be a single return of a pure expression. + //:: ExpectedOutput(type_error) + pure func g() (x int) { + x = 0 + return x + } + _ = cl +} + +// A pure closure literal that satisfies all of the requirements above is accepted. +func wellFormed() { + cl := ensures res == 0 + decreases + pure func g() (res int) { + return 0 + } + assert cl() as g == 0 +} diff --git a/src/test/resources/regressions/features/opaque/opaque-closure-fail1.gobra b/src/test/resources/regressions/features/opaque/opaque-closure-fail1.gobra index 86f1f5272..87dc4653b 100644 --- a/src/test/resources/regressions/features/opaque/opaque-closure-fail1.gobra +++ b/src/test/resources/regressions/features/opaque/opaque-closure-fail1.gobra @@ -7,11 +7,10 @@ func main() { x@ := 0 // Closure cannot be made opaque //:: ExpectedOutput(type_error) - c := preserves acc(&x) - ensures x == old(x) + n && m == x + c := requires acc(&x, _) + ensures m == x + n opaque pure func f(n int) (m int) { - x += n; - return x + return x + n } } From 2eda1d1110ba71f19d86d652ce36770c02efb597 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 4 Sep 2026 07:37:04 +0000 Subject: [PATCH 12/16] Document why the termination checks need their own test suite Record why `GobraCheckTerminationTests` exists and what belongs in it, and point at it from the place where the main regression test suite disables the check, so that the next reader does not have to rediscover that an in-file configuration cannot opt out of that setting. Likewise, record in `mustTerminateErrors` why it does not test `!measuresGuaranteeTermination`: the two reject exactly the same specifications, and the difference is only a second, vaguer message for a specification whose measures are all conditional. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01SBDq9vf2yu39GBS6iWDFfx --- .../typing/TerminationTyping.scala | 15 ++++++++++----- .../gobra/GobraCheckTerminationTests.scala | 17 ++++++++++------- src/test/scala/viper/gobra/GobraTests.scala | 4 +++- 3 files changed, 23 insertions(+), 13 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala index 72f9403ef..a267ede03 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala @@ -63,11 +63,16 @@ trait TerminationTyping extends BaseTyping { this: TypeInfoImpl => * The missing-measure error is reported on `node`, which should be the member or signature that * `spec` specifies. * - * Note that this does not simply reject the specifications for which `measuresGuaranteeTermination` - * does not hold, because that would collapse two distinct problems into one message. Instead, a - * missing measure and a conditional measure are reported separately, the latter on the offending - * measure itself. Reporting a missing measure is subject to `disableCheckTerminationPureFns`, - * whereas conditional measures are always rejected. + * Ghost and pure members are held to a stricter rule than `measuresGuaranteeTermination`: they may + * not carry a conditional measure at all, not even next to a non-conditional one, because we do not + * check that the conditions of conditional measures cover all inputs. The two problems are therefore + * reported separately, the missing measure on `node` and each conditional measure on the measure + * itself, and only the former is subject to `disableCheckTerminationPureFns`. + * + * Testing `terminationMeasures.isEmpty` rather than `!measuresGuaranteeTermination(...)` makes no + * difference to which specifications are rejected: the two differ only when every measure of a + * specification is conditional, which `noConditionalMeasureErrors` rejects anyway. It only avoids a + * second, vaguer message for that one mistake. */ private[typing] def mustTerminateErrors(node: PNode, spec: PFunctionSpec): Messages = { val missingMeasureError = error(node, diff --git a/src/test/scala/viper/gobra/GobraCheckTerminationTests.scala b/src/test/scala/viper/gobra/GobraCheckTerminationTests.scala index fb61b9f89..f8464605b 100644 --- a/src/test/scala/viper/gobra/GobraCheckTerminationTests.scala +++ b/src/test/scala/viper/gobra/GobraCheckTerminationTests.scala @@ -11,14 +11,17 @@ import viper.gobra.frontend.Config /** * Runs the test files in `src/test/resources/check_termination` with `disableCheckTerminationPureFns` - * disabled, i.e., with the requirement that all pure and ghost members carry a termination measure. + * disabled, i.e., with the requirement that all ghost and pure members carry a termination measure. * - * The main regression test suite ([[GobraTests]]) sets `disableCheckTerminationPureFns` to `true`, - * because adding termination measures to all of its test files is still pending work. Note that an - * in-file configuration (`// ##(...)`) cannot be used to opt out of that setting, as configurations - * are merged by taking the disjunction of the boolean flags. This suite exists so that the - * requirement itself can be tested; test files that are unrelated to termination checking belong to - * the main regression test suite instead. + * This suite exists because that requirement cannot be tested from the main regression test suite: + * [[GobraTests]] sets `disableCheckTerminationPureFns` to `true`, as adding termination measures to + * all of its test files is still pending work, and an in-file configuration (`// ##(...)`) cannot opt + * out of that setting. In-file configurations are merged into the base configuration by taking the + * disjunction of the boolean flags (see `Config.merge`), so they can only ever turn this flag on. + * + * Only test files about that requirement belong here. Everything else, including the requirements on + * ghost and pure members that hold irrespective of the flag, belongs to the main regression test + * suite, which is where a reader looks for it. */ class GobraCheckTerminationTests extends GobraTests { val checkTerminationPropertyName = "GOBRATESTS_CHECK_TERMINATION_DIR" diff --git a/src/test/scala/viper/gobra/GobraTests.scala b/src/test/scala/viper/gobra/GobraTests.scala index f64568540..a016bbccc 100644 --- a/src/test/scala/viper/gobra/GobraTests.scala +++ b/src/test/scala/viper/gobra/GobraTests.scala @@ -57,7 +57,9 @@ class GobraTests extends AbstractGobraTests with BeforeAndAfterAll { cacheParserAndTypeChecker = cacheParserAndTypeChecker, z3Exe = z3Exe, // termination checks in functions are currently disabled in the tests. This can be enabled in the future, - // but requires some work to add termination measures all over the test suite. + // but requires some work to add termination measures all over the test suite. Test files that are about + // that requirement belong to `GobraCheckTerminationTests`, which overrides this setting; an in-file + // configuration cannot, as `Config.merge` only ever turns boolean flags on. disableCheckTerminationPureFns = true, ) From 844fa54a3586e37e8a160911e761e207e14122eb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 4 Sep 2026 09:58:10 +0200 Subject: [PATCH 13/16] Update src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala --- .../info/implementation/typing/TerminationTyping.scala | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala index a267ede03..48c506414 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala @@ -68,11 +68,6 @@ trait TerminationTyping extends BaseTyping { this: TypeInfoImpl => * check that the conditions of conditional measures cover all inputs. The two problems are therefore * reported separately, the missing measure on `node` and each conditional measure on the measure * itself, and only the former is subject to `disableCheckTerminationPureFns`. - * - * Testing `terminationMeasures.isEmpty` rather than `!measuresGuaranteeTermination(...)` makes no - * difference to which specifications are rejected: the two differ only when every measure of a - * specification is conditional, which `noConditionalMeasureErrors` rejects anyway. It only avoids a - * second, vaguer message for that one mistake. */ private[typing] def mustTerminateErrors(node: PNode, spec: PFunctionSpec): Messages = { val missingMeasureError = error(node, From 467f4fbd5e0735650a4e08e4550507cf700eaead Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 4 Sep 2026 09:58:19 +0200 Subject: [PATCH 14/16] Update src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala --- .../info/implementation/typing/TerminationTyping.scala | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala index 48c506414..fd6e58288 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/TerminationTyping.scala @@ -64,10 +64,10 @@ trait TerminationTyping extends BaseTyping { this: TypeInfoImpl => * `spec` specifies. * * Ghost and pure members are held to a stricter rule than `measuresGuaranteeTermination`: they may - * not carry a conditional measure at all, not even next to a non-conditional one, because we do not - * check that the conditions of conditional measures cover all inputs. The two problems are therefore - * reported separately, the missing measure on `node` and each conditional measure on the measure - * itself, and only the former is subject to `disableCheckTerminationPureFns`. + * not carry a conditional measure at all because we do not check that the conditions of conditional + * measures cover all inputs. The two problems are therefore reported separately, the missing + * measure on `node` and each conditional measure on the measure itself, and only the former + * is subject to `disableCheckTerminationPureFns`. */ private[typing] def mustTerminateErrors(node: PNode, spec: PFunctionSpec): Messages = { val missingMeasureError = error(node, From ae62d80b22026a011a89a18d250cfecf492852ba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 4 Sep 2026 09:58:27 +0200 Subject: [PATCH 15/16] Update src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala --- src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala index 465eaa4d2..0141ae4fb 100644 --- a/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala +++ b/src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala @@ -902,9 +902,6 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole /** * Visits Gobra specifications * - * The returned node is positioned here rather than by `visitChildren` of the enclosing context, because - * `visitMethodSpec` calls this method directly. Positioning it twice is harmless, as `visitChildren` positions - * it at the very same `specification` context. * */ override def visitSpecification(ctx: GobraParser.SpecificationContext): PFunctionSpec = { // Get the backend options if available From 309fbb148a9a900992998dd69b469da9df7aa12e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 4 Sep 2026 09:58:37 +0200 Subject: [PATCH 16/16] Update src/test/resources/regressions/features/opaque/opaque-closure-fail1.gobra --- .../regressions/features/opaque/opaque-closure-fail1.gobra | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/resources/regressions/features/opaque/opaque-closure-fail1.gobra b/src/test/resources/regressions/features/opaque/opaque-closure-fail1.gobra index 87dc4653b..0fa5b878c 100644 --- a/src/test/resources/regressions/features/opaque/opaque-closure-fail1.gobra +++ b/src/test/resources/regressions/features/opaque/opaque-closure-fail1.gobra @@ -7,7 +7,7 @@ func main() { x@ := 0 // Closure cannot be made opaque //:: ExpectedOutput(type_error) - c := requires acc(&x, _) + c := requires acc(&x) ensures m == x + n opaque pure func f(n int) (m int) {