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

fix!: Disable automatically mapping a Dafny string to a Go string in externs #3647

Merged
merged 12 commits into from
Feb 28, 2023
Merged
Next Next commit
Added test, remove dead code (seems to be already fixed?)
  • Loading branch information
robin-aws committed Feb 24, 2023
commit 78ae250cc64a6aa3ab19641ef05c9342510a2b99
19 changes: 1 addition & 18 deletions Source/DafnyCore/Compilers/GoLang/Compiler-go.cs
Original file line number Diff line number Diff line change
Expand Up @@ -1402,9 +1402,7 @@ protected class ClassWriter : IClassWriter {
Contract.Assume(type != null); // precondition; this ought to be declared as a Requires in the superclass

var xType = DatatypeWrapperEraser.SimplifyType(type);
if (xType is SpecialNativeType snt) {
return snt.Name;
} else if (xType is BoolType) {
if (xType is BoolType) {
return "bool";
} else if (xType is CharType) {
return CharTypeName;
Expand Down Expand Up @@ -1675,21 +1673,6 @@ protected class ClassWriter : IClassWriter {
return Capitalize(formal.CompileName);
}

protected override Type NativeForm(Type type) {
if (type.IsStringType) {
return NativeStringType;
} else {
return type;
}
}

/// A type which is rendered to Go exactly as specified. Used to represent the native string type.
private class SpecialNativeType : UserDefinedType {
internal SpecialNativeType(string name) : base(Token.NoToken, name, null) { }
}

private readonly static SpecialNativeType NativeStringType = new SpecialNativeType("string");

// ----- Declarations -------------------------------------------------------------

protected void DeclareField(string name, bool isExtern, bool isStatic, bool isConst, Type type, IToken tok, string/*?*/ rhs, string className, ConcreteSyntaxTree wr, ConcreteSyntaxTree initWriter, ConcreteSyntaxTree concreteMethodWriter) {
Expand Down
13 changes: 13 additions & 0 deletions Test/git-issues/github-issue-2989.dfy
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
// RUN: %translate go --unicode-char:false "%s" > "%t"
// RUN: %translate go --unicode-char:true "%s" >> "%t"
// RUN: %diff "%s.expect" "%t"

method Main() {
var s := Foo();
}

method {:extern "foo"} Foo() returns (s: string)

method Bar() returns (s: string) {
return "hello";
}
Empty file.