From f8227fec3e63f3863c9494aa816e2fee408d73a0 Mon Sep 17 00:00:00 2001 From: Jad Hamza Date: Wed, 28 Jul 2021 15:26:57 +0200 Subject: [PATCH] Add unchecked annotation to inlined body --- .../stainless/extraction/inlining/FunctionInlining.scala | 9 ++------- .../verification/invalid/InliningUnchecked.scala | 9 +++++++++ 2 files changed, 11 insertions(+), 7 deletions(-) create mode 100644 frontends/benchmarks/verification/invalid/InliningUnchecked.scala diff --git a/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala b/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala index 0e0f570382..56897f73ec 100644 --- a/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala +++ b/core/src/main/scala/stainless/extraction/inlining/FunctionInlining.scala @@ -73,7 +73,7 @@ trait FunctionInlining extends CachingPhase with IdentitySorts { self => val specced = BodyWithSpecs(tfd.fullBody) // simple path for inlining when all arguments are values, and the function's body doesn't contain other function invocations if (specced.specs.isEmpty && args.forall(isValue) && !exprOps.containsFunctionCalls(tfd.fullBody)) { - exprOps.replaceFromSymbols(tfd.params.zip(args).toMap, exprOps.freshenLocals(tfd.fullBody)) + annotated(exprOps.replaceFromSymbols(tfd.params.zip(args).toMap, exprOps.freshenLocals(tfd.fullBody)), Unchecked) } else { // We need to keep the body as-is for `@synthetic` methods, such as // `copy` or implicit conversions for implicit classes, in order to @@ -119,15 +119,10 @@ trait FunctionInlining extends CachingPhase with IdentitySorts { self => case _ => e } - val res = ValDef.fresh("inlined", tfd.returnType) val inlined = addPreconditionAssertions(addPostconditionAssumption(body)) - // We bind the inlined expression in a let to avoid propagating - // the @unchecked annotation to postconditions, etc. - val newBody = let(res, inlined, res.toVariable.setPos(fi)).setPos(fi) - - val result = (tfd.params zip args).foldRight(newBody) { + val result = (tfd.params zip args).foldRight(inlined) { case ((vd, e), body) => let(vd, e, body).setPos(fi) } diff --git a/frontends/benchmarks/verification/invalid/InliningUnchecked.scala b/frontends/benchmarks/verification/invalid/InliningUnchecked.scala new file mode 100644 index 0000000000..664e55d6f8 --- /dev/null +++ b/frontends/benchmarks/verification/invalid/InliningUnchecked.scala @@ -0,0 +1,9 @@ +object InliningUnchecked { + + @inline def f: Int = 0 + + def g: Int = { + f + }.ensuring(_ == 10) + +}