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.

Sign up for GitHub

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

Feat: Translate Dafny tests to Rust tests #5676

Merged
merged 18 commits into from
Sep 12, 2024
Merged

Feat: Translate Dafny tests to Rust tests #5676

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
7f9f755
Feat: Translate Dafny tests to Rust tests
MikaelMayer Aug 8, 2024
2313986
Ran make pr
MikaelMayer Aug 8, 2024
a7b0708
Setting working directory only for cargo command
MikaelMayer Aug 8, 2024
83280dd
Resolved merge conflicts
MikaelMayer Aug 8, 2024
cb0f4e0
Merge branch 'master' into feat-5666-cargo-test
MikaelMayer Sep 4, 2024
2f23e61
Ensure determinism in test file
MikaelMayer Sep 4, 2024
9a07648
Merge branch 'feat-5666-cargo-test' of https://github.com/dafny-lang/…
MikaelMayer Sep 4, 2024
e82e76c
Merge branch 'master' into feat-5666-cargo-test
MikaelMayer Sep 4, 2024
9885d64
Merge branch 'master' into feat-5666-cargo-test
MikaelMayer Sep 6, 2024
7553c55
Merge branch 'master' into feat-5666-cargo-test
MikaelMayer Sep 6, 2024
cc1984f
Update 5666.feat
MikaelMayer Sep 12, 2024
6732b79
Merge branch 'master' into feat-5666-cargo-test
MikaelMayer Sep 12, 2024
5b8836f
Renamed test option
MikaelMayer Sep 12, 2024
b4d7344
Merge branch 'feat-5666-cargo-test' of https://github.com/dafny-lang/…
MikaelMayer Sep 12, 2024
ecfb6e4
Updated release notes
MikaelMayer Sep 12, 2024
d2d082c
Update docs/DafnyRef/integration- rust/IntegrationRust.md
MikaelMayer Sep 12, 2024
f3b20d2
Update and rename 5666.feat to 5676.feat
MikaelMayer Sep 12, 2024
32f7db6
Updated the test annotation
MikaelMayer Sep 12, 2024
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
4 changes: 2 additions & 2 deletions Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,8 +40,8 @@ public static void TestApply()
_3_std__any__Any = (((RAST.__default.@global).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("std"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("any"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"));
RAST._IType _4_Any;
_4_Any = RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"));
FactorPathsOptimizationTest.__default.ShouldBeEqual(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
FactorPathsOptimizationTest.__default.ShouldBeEqual(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
FactorPathsOptimizationTest.__default.ShouldBeEqual(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
FactorPathsOptimizationTest.__default.ShouldBeEqual(FactorPathsOptimization.__default.apply(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
}
}
} // end of namespace FactorPathsOptimizationTest
4 changes: 2 additions & 2 deletions Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,7 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
wr.WriteLine("#if ISDAFNYRUNTIMELIB");
}

var dafnyNamespace = CreateModule("Dafny", false, null, null, wr);
var dafnyNamespace = CreateModule("Dafny", false, null, null, null, wr);
EmitInitNewArrays(systemModuleManager, dafnyNamespace);
if (Synthesize) {
CsharpSynthesizer.EmitMultiMatcher(dafnyNamespace);
Expand Down Expand Up @@ -269,7 +269,7 @@ string IdProtectModule(string moduleName) {
}

protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
string libraryName /*?*/, ConcreteSyntaxTree wr) {
string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
moduleName = IdProtectModule(moduleName);
return wr.NewBlock($"namespace {moduleName}", " // end of " + $"namespace {moduleName}");
}
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -160,7 +160,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
}

protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
string libraryName /*?*/, ConcreteSyntaxTree wr) {
string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
var s = $"namespace {IdProtect(moduleName)} ";
string footer = "// end of " + s + " declarations";
this.modDeclWr = this.modDeclsWr.NewBlock(s, footer);
Expand Down
1 change: 1 addition & 0 deletions Source/DafnyCore/Backends/Dafny/AST.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -204,6 +204,7 @@ module {:extern "DAST"} DAST {
datatype Formal = Formal(name: VarName, typ: Type, attributes: seq<Attribute>)

datatype Method = Method(
attributes: seq<Attribute>,
isStatic: bool,
hasBody: bool,
outVarsAreUninitFieldsToAssign: bool, // For constructors
Expand Down
15 changes: 9 additions & 6 deletions Source/DafnyCore/Backends/Dafny/ASTBuilder.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -365,15 +365,14 @@ interface ClassLike {

void AddField(DAST.Formal item, _IOption<DAST._IExpression> defaultValue);

public MethodBuilder Method(
bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction,
public MethodBuilder Method(bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction,
ISequence<ISequence<Rune>> overridingPath,
ISequence<_IAttribute> attributes,
string name,
List<DAST.TypeArgDecl> typeArgs,
List<TypeArgDecl> typeArgs,
Sequence<DAST.Formal> params_,
List<DAST.Type> outTypes, List<ISequence<Rune>> outVars
) {
return new MethodBuilder(this, isStatic, hasBody, outVarsAreUninitFieldsToAssign, wasFunction, overridingPath, name, typeArgs, params_, outTypes, outVars);
List<DAST.Type> outTypes, List<ISequence<Rune>> outVars) {
return new MethodBuilder(this, isStatic, hasBody, outVarsAreUninitFieldsToAssign, wasFunction, overridingPath, attributes, name, typeArgs, params_, outTypes, outVars);
}

public object Finish();
Expand All @@ -392,11 +391,13 @@ class MethodBuilder : StatementContainer {
readonly List<DAST.Type> outTypes;
readonly List<ISequence<Rune>> outVars;
readonly List<object> body = new();
private ISequence<_IAttribute> attributes;

public MethodBuilder(
ClassLike parent,
bool isStatic, bool hasBody, bool outVarsAreUninitFieldsToAssign, bool wasFunction,
ISequence<ISequence<Rune>> overridingPath,
ISequence<_IAttribute> attributes,
string name,
List<DAST.TypeArgDecl> typeArgs,
Sequence<DAST.Formal> params_,
Expand All @@ -408,6 +409,7 @@ public MethodBuilder(
this.outVarsAreUninitFieldsToAssign = outVarsAreUninitFieldsToAssign;
this.wasFunction = wasFunction;
this.overridingPath = overridingPath;
this.attributes = attributes;
this.name = name;
this.typeArgs = typeArgs;
this.params_ = params_;
Expand All @@ -434,6 +436,7 @@ public DAST.Method Build() {
StatementContainer.RecursivelyBuild(body, builtStatements);

return (DAST.Method)DAST.Method.create(
attributes,
isStatic,
hasBody,
outVarsAreUninitFieldsToAssign,
Expand Down
13 changes: 10 additions & 3 deletions Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,9 +125,9 @@ private bool NeedsExternalImport(MemberDecl memberDecl) {
}

protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
string libraryName, ConcreteSyntaxTree wr) {
string libraryName, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
if (currentBuilder is ModuleContainer moduleBuilder) {
var attributes = (Sequence<DAST.Attribute>)Sequence<DAST.Attribute>.Empty;
var attributes = (Sequence<DAST.Attribute>)ParseAttributes(moduleAttributes);
if (externModule != null) {
attributes = (Sequence<DAST.Attribute>)ParseAttributes(externModule.Attributes);
}
Expand Down Expand Up @@ -551,9 +551,12 @@ public ConcreteSyntaxTree CreateMethod(Method m, List<TypeArgumentInstantiation>
GenType(md.GetType())
).ToList();*/
}

var attributes = compiler.ParseAttributes(m.Attributes);
var builder = this.builder.Method(
m.IsStatic, createBody, m is Constructor, false,
overridingTrait != null ? compiler.PathFromTopLevel(overridingTrait) : null,
attributes,
m.GetCompileName(compiler.Options),
astTypeArgs, params_,
outTypes, outVars
Expand Down Expand Up @@ -586,10 +589,11 @@ public ConcreteSyntaxTree CreateFunction(string name, List<TypeArgumentInstantia
var params_ = compiler.GenFormals(formals);

var overridingTrait = member.OverriddenMember?.EnclosingClass;

var attributes = compiler.ParseAttributes(member.Attributes);
var builder = this.builder.Method(
isStatic, createBody, false, true,
overridingTrait != null ? compiler.PathFromTopLevel(overridingTrait) : null,
attributes,
name,
astTypeArgs, params_,
new() {
Expand All @@ -614,9 +618,12 @@ public ConcreteSyntaxTree CreateGetter(string name, TopLevelDecl enclosingDecl,

var overridingTrait = member.OverriddenMember?.EnclosingClass;

var attributes = compiler.ParseAttributes(enclosingDecl.Attributes);

var builder = this.builder.Method(
isStatic, createBody, false, true,
overridingTrait != null ? compiler.PathFromTopLevel(overridingTrait) : null,
attributes,
name,
new(), (Sequence<DAST.Formal>)Sequence<DAST.Formal>.Empty,
new() {
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,7 @@ private Import CreateImport(string moduleName, bool isDefault, ModuleDefinition

protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault,
ModuleDefinition externModule,
string libraryName /*?*/, ConcreteSyntaxTree wr) {
string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
if (isDefault) {
// Fold the default module into the main module
return wr;
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -380,7 +380,7 @@ string IdProtectModule(string moduleName) {
}

protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
string libraryName /*?*/, ConcreteSyntaxTree wr) {
string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
moduleName = IdProtectModule(moduleName);
if (isDefault) {
// Fold the default module into the main module
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
}

protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
string libraryName /*?*/, ConcreteSyntaxTree wr) {
string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
moduleName = IdProtect(moduleName);
if (externModule == null || libraryName != null) {
wr.Write("let {0} = ", moduleName);
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
}

protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
string libraryName, ConcreteSyntaxTree wr) {
string libraryName, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
var pythonModuleName = PythonModuleMode ? PythonModuleName + "." : "";

moduleName = PublicModuleIdProtect(moduleName);
Expand Down
Loading