Skip to content

Commit

Permalink
Golang: Skip ghost parameters in type parameter downcast (#5815)
Browse files Browse the repository at this point in the history
### Description
Fixes #5814

### How has this been tested?
github-issue-5814.dfy

<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: Stefan Zetzsche <[email protected]>
  • Loading branch information
robin-aws and stefan-aws authored Oct 11, 2024
1 parent 8f8f585 commit c4dd8e5
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 1 deletion.
2 changes: 1 addition & 1 deletion Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -1367,7 +1367,7 @@ private ConcreteSyntaxTree CreateSubroutine(string name, List<TypeArgumentInstan
for (var i = 0; i < inParams.Count; i++) {
var p = (overriddenInParams ?? inParams)[i];
var instantiatedType = p.Type.Subst(thisContext.ParentFormalTypeParametersToActuals);
if (!instantiatedType.Equals(p.Type)) {
if (!p.IsGhost && !instantiatedType.Equals(p.Type)) {
// var p instantiatedType = p.(instantiatedType)
var pName = IdName(inParams[i]);
DeclareLocalVar(pName, instantiatedType, p.tok, true, null, w);
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// RUN: %testDafnyForEachCompiler "%s"

trait MyTrait<T> {
method Bar(ghost x: T, y: T) returns (z: T)
}

class MyClass extends MyTrait<int> {
constructor() {}
method Bar(ghost x: int, y: int) returns (z: int) {
return y;
}
}

method Main() {
var c := new MyClass();
var z := c.Bar(7, 42);
expect z == 42;
}
Empty file.

0 comments on commit c4dd8e5

Please sign in to comment.