diff --git a/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala b/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala index dbbce3b7b..1fa123add 100644 --- a/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala +++ b/src/main/scala/viper/gobra/ast/internal/transform/CGEdgesTerminationTransform.scala @@ -156,7 +156,7 @@ object CGEdgesTerminationTransform extends InternalTransform { // new body to check termination val terminationCheckBody = { val returnType = m.results.head.typ - val fallbackProxyCall = in.PureMethodCall(m.receiver, fallbackProxy, m.args, returnType)(src) + val fallbackProxyCall = in.PureMethodCall(m.receiver, fallbackProxy, m.args, returnType, false)(src) val implProxies: Vector[(in.Type, in.MemberProxy)] = implementations.toVector.flatMap{ impl => table.lookup(impl, proxy.name).map(implProxy => (impl, implProxy)) } @@ -166,7 +166,7 @@ object CGEdgesTerminationTransform extends InternalTransform { case implProxy: in.MethodProxy if !subT.isInstanceOf[in.InterfaceT] => in.Conditional( in.EqCmp(in.TypeOf(m.receiver)(src), typeAsExpr(subT)(src))(src), - in.PureMethodCall(in.TypeAssertion(m.receiver, subT)(src), implProxy, m.args, returnType)(src), + in.PureMethodCall(in.TypeAssertion(m.receiver, subT)(src), implProxy, m.args, returnType, false)(src), accum, returnType )(src) diff --git a/src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala b/src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala index 883d861b6..96cd1051d 100644 --- a/src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala +++ b/src/main/scala/viper/gobra/ast/internal/transform/OverflowChecksTransform.scala @@ -34,18 +34,18 @@ object OverflowChecksTransform extends InternalTransform { // Adds pre-conditions stating the bounds of each argument and a post-condition to check if the body expression // overflows - case f@PureFunction(name, args, results, pres, posts, terminationMeasure, body) => body match { + case f@PureFunction(name, args, results, pres, posts, terminationMeasure, body, isOpaque) => body match { case Some(expr) => val newPost = posts ++ getPureBlockPosts(expr, results) - PureFunction(name, args, results, pres, newPost, terminationMeasure, body)(f.info) + PureFunction(name, args, results, pres, newPost, terminationMeasure, body, isOpaque)(f.info) case None => f } // Same as pure functions - case m@PureMethod(receiver, name, args, results, pres, posts, terminationMeasure, body) => body match { + case m@PureMethod(receiver, name, args, results, pres, posts, terminationMeasure, body, isOpaque) => body match { case Some(expr) => val newPost = posts ++ getPureBlockPosts(expr, results) - PureMethod(receiver, name, args, results, pres, newPost, terminationMeasure, body)(m.info) + PureMethod(receiver, name, args, results, pres, newPost, terminationMeasure, body, isOpaque)(m.info) case None => m } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala index 9629169a3..38d37c758 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala @@ -554,7 +554,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl => expr match { case PDot(base, _) => goEorT(base) - case PInvoke(base, args, None) => { + case PInvoke(base, args, None, _) => { val res1 = goEorT(base) val res2 = combineTriggerResults(args.map(validTriggerPattern)) combineTriggerResults(res1, res2) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala index 29112774b..e921faeae 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostMiscTyping.scala @@ -219,7 +219,7 @@ trait GhostMiscTyping extends BaseTyping { this: TypeInfoImpl => } implicit lazy val wellDefSpec: WellDefinedness[PSpecification] = createWellDef { - case n@ PFunctionSpec(pres, preserves, posts, terminationMeasures, _, _) => + case n@ PFunctionSpec(pres, preserves, posts, terminationMeasures, _, _, _) => pres.flatMap(assignableToSpec) ++ preserves.flatMap(assignableToSpec) ++ posts.flatMap(assignableToSpec) ++ preserves.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++ pres.flatMap(e => allChildren(e).flatMap(illegalPreconditionNode)) ++ diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala index b524fc44c..c28e33755 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/separation/GoifyingPrinter.scala @@ -77,8 +77,9 @@ class GoifyingPrinter(info: TypeInfoImpl) extends DefaultPrettyPrinter { * Shows the Goified version of the function / method specification */ override def showSpec(spec: PSpecification): Doc = spec match { - case PFunctionSpec(pres, preserves, posts, measures, isPure, isTrusted) => + case PFunctionSpec(pres, preserves, posts, measures, isPure, isTrusted, isOpaque) => (if (isPure) specComment <+> showPure else emptyDoc) <> + (if (isOpaque) specComment <+> showOpaque else emptyDoc) <> (if (isTrusted) specComment <+> showTrusted else emptyDoc) <> hcat(pres map (p => specComment <+> showPre(p) <> line)) <> hcat(preserves map (p => specComment <+> showPreserves(p) <> line)) <> diff --git a/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala index c5416a789..d5d7bb30a 100644 --- a/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/StringEncoding.scala @@ -298,7 +298,8 @@ class StringEncoding extends LeafTypeEncoding { pres = Vector(pre), posts = Vector(), terminationMeasures = Vector(in.WildcardMeasure(None)(info)), - body = None + body = None, + isOpaque = false )(info) val translatedFunc = ctx.function(func) translatedFunc.res diff --git a/src/main/scala/viper/gobra/translator/encodings/channels/ChannelEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/channels/ChannelEncoding.scala index 4a6d21074..d13147fa5 100644 --- a/src/main/scala/viper/gobra/translator/encodings/channels/ChannelEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/channels/ChannelEncoding.scala @@ -155,7 +155,7 @@ class ChannelEncoding extends LeafTypeEncoding { _ <- write(vprIsChannelInhale) // inhale [a].BufferSize() == [bufferSize] - bufferSizeCall = in.PureMethodCall(a, bufferSizeMProxy, Vector(), in.IntT(Addressability.outParameter))(makeStmt.info) + bufferSizeCall = in.PureMethodCall(a, bufferSizeMProxy, Vector(), in.IntT(Addressability.outParameter), false)(makeStmt.info) bufferSizeEq = in.EqCmp(bufferSizeCall, bufferSizeArg)(makeStmt.info) vprBufferSizeEq <- ctx.expression(bufferSizeEq) vprBufferSizeInhale = vpr.Inhale(vprBufferSizeEq)(pos, info, errT) @@ -262,7 +262,7 @@ class ChannelEncoding extends LeafTypeEncoding { private def getChannelInvariantAccess(channel: in.Expr, invariant: in.MethodProxy, args: Vector[in.Expr], argTypes: Vector[in.Type])(src: Source.Parser.Info): in.Access = { require(args.length == argTypes.length) val permReturnT = in.PredT(argTypes, Addressability.outParameter) - val permPred = in.PureMethodCall(channel, invariant, Vector(), permReturnT)(src) + val permPred = in.PureMethodCall(channel, invariant, Vector(), permReturnT, false)(src) in.Access(in.Accessible.PredExpr(in.PredExprInstance(permPred, args)(src)), in.FullPerm(src))(src) } } diff --git a/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala b/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala index 3a35fcd57..3b12c07bc 100644 --- a/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala +++ b/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala @@ -48,7 +48,7 @@ protected class ClosureSpecsEncoder { def callToClosureGetter(func: in.FunctionMemberOrLitProxy, captured: Vector[(in.Expr, in.Parameter.In)] = Vector.empty)(ctx: Context): CodeWriter[vpr.Exp] = { val errorTransformers = register(in.ClosureSpec(func, Map.empty)(func.info))(ctx, func.info) for { - exp <- ctx.expression(in.PureFunctionCall(closureGetterFunctionProxy(func), captured.map(c => c._1), genericFuncType)(func.info)) + exp <- ctx.expression(in.PureFunctionCall(closureGetterFunctionProxy(func), captured.map(c => c._1), genericFuncType, false)(func.info)) _ <- errorT(errorTransformers: _*) } yield exp } @@ -77,7 +77,7 @@ protected class ClosureSpecsEncoder { register(c.spec)(ctx, c.spec.info) for { - exp <- ctx.expression(in.PureFunctionCall(closureCallProxy(c.spec)(c.info), closureCallArgs(c.closure, c.args, c.spec)(ctx), c.typ)(c.info)) + exp <- ctx.expression(in.PureFunctionCall(closureCallProxy(c.spec)(c.info), closureCallArgs(c.closure, c.args, c.spec)(ctx), c.typ, false)(c.info)) callNode = exp.deepCollect{ case funcApp: vpr.FuncApp => funcApp }.head _ <- errorT(doesNotImplementSpecErr(callNode, c.closure.info.tag)) } yield exp @@ -208,7 +208,7 @@ protected class ClosureSpecsEncoder { val result = in.Parameter.Out(Names.closureArg, genericFuncType)(info) val satisfiesSpec = in.ExprAssertion(in.ClosureImplements(result, in.ClosureSpec(func, Map.empty)(info))(info))(info) val (args, captAssertions) = capturedArgsAndAssertions(ctx)(result, captured(ctx)(func), info) - val getter = in.PureFunction(proxy, args, Vector(result), Vector.empty, Vector(satisfiesSpec) ++ captAssertions, Vector.empty, None)(memberOrLit(ctx)(func).info) + val getter = in.PureFunction(proxy, args, Vector(result), Vector.empty, Vector(satisfiesSpec) ++ captAssertions, Vector.empty, None, false)(memberOrLit(ctx)(func).info) ctx.defaultEncoding.pureFunction(getter)(ctx) } @@ -282,7 +282,7 @@ protected class ClosureSpecsEncoder { Some(in.ExprAssertion(in.ClosureImplements(closurePar, specWithFuncArgs(spec, func))(spec.info))(spec.info)) else None val fromClosureGetter = if (captArgs.nonEmpty) Some(in.ExprAssertion(in.EqCmp(closurePar, - in.PureFunctionCall(closureGetterFunctionProxy(spec.func), captArgs, genericFuncType)(spec.info))(spec.info) + in.PureFunctionCall(closureGetterFunctionProxy(spec.func), captArgs, genericFuncType, false)(spec.info))(spec.info) )(spec.info)) else None val args = Vector(closurePar) ++ captArgs ++ func.args val pres = implementsAssertion.toVector ++ fromClosureGetter ++ func.pres @@ -300,12 +300,12 @@ protected class ClosureSpecsEncoder { ctx.defaultEncoding.function(func)(ctx) case f: in.PureFunction => val posts = func.posts ++ assertionFromPureFunctionBody(f.body, f.results.head) - val m = in.PureFunction(proxy, args, f.results, pres, posts, f.terminationMeasures, None)(spec.info) + val m = in.PureFunction(proxy, args, f.results, pres, posts, f.terminationMeasures, None, f.isOpaque)(spec.info) ctx.defaultEncoding.pureFunction(m)(ctx) case lit: in.PureFunctionLit => val body = if (spec.params.isEmpty) lit.body else None val posts = lit.posts ++ (if (spec.params.isEmpty) Vector.empty else assertionFromPureFunctionBody(lit.body, lit.results.head).toVector) - val func = in.PureFunction(proxy, args, lit.results, pres, posts, lit.terminationMeasures, body)(lit.info) + val func = in.PureFunction(proxy, args, lit.results, pres, posts, lit.terminationMeasures, body, false)(lit.info) ctx.defaultEncoding.pureFunction(func)(ctx) } } diff --git a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala index 1f70d737f..03828766f 100644 --- a/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/interfaces/InterfaceEncoding.scala @@ -742,7 +742,7 @@ class InterfaceEncoding extends LeafTypeEncoding { val itfSymb = ctx.lookup(p.superProxy).asInstanceOf[in.PureMethod] val vItfFun = ctx.defaultEncoding.pureMethod(itfSymb)(ctx).res - val body = p.body.getOrElse(in.PureMethodCall(p.receiver, p.subProxy, p.args, p.results.head.typ)(p.info)) + val body = p.body.getOrElse(in.PureMethodCall(p.receiver, p.subProxy, p.args, p.results.head.typ, false)(p.info)) val pureMethodDummy = ctx.defaultEncoding.pureMethod(in.PureMethod( receiver = p.receiver, @@ -752,7 +752,8 @@ class InterfaceEncoding extends LeafTypeEncoding { pres = Vector.empty, posts = Vector.empty, terminationMeasures = Vector.empty, - body = Some(body) + body = Some(body), + isOpaque = false )(p.info))(ctx) val pres = vItfFun.pres.map { pre => diff --git a/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala index df86ccff2..0299e76cc 100644 --- a/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/typeless/BuiltInEncoding.scala @@ -216,7 +216,7 @@ class BuiltInEncoding extends Encoding { val pres: Vector[in.Assertion] = Vector( in.Access(isChannelInst, in.WildcardPerm(src))(src), ) - in.PureMethod(recvParam, x.name, Vector(), Vector(kParam), pres, Vector(), Vector(), None)(src) + in.PureMethod(recvParam, x.name, Vector(), Vector(kParam), pres, Vector(), Vector(), None, false)(src) case (tag: ChannelInvariantMethodTag, recv: in.ChannelT) => /** @@ -242,7 +242,7 @@ class BuiltInEncoding extends Encoding { val pres: Vector[in.Assertion] = Vector( in.Access(chanPredicate, in.WildcardPerm(src))(src) ) - in.PureMethod(recvParam, x.name, Vector(), Vector(resParam), pres, Vector(), Vector(), None)(src) + in.PureMethod(recvParam, x.name, Vector(), Vector(resParam), pres, Vector(), Vector(), None, false)(src) case (InitChannelMethodTag, recv: in.ChannelT) => /** @@ -680,6 +680,6 @@ class BuiltInEncoding extends Encoding { */ private def builtInPureMethodCall(tag: BuiltInMethodTag, recv: in.Expr, args: Vector[in.Expr], retType: in.Type)(src: Source.Parser.Info)(ctx: Context): in.PureMethodCall = { val method = getOrGenerateMethod(tag, recv.typ, args.map(_.typ))(src)(ctx) - in.PureMethodCall(recv, method, args, retType)(src) + in.PureMethodCall(recv, method, args, retType, false)(src) } } diff --git a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala index a8a132b6e..c704199b8 100644 --- a/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala +++ b/src/test/scala/viper/gobra/parsing/ParserUnitTests.scala @@ -24,13 +24,13 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { test("Parser: Invoke") { frontend.parseExpOrFail("Contains(v)") should matchPattern { - case PInvoke(PNamedOperand(PIdnUse("Contains")), Vector(PNamedOperand(PIdnUse("v"))), None) => + case PInvoke(PNamedOperand(PIdnUse("Contains")), Vector(PNamedOperand(PIdnUse("v"))), None, false) => } } test("Parser: DotInvoke") { frontend.parseExpOrFail("self.Contains(v)") should matchPattern { - case PInvoke(PDot(PNamedOperand(PIdnUse("self")), PIdnUse("Contains")), Vector(PNamedOperand(PIdnUse("v"))), None) => + case PInvoke(PDot(PNamedOperand(PIdnUse("self")), PIdnUse("Contains")), Vector(PNamedOperand(PIdnUse("v"))), None, false) => } } @@ -42,13 +42,13 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { test("Parser: DoubleDotInvoke1") { frontend.parseExpOrFail("(self.Left).Contains(v)") should matchPattern { - case PInvoke(PDot(PDot(PNamedOperand(PIdnUse("self")), PIdnUse("Left")), PIdnUse("Contains")), Vector(PNamedOperand(PIdnUse("v"))), None) => + case PInvoke(PDot(PDot(PNamedOperand(PIdnUse("self")), PIdnUse("Left")), PIdnUse("Contains")), Vector(PNamedOperand(PIdnUse("v"))), None, false) => } } test("Parser: DoubleDotInvoke2") { frontend.parseExpOrFail("self.Left.Contains(v)") should matchPattern { - case PInvoke(PDot(PDot(PNamedOperand(PIdnUse("self")), PIdnUse("Left")), PIdnUse("Contains")), Vector(PNamedOperand(PIdnUse("v"))), None) => + case PInvoke(PDot(PDot(PNamedOperand(PIdnUse("self")), PIdnUse("Left")), PIdnUse("Contains")), Vector(PNamedOperand(PIdnUse("v"))), None, false) => } } @@ -120,13 +120,13 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { test("Parser: spec only function") { frontend.parseFunctionDecl("func foo() { b.bar() }", specOnly = true) should matchPattern { - case PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), false, false), None) => + case PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), false, false, false), None) => } } test("Parser: spec only function with nested blocks") { frontend.parseFunctionDecl("func foo() { if(true) { b.bar() } else { foo() } }", specOnly = true) should matchPattern { - case PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), false, false), None) => + case PFunctionDecl(PIdnDef("foo"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), false, false, false), None) => } } @@ -145,13 +145,13 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { test("Parser: fold mpredicate call") { frontend.parseStmtOrFail("fold (*(b.Rectangle)).RectMem(&r)") should matchPattern { - case PFold(PPredicateAccess(PInvoke(PDot(PDeref(PDot(PNamedOperand(PIdnUse("b")), PIdnUse("Rectangle"))), PIdnUse("RectMem")), Vector(PReference(PNamedOperand(PIdnUse("r")))), None), PFullPerm())) => + case PFold(PPredicateAccess(PInvoke(PDot(PDeref(PDot(PNamedOperand(PIdnUse("b")), PIdnUse("Rectangle"))), PIdnUse("RectMem")), Vector(PReference(PNamedOperand(PIdnUse("r")))), None, false), PFullPerm())) => } } test("Parser: fold fpredicate call") { frontend.parseStmtOrFail("fold b.RectMem(&r)") should matchPattern { - case PFold(PPredicateAccess(PInvoke(PDot(PNamedOperand(PIdnUse("b")), PIdnUse("RectMem")), Vector(PReference(PNamedOperand(PIdnUse("r")))), None), PFullPerm())) => + case PFold(PPredicateAccess(PInvoke(PDot(PNamedOperand(PIdnUse("b")), PIdnUse("RectMem")), Vector(PReference(PNamedOperand(PIdnUse("r")))), None, false), PFullPerm())) => } } @@ -159,7 +159,7 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { val modes: Set[Boolean] = Set(false, true) modes.foreach(specOnly => { frontend.parseFunctionDecl("func bar()", specOnly) should matchPattern { - case PFunctionDecl(PIdnDef("bar"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), false, false), None) => + case PFunctionDecl(PIdnDef("bar"), Vector(), PResult(Vector()), PFunctionSpec(Vector(), Vector(), Vector(), Vector(), false, false, false), None) => } }) } @@ -2516,7 +2516,7 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { test("Parser: should be able to parse an explicit short var decl") { frontend.parseStmtOrFail("ghost res := test(s)") should matchPattern { case PExplicitGhostStatement(PShortVarDecl( - Vector(PInvoke(PNamedOperand(PIdnUse("test")), Vector(PNamedOperand(PIdnUse("s"))), None)), + Vector(PInvoke(PNamedOperand(PIdnUse("test")), Vector(PNamedOperand(PIdnUse("s"))), None, false)), Vector(PIdnUnk("res")), Vector(false))) => } @@ -2525,7 +2525,7 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { test("Parser: should be able to parse an explicit short var decl with ghost in the declaration") { frontend.parseStmtOrFail("ghost ghostRes := test(s)") should matchPattern { case PExplicitGhostStatement(PShortVarDecl( - Vector(PInvoke(PNamedOperand(PIdnUse("test")), Vector(PNamedOperand(PIdnUse("s"))), None)), + Vector(PInvoke(PNamedOperand(PIdnUse("test")), Vector(PNamedOperand(PIdnUse("s"))), None, false)), Vector(PIdnUnk("ghostRes")), Vector(false))) => } @@ -2619,7 +2619,7 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { // 0xf8 == 248 val parseRes = frontend.parseExp("string(248)") inside (parseRes) { - case Right(PInvoke(PNamedOperand(PIdnUse("string")), Vector(PIntLit(value, Decimal)), None)) => value should be (0xf8) + case Right(PInvoke(PNamedOperand(PIdnUse("string")), Vector(PIntLit(value, Decimal)), None, false)) => value should be (0xf8) } } @@ -2643,19 +2643,19 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { test("Parser: should be able to parse normal termination measure") { frontend.parseFunctionDecl("decreases n; func factorial (n int) int") should matchPattern { - case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), None)), false, false), None) => + case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), None)), false, false, false), None) => } } test("Parser: should be able to parse underscore termination measure") { frontend.parseFunctionDecl("decreases _; func factorial (n int) int") should matchPattern { - case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PWildcardMeasure(None)), false, false), None) => + case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PWildcardMeasure(None)), false, false, false), None) => } } test("Parser: should be able to parse conditional termination measure" ) { frontend.parseFunctionDecl("decreases n if n>1; decreases _ if n<2; func factorial (n int) int") should matchPattern { - case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), Some(PGreater(PNamedOperand(PIdnUse("n")), PIntLit(one, Decimal)))), PWildcardMeasure(Some(PLess(PNamedOperand(PIdnUse("n")), PIntLit(two, Decimal))))), false, false), None) if one == 1 && two == 2 => + case PFunctionDecl(PIdnDef("factorial"), Vector(PNamedParameter(PIdnDef("n"), PIntType())), PResult(Vector(PUnnamedParameter(PIntType()))), PFunctionSpec(Vector(), Vector(), Vector(), Vector(PTupleTerminationMeasure(Vector(PNamedOperand(PIdnUse("n"))), Some(PGreater(PNamedOperand(PIdnUse("n")), PIntLit(one, Decimal)))), PWildcardMeasure(Some(PLess(PNamedOperand(PIdnUse("n")), PIntLit(two, Decimal))))), false, false, false), None) if one == 1 && two == 2 => } } @@ -2674,7 +2674,7 @@ class ParserUnitTests extends AnyFunSuite with Matchers with Inside { test("Parser: should be able to parse type conversions") { frontend.parseExpOrFail("uint8(1)") should matchPattern { - case PInvoke(PNamedOperand(PIdnUse("uint8")), Vector(x), None) if x == PIntLit(1) => + case PInvoke(PNamedOperand(PIdnUse("uint8")), Vector(x), None, false) if x == PIntLit(1) => } }