Skip to content

Commit

Permalink
Fix: --compile-suffix avoids the extra renaming of homonymous classes (
Browse files Browse the repository at this point in the history
…#6073)

Fixes #6072 

### What was changed?
I changed it so that the comparison between the module name and the
class name is done on the C# string, not the Dafny string vs. C# string.

### How has this been tested?
I added a check to ensure that in the generated C# code, the class named
`A` is not escaped when using `--compile-suffix`

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
MikaelMayer authored Jan 24, 2025
1 parent 0460827 commit 16afdc8
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 2 deletions.
2 changes: 1 addition & 1 deletion Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -270,7 +270,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
/// </summary>
private string protectedTypeName(TopLevelDecl dt) {
var protectedName = IdName(dt);
if (dt.EnclosingModuleDefinition is { Name: var moduleName } && moduleName == protectedName) {
if (dt.EnclosingModuleDefinition.GetCompileName(Options) == protectedName) {
return $"_{protectedName}";
}
return protectedName;
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,13 @@
// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s"
// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s"
// Extra check for the C# compiler with the --compile-suffix option.
// RUN: %baredafny build -t:cs --compile-suffix "%s"
// RUN: %OutputCheck --file-to-check "%S/git-issue-6014.cs" "%s"
// Just to make sure that if we use --compile-suffix, we don't do the escape
// CHECK: .*A_Compile\.A.*
// With the class named B_Compile, it becomes B__Compile so there should be no conflict
// Adding this test in case someone changes the underscore escaping rules to account for this possibility
// CHECK: .*B_Compile\.B__Compile.*


module State {

Expand All @@ -23,6 +32,9 @@ module Enclosing {
datatype A = Whatever
}

module B {
datatype B_Compile = Whatever
}
}

module UsingEnclosing {
Expand Down

0 comments on commit 16afdc8

Please sign in to comment.