Skip to content

Commit

Permalink
Avoid name clashes with Default method (#6031)
Browse files Browse the repository at this point in the history
### What was changed?
Avoid name clash between user defined and Dafny generated Default method
for data types.

### How has this been tested?
Add test
Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3809.dfy

Fixes #3809 


<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
olivier-aws authored Jan 13, 2025
1 parent b79708e commit e7e3ed4
Show file tree
Hide file tree
Showing 5 changed files with 33 additions and 1 deletion.
1 change: 1 addition & 0 deletions Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -2490,6 +2490,7 @@ public override string PublicIdProtect(string name) {
case "ToString":
case "GetHashCode":
case "Main":
case "Default":
return "_" + name;
default:
return name;
Expand Down
3 changes: 2 additions & 1 deletion Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -2515,7 +2515,7 @@ private string IdName(Declaration decl) {
// Don't use Go_ because Capitalize might use it and we know there's a conflict
return "Go__" + decl.GetCompileName(Options);
} else {
return Capitalize(decl.GetCompileName(Options));
return IdProtect(Capitalize(decl.GetCompileName(Options)));
}
}

Expand Down Expand Up @@ -2579,6 +2579,7 @@ public override string PublicIdProtect(string name) {
case "String":
case "Equals":
case "EqualsGeneric":
case "Default":

// Built-in types (can also be used as functions)
case "bool":
Expand Down
1 change: 1 addition & 0 deletions Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -2440,6 +2440,7 @@ private static string PublicIdProtectAux(string name) {
case "toString":
case "equals":
case "hashCode":
case "Default":
return name + "_"; // TODO: figure out what to do here (C# uses @, Go uses _, JS uses _$$_)
default:
return name; // Package name is not a keyword, so it can be used
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s"

module m {
datatype D = A
| B
| C {
static const Default: D := B // This one will be translated as Default_
method Default_() { // Just to be sure there is no clash: this is translated as Default__
print "Default_ Method\n";
}
}



method Main() {
var x := D.Default;
x.Default_();
match x {
case A => print "A!\n";
case B => print "B!\n";
case C => print "C!\n";
}
print "Hello!\n";
}

}
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Default_ Method
B!
Hello!

0 comments on commit e7e3ed4

Please sign in to comment.