diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index d13f74b816a..7ee7455d38b 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -2236,8 +2236,11 @@ protected override void EmitNew(Type type, IToken tok, CallStmt initCall /*?*/, if (cl is TraitDecl { IsObjectTrait: true }) { wr.Write("_dafny.New_Object()"); } else { + var ctor = (Constructor)initCall?.Method; // correctness of cast follows from precondition of "EmitNew" + var sep = ""; wr.Write("{0}(", TypeName_Initializer(type, wr, tok)); EmitTypeDescriptorsActuals(TypeArgumentInstantiation.ListFromClass(cl, type.TypeArgs), tok, wr); + wr.Write(ConstructorArguments(initCall, wStmts, ctor, sep)); wr.Write(")"); } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Class.java b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Class.java index 1827be2bfc6..f6549c6aaf0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Class.java +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Class.java @@ -2,7 +2,7 @@ import java.math.BigInteger; -public class Class extends _ExternBase_Class { +public class Class { private final BigInteger n; public Class(BigInteger n) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.go b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.go index 93aaf858db5..2bcbd00321c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.go +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.go @@ -17,12 +17,6 @@ func (obj *Class) Get() dafny.Int { return obj.n } -// have to implement this because the Go backend can't mix Dafny and Go code :-\ - -func (obj *Class) Print() { - fmt.Printf("My value is %d\n", obj.n) -} - type CompanionStruct_Class_ struct{} var Companion_Class_ = CompanionStruct_Class_{} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.py index 3aa02f16f22..219b6d1836c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.py +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors-externs/Library.py @@ -17,8 +17,3 @@ def SayHi(): def Get(self): return self.n - - def Print(self): - _dafny.print(_dafny.string_of(_dafny.Seq("My value is "))) - _dafny.print(_dafny.string_of((self).Get())) - _dafny.print(_dafny.string_of(_dafny.Seq("\n"))) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy index d0d50d7383d..e3cacf6ee6a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy @@ -1,15 +1,16 @@ // RUN: %run --target cs "%s" --input %S/ExternCtors-externs/Library.cs > "%t" // RUN: %run --target java "%s" --input %S/ExternCtors-externs/Class.java >> "%t" // RUN: %run --target py "%s" --input %S/ExternCtors-externs/Library.py >> "%t" +// RUN: %run --target go "%s" --input %S/ExternCtors-externs/Library.go >> "%t" // RUN: %diff "%s.expect" "%t" -// FIXME: Extern constructors are currently broken in Go and JavaScript, -// so they are omitted +// FIXME: Extern constructors are currently broken in JavaScript, +// so that is omitted method Main() { Library.Class.SayHi(); var obj := new Library.Class(42); - obj.Print(); + print "My value is ", obj.Get(), "\n"; } module {:extern "Library"} Library { @@ -17,8 +18,6 @@ module {:extern "Library"} Library { constructor {:extern} (n: int) static method {:extern} SayHi() function {:extern} Get() : int - method Print() { - print "My value is ", Get(), "\n"; - } } } + diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy.expect index ce258f458fa..ef9433efad1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy.expect @@ -10,3 +10,7 @@ My value is 42 Dafny program verifier finished with 1 verified, 0 errors Hello! My value is 42 + +Dafny program verifier finished with 1 verified, 0 errors +Hello! +My value is 42