From 719e203e636bf88a0e83449429542d17ee90a731 Mon Sep 17 00:00:00 2001 From: Jad Hamza Date: Sat, 27 Feb 2021 09:40:53 +0100 Subject: [PATCH] Prevent name mangling for exported functions in GenC (fix #921) --- .../scala/stainless/genc/phases/Scala2IRPhase.scala | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala index f45edf73fd..cd199e33ff 100644 --- a/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala +++ b/core/src/main/scala/stainless/genc/phases/Scala2IRPhase.scala @@ -140,8 +140,10 @@ private class S2IRImpl(val ctx: inox.Context, val ctxDB: FunCtxDB, val deps: Dep // rec(tfd.fd.id) + (if (tfd.tps.nonEmpty) buildIdPostfix(tfd.tps) else buildIdFromTypeMapping(tm)) // Include the "nesting path" in case of generic functions to avoid ambiguity - private def buildId(fa: FunAbstraction, tps: Seq[Type])(implicit tm: TypeMapping): CIR.Id = - rec(fa.id) + (if (tps.nonEmpty) buildIdPostfix(tps) else buildIdFromTypeMapping(tm)) + private def buildId(fa: FunAbstraction, tps: Seq[Type])(implicit tm: TypeMapping): CIR.Id = { + val exported = fa.isInstanceOf[Outer] && fa.asInstanceOf[Outer].fd.isExported + rec(fa.id, withUnique = !exported) + (if (tps.nonEmpty) buildIdPostfix(tps) else buildIdFromTypeMapping(tm)) + } private def buildId(ct: ClassType)(implicit tm: TypeMapping): CIR.Id = rec(ct.tcd.id) + buildIdPostfix(ct.tps) @@ -420,9 +422,9 @@ private class S2IRImpl(val ctx: inox.Context, val ctxDB: FunCtxDB, val deps: Dep /**************************************************************************************************** * Recursive conversion * ****************************************************************************************************/ - private def rec(id: Identifier): CIR.Id = { - if (id.name == "main") "main" - else id.uniqueNameDelimited("_") + private def rec(id: Identifier, withUnique: Boolean = true): CIR.Id = { + if (withUnique) id.uniqueNameDelimited("_") + else id.name } private def rec(vd: ValDef): CIR.Id = {