Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Avoid name clashes with Default method #6031

Merged
merged 49 commits into from
Jan 13, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
49 commits
Select commit Hold shift + click to select a range
5bde019
Update test to run on all back-ends
olivier-aws Jan 3, 2025
32e1456
Change name of namespace if there is a name clash with a data type
olivier-aws Jan 6, 2025
f8333da
Adding fix files
olivier-aws Jan 6, 2025
2183843
Avoid issue when translating multiple times a module named Dafny
olivier-aws Jan 6, 2025
38af532
Updating .expect file
olivier-aws Jan 6, 2025
0000eb2
Addind newline
olivier-aws Jan 7, 2025
8758fa6
Fixing comment at the end of the namespace definition
olivier-aws Jan 7, 2025
63cf404
Adding comments
olivier-aws Jan 7, 2025
ffd7b41
Change logic to update name of class rather than name of namespace. M…
olivier-aws Jan 7, 2025
c217fb5
Remove debug code
olivier-aws Jan 7, 2025
8b8382d
Fix issue
olivier-aws Jan 7, 2025
33aae8f
Extension to classes within modules
olivier-aws Jan 7, 2025
f7e1492
Whitespace formatting
olivier-aws Jan 7, 2025
057771a
Fix cpp code generation and test
olivier-aws Jan 8, 2025
72d4da6
Test for CPP compiler
olivier-aws Jan 8, 2025
9244f82
Simplification to remove duplicate argument to CreateClass
olivier-aws Jan 8, 2025
96a8013
Fix tests
olivier-aws Jan 8, 2025
7ce2104
Fixing expect file
olivier-aws Jan 8, 2025
2a839d2
Fix test 4449
olivier-aws Jan 8, 2025
49cb090
Really fix test 4440
olivier-aws Jan 8, 2025
3897266
Update Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
olivier-aws Jan 9, 2025
d311c33
Adding Default as a protected name
olivier-aws Jan 9, 2025
b000601
Apply CR suggestions
olivier-aws Jan 9, 2025
0927bfe
Removing useless if-then-else
olivier-aws Jan 9, 2025
6c73672
Adding test files
olivier-aws Jan 9, 2025
06ece5a
Default protected name in CS also
olivier-aws Jan 9, 2025
87d818e
Renaming files
olivier-aws Jan 9, 2025
80d2341
Better test to check that Default is correct
olivier-aws Jan 9, 2025
22fe2cd
Fix Go case also
olivier-aws Jan 9, 2025
eb8a522
Remove extra comment
olivier-aws Jan 9, 2025
eccab32
Adding Default as a protected name
olivier-aws Jan 9, 2025
68b41b4
Adding test files
olivier-aws Jan 9, 2025
86c6209
Default protected name in CS also
olivier-aws Jan 9, 2025
137798e
Renaming files
olivier-aws Jan 9, 2025
8f990c8
Better test to check that Default is correct
olivier-aws Jan 9, 2025
10b5a1c
Fix Go case also
olivier-aws Jan 9, 2025
9685363
Improved test
olivier-aws Jan 9, 2025
7dee024
Really fix Go case
olivier-aws Jan 9, 2025
ba287a1
Merge branch 'master' into fix_3809
olivier-aws Jan 11, 2025
40435ca
Adding test files
olivier-aws Jan 9, 2025
2bb5d3c
Renaming files
olivier-aws Jan 9, 2025
ca639a9
Better test to check that Default is correct
olivier-aws Jan 9, 2025
fa41898
Update to .NET 8 (#5322)
atomb Jan 8, 2025
e1affea
Set a default verification time limit (#6028)
keyboardDrummer Jan 9, 2025
ca63bcf
Attempt at fixing nightly. (#6035)
keyboardDrummer Jan 10, 2025
8946261
Delete test for legacy CLI that tests broken behavior (#6037)
keyboardDrummer Jan 10, 2025
8f66814
Merge branch 'fix_3809' of https://github.com/olivier-aws/dafny into …
olivier-aws Jan 13, 2025
899cc29
Merge branch 'master' into fix_3809
olivier-aws Jan 13, 2025
df277dd
Merge branch 'master' into fix_3809
olivier-aws Jan 13, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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!
Loading