Skip to content

Commit

Permalink
Missing escaping when creating import of existing Go module (#5767)
Browse files Browse the repository at this point in the history
### Description
<!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md
-->
<!-- Is this a bug fix for an issue visible in the latest release?
Mention this in the PR details and ensure a patch release is considered
-->
See test for what this fixes: without this fix we end up with an import
on the consumer side that says `import Math ".../Math"` when the correct
name is `Math_`.

### How has this been tested?
Augmented the `timesTwo.dfy` separate compilation test.

<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>

---------

Co-authored-by: Mikael Mayer <[email protected]>
  • Loading branch information
robin-aws and MikaelMayer authored Oct 4, 2024
1 parent ab3d5d6 commit b5f57e0
Show file tree
Hide file tree
Showing 4 changed files with 17 additions and 1 deletion.
3 changes: 2 additions & 1 deletion Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -253,7 +253,8 @@ protected override void DependOnModule(Program program, ModuleDefinition module,
}
}

var import = CreateImport(module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName);
var publicModuleName = PublicModuleIdProtect(module.GetCompileName(Options));
var import = CreateImport(publicModuleName, module.IsDefaultModule, externModule, libraryName);
import.Path = goModuleName + import.Path;
AddImport(import);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,3 +23,10 @@ module {:options "--function-syntax:4"} CoolLibraryName {

}
}

// Ensuring reserved names in some languages are escaped consistently across languages
module Math {
function Add(x: int, y: int): int {
x + y
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -50,12 +50,16 @@ include "Inputs/producer/timesTwo.dfy"
module ConsumerModule {

import opened CoolLibraryName.LibraryModule
import Math

method Main() {
var n := 21;
var TwoN := TimesTwo(n);
print "Two times ", n, " is ", TwoN, "\n";

var z := Math.Add(20, 22);
print "20 plus 22 is ", z, "\n";

// Need to actually execute the use of nat's type descriptor
// to ensure it works on dynamic language targets.
var aNat := PickANat();
Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,8 @@
Two times 21 is 42
20 plus 22 is 42
Two times 21 is 42
20 plus 22 is 42
Two times 21 is 42
20 plus 22 is 42
Two times 21 is 42
20 plus 22 is 42

0 comments on commit b5f57e0

Please sign in to comment.