diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index d001837f05b..961ed13aa8e 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -110,8 +110,8 @@ void EmitImports(ConcreteSyntaxTree wr, out ConcreteSyntaxTree importWriter, out } } - public static string TransformToClassName(string baseName) => - Regex.Replace(baseName, "[^_A-Za-z0-9$]", "_"); + public string TransformToClassName(string baseName) => + IdProtect(Regex.Replace(baseName, "[^_A-Za-z0-9$]", "_")); public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) { var companion = TypeName_Companion(UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(mainMethod.EnclosingClass), wr, mainMethod.tok, mainMethod); @@ -167,11 +167,11 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef return wr; } - var import = CreateImport(moduleName, isDefault, externModule, libraryName); + ModuleName = PublicModuleIdProtect(moduleName); + var import = CreateImport(ModuleName, isDefault, externModule, libraryName); var filename = string.Format("{0}/{0}.go", import.Path); var w = wr.NewFile(filename); - ModuleName = moduleName; EmitModuleHeader(w); AddImport(import); @@ -2519,6 +2519,14 @@ public override string PublicIdProtect(string name) { } } + public string PublicModuleIdProtect(string name) { + if (name == "C") { + return "_C"; + } else { + return name; + } + } + protected override string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null) { return UserDefinedTypeName(udt, full: true, member: member); } @@ -2541,28 +2549,30 @@ private string UserDefinedTypeName(UserDefinedType udt, bool full, MemberDecl/*? } private string UserDefinedTypeName(TopLevelDecl cl, bool full, MemberDecl/*?*/ member = null) { + var enclosingModuleDefinitionId = PublicModuleIdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options)); if (IsExternMemberOfExternModule(member, cl)) { // omit the default class name ("_default") in extern modules, when the class is used to qualify an extern member Contract.Assert(!cl.EnclosingModuleDefinition.IsDefaultModule); // default module is not marked ":extern" - return IdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options)); + return enclosingModuleDefinitionId; } else { if (cl.IsExtern(Options, out var qual, out _)) { // No need to take into account the second argument to extern, since // it'll already be cl.CompileName if (qual == null) { - if (this.ModuleName == cl.EnclosingModuleDefinition.GetCompileName(Options)) { + if (this.ModuleName == enclosingModuleDefinitionId) { qual = ""; } else { - qual = cl.EnclosingModuleDefinition.GetCompileName(Options); + qual = enclosingModuleDefinitionId; } } // Don't use IdName since that'll capitalize, which is unhelpful for // built-in types return qual + (qual == "" ? "" : ".") + cl.GetCompileName(Options); - } else if (!full || cl.EnclosingModuleDefinition.TryToAvoidName || this.ModuleName == cl.EnclosingModuleDefinition.GetCompileName(Options)) { + + } else if (!full || cl.EnclosingModuleDefinition.TryToAvoidName || this.ModuleName == enclosingModuleDefinitionId) { return IdName(cl); } else { - return cl.EnclosingModuleDefinition.GetCompileName(Options) + "." + IdName(cl); + return enclosingModuleDefinitionId + "." + IdName(cl); } } } diff --git a/Test/git-issues/git-issue-4181.dfy b/Test/git-issues/git-issue-4181.dfy new file mode 100644 index 00000000000..1f6928be6ca --- /dev/null +++ b/Test/git-issues/git-issue-4181.dfy @@ -0,0 +1,11 @@ +// RUN: %testDafnyForEachCompiler "%s" + +module C { + method Test() { + print "done\n"; + } +} + +method Main(){ + C.Test(); +} \ No newline at end of file diff --git a/Test/git-issues/git-issue-4181.dfy.expect b/Test/git-issues/git-issue-4181.dfy.expect new file mode 100644 index 00000000000..19f86f493ab --- /dev/null +++ b/Test/git-issues/git-issue-4181.dfy.expect @@ -0,0 +1 @@ +done diff --git a/docs/dev/news/4181.fix b/docs/dev/news/4181.fix new file mode 100644 index 00000000000..26788364524 --- /dev/null +++ b/docs/dev/news/4181.fix @@ -0,0 +1 @@ +Reserved module identifiers correctly escaped in GoLang \ No newline at end of file