From 5f2330113320f2af0476473fd267b5b547f94cba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Tue, 12 Nov 2024 14:09:03 -0600 Subject: [PATCH] Fix 5724 compile suffix main arguments (#5910) Fixes #5724 ### Description - Support for `--compile-suffix` for emitting the main method name. - Support for main methods with arguments. - Support for test main methods with implicit formals ### How has this been tested? - Modified the existing `comp/rust/tests.dfy` test in a way that was reproducing the two issues mentioned in #5724 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). --- .../Backends/CSharp/CsharpCodeGenerator.cs | 2 +- .../Backends/Cplusplus/CppCodeGenerator.cs | 2 +- .../Backends/Dafny/DafnyCodeGenerator.cs | 4 +- .../Backends/DafnyExecutableBackend.cs | 8 +++- .../Backends/DafnyWrittenCodeGenerator.cs | 5 ++- .../Backends/GoLang/GoCodeGenerator.cs | 2 +- .../Backends/Java/JavaCodeGenerator.cs | 2 +- .../JavaScript/JavaScriptCodeGenerator.cs | 2 +- .../Backends/Python/PythonCodeGenerator.cs | 2 +- .../Dafny-compiler-fdafny.dfy | 2 +- ...edDesugaredExecutableDafnyCodeGenerator.cs | 9 ++-- .../Backends/Rust/Dafny-compiler-rust.dfy | 32 ++++++++----- .../Backends/Rust/RustCodeGenerator.cs | 26 ++++++++--- .../SinglePassCodeGenerator.cs | 4 +- Source/DafnyCore/GeneratedFromDafny/DCOMP.cs | 45 ++++++++++++++----- .../ResolvedDesugaredExecutableDafnyPlugin.cs | 2 +- .../DafnyRuntime/DafnyRuntimeRust/src/lib.rs | 4 +- .../LitTests/LitTest/comp/rust/tests.dfy | 19 +++++++- .../LitTest/comp/rust/tests.dfy.expect | 3 +- .../LitTest/comp/rust/tests.dfy.main.expect | 2 + 20 files changed, 125 insertions(+), 52 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy.main.expect diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 8f1af398528..e5bfab5c191 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -1776,7 +1776,7 @@ protected override string TypeName_UDT(string fullCompileName, List", s, ActualTypeArgs(typeArgs)); } - protected override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member) { + internal override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member) { // There are no companion classes for Cpp var t = TypeName(type, wr, tok, member, true); return t; diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index 45a3bda471a..5ad8399a099 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -468,7 +468,7 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name, private Sequence GenFormals(List formals) { List paramsList = new(); foreach (var param in formals) { - if (param is not ImplicitFormal && !param.IsGhost) { + if (!param.IsGhost) { paramsList.Add((DAST.Formal)DAST.Formal.create_Formal( Sequence.UnicodeFromString(IdProtect(param.CompileName)), GenType(param.Type), ParseAttributes(param.Attributes))); } @@ -821,7 +821,7 @@ protected override string TypeName_UDT(string fullCompileName, List st) { actualBuilder = st.Builder; diff --git a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs b/Source/DafnyCore/Backends/DafnyExecutableBackend.cs index 00efe28dca5..b070d47c59c 100644 --- a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs +++ b/Source/DafnyCore/Backends/DafnyExecutableBackend.cs @@ -64,7 +64,13 @@ public override void Compile(Program dafnyProgram, string dafnyProgramName, Conc } public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree output) { - var o = DafnyCodeGenerator.EmitCallToMain(mainMethod.FullSanitizedName); + var sourceBuf = new ExprBuffer(null); + var mainCallHolder = new BuilderSyntaxTree(sourceBuf, ((DafnyCodeGenerator)codeGenerator)); + ((DafnyCodeGenerator)codeGenerator).TypeName_Companion(UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(mainMethod.EnclosingClass), mainCallHolder, mainMethod.tok, mainMethod); + var companion = sourceBuf.Finish(); + var hasArguments = mainMethod.Ins.Any(); + var mainMethodName = (Sequence)Sequence.UnicodeFromString(mainMethod.Name); + var o = DafnyCodeGenerator.EmitCallToMain(companion, mainMethodName, hasArguments); output.Write(o.ToVerbatimString(false)); } diff --git a/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs b/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs index ba6d3b79dfe..458a9e3851c 100644 --- a/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs +++ b/Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs @@ -7,7 +7,10 @@ public abstract class DafnyWrittenCodeGenerator { public abstract void Compile(Sequence program, Sequence> otherFiles, ConcreteSyntaxTree w); - public abstract ISequence EmitCallToMain(string fullName); + public abstract ISequence EmitCallToMain( + DAST.Expression companion, + Sequence mainMethodName, + bool hasArguments); } diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index 5bd0e5fd8f9..d095d265459 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -1847,7 +1847,7 @@ protected string TypeName_Constructor(DatatypeCtor ctor, ConcreteSyntaxTree wr) return string.Format("{0}{1}_{2}", ptr, TypeName(UserDefinedType.FromTopLevelDecl(ctor.tok, ctor.EnclosingDatatype), wr, ctor.tok), ctor.GetCompileName(Options)); } - protected override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member) { + internal override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member) { type = UserDefinedType.UpcastToMemberEnclosingType(type, member); // XXX This duplicates some of the logic in UserDefinedTypeName, but if we // don't do it here, we end up passing the name of the module to diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index a55a85280a6..0186120f398 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -1532,7 +1532,7 @@ protected override void EmitConstructorCheck(string source, DatatypeCtor ctor, C wr.Write($"{source}.is_{ctor.GetCompileName(Options)}()"); } - protected override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member) { + internal override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member) { type = UserDefinedType.UpcastToMemberEnclosingType(type, member); if (type is UserDefinedType udt) { var name = udt.ResolvedClass is TraitDecl ? udt.GetFullCompanionCompileName(Options) : FullTypeName(udt, member, true); diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs index 57b208281dc..21e925acbb6 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs +++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs @@ -1064,7 +1064,7 @@ protected override string TypeName_UDT(string fullCompileName, List) returns (s: string) { + static method EmitCallToMain(fullName: Expression) returns (s: string) { s := ""; } } diff --git a/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs b/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs index 73dd85af21f..3524aa775e7 100644 --- a/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs @@ -12,9 +12,10 @@ public override void Compile(Sequence program, Sequence EmitCallToMain(string fullName) { - var splitByDot = fullName.Split('.'); - var convertedToUnicode = Sequence>.FromArray(splitByDot.Select(s => (Sequence)Sequence.UnicodeFromString(s)).ToArray()); - return COMP.EmitCallToMain(convertedToUnicode); + public override ISequence EmitCallToMain( + DAST.Expression companion, + Sequence mainMethodName, + bool hasArguments) { + return COMP.EmitCallToMain(companion); } } diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy index 1fc4232fece..633151d01cf 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy @@ -23,6 +23,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler { const thisFile: R.Path := if rootType.RootCrate? then R.crate else R.crate.MSel(rootType.moduleName) const DafnyChar := if charType.UTF32? then "DafnyChar" else "DafnyCharUTF16" + const conversions := if charType.UTF32? then "unicode_chars_true" else "unicode_chars_false" const DafnyCharUnderlying := if charType.UTF32? then R.RawType("char") else R.RawType("u16") const string_of := if charType.UTF32? then "string_of" else "string_utf16_of" const allocate := @@ -3772,21 +3773,30 @@ module {:extern "DCOMP"} DafnyToRustCompiler { } s := s + "\n"; s := s + m.ToString(""); - } } - static method EmitCallToMain(fullName: seq) returns (s: string) { - s := "\nfn main() {\n"; - var i := 0; - while i < |fullName| { - if i > 0 { - s := s + "::"; - } - s := s + escapeName(fullName[i]); - i := i + 1; + method EmitCallToMain(companion: Expression, mainMethodName: string, hasArgs: bool) returns (s: string) + modifies this + { + s := "\nfn main() {"; + if hasArgs { + s := s + @" + let args: Vec = ::std::env::args().collect(); + let dafny_args = + ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence( + &args, |s| + ::dafny_runtime::dafny_runtime_conversions::" + conversions + @"::string_to_dafny_string(s)); + "; + } + var call, _, _ := GenExpr(companion, NoSelf, Environment.Empty(), OwnershipOwned); + call := call.FSel(mainMethodName); + if hasArgs { + call := call.Apply1(R.Borrow(R.Identifier("dafny_args"))); + } else { + call := call.Apply([]); } - s := s + "();\n}"; + s := s + call.ToString("") + ";\n}"; } } } \ No newline at end of file diff --git a/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs b/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs index ea3e36828e3..8dc6839eb87 100644 --- a/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs @@ -15,7 +15,7 @@ public RustCodeGenerator(DafnyOptions options) { this.Options = options; } - public override void Compile(Sequence program, Sequence> otherFiles, ConcreteSyntaxTree w) { + private COMP CreateCompiler() { var c = new DCOMP.COMP(); var charType = Options.Get(CommonOptionBag.UnicodeCharacters) ? Defs.CharType.create_UTF32() @@ -24,9 +24,14 @@ public override void Compile(Sequence program, Sequence.UnicodeFromString(opt)) - : Defs.RootType.create_RootCrate(); + Defs.RootType.create_RootPath(Sequence.UnicodeFromString(opt)) + : Defs.RootType.create_RootCrate(); c.__ctor(charType, pointerType, rootType); + return c; + } + + public override void Compile(Sequence program, Sequence> otherFiles, ConcreteSyntaxTree w) { + var c = CreateCompiler(); var s = c.Compile(program, otherFiles); if (!Options.Get(CommonOptionBag.EmitUncompilableCode) && c.error.is_Some) { throw new UnsupportedInvalidOperationException(c.error.dtor_value.ToVerbatimString(false)); @@ -34,10 +39,17 @@ public override void Compile(Sequence program, Sequence EmitCallToMain(string fullName) { - var splitByDot = fullName.Split('.'); - var convertedToUnicode = Sequence>.FromArray(splitByDot.Select(s => (Sequence)Sequence.UnicodeFromString(s)).ToArray()); - return DCOMP.COMP.EmitCallToMain(convertedToUnicode); + public override ISequence EmitCallToMain( + DAST.Expression companion, + Sequence mainMethodName, + bool hasArguments) { + var c = CreateCompiler(); + var result = c.EmitCallToMain(companion, mainMethodName, hasArguments); + if (!Options.Get(CommonOptionBag.EmitUncompilableCode) && c.error.is_Some) { + throw new UnsupportedInvalidOperationException(c.error.dtor_value.ToVerbatimString(false)); + } + + return result; } } diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index a5bd26af4c8..b9a115b7c81 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -376,12 +376,12 @@ protected string TypeName_UDT(string fullCompileName, UserDefinedType udt, Concr } protected abstract string TypeName_UDT(string fullCompileName, List variance, List typeArgs, ConcreteSyntaxTree wr, IToken tok, bool omitTypeArguments); - protected abstract string/*?*/ TypeName_Companion(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member); + abstract internal string/*?*/ TypeName_Companion(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member); protected virtual void EmitTypeName_Companion(Type type, ConcreteSyntaxTree wr, ConcreteSyntaxTree surrounding, IToken tok, MemberDecl/*?*/ member) { wr.Write(TypeName_Companion(type, surrounding, tok, member)); } - protected string TypeName_Companion(TopLevelDecl cls, ConcreteSyntaxTree wr, IToken tok) { + internal string TypeName_Companion(TopLevelDecl cls, ConcreteSyntaxTree wr, IToken tok) { Contract.Requires(cls != null); Contract.Requires(wr != null); Contract.Requires(tok != null); diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index 4482140deb5..49f3c4219ce 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -6717,20 +6717,36 @@ public RAST._IExpr Error(Dafny.ISequence message, RAST._IExpr defaul after_0: ; return s; } - public static Dafny.ISequence EmitCallToMain(Dafny.ISequence> fullName) + public Dafny.ISequence EmitCallToMain(DAST._IExpression companion, Dafny.ISequence mainMethodName, bool hasArgs) { Dafny.ISequence s = Dafny.Sequence.Empty; - s = Dafny.Sequence.UnicodeFromString("\nfn main() {\n"); - BigInteger _0_i; - _0_i = BigInteger.Zero; - while ((_0_i) < (new BigInteger((fullName).Count))) { - if ((_0_i).Sign == 1) { - s = Dafny.Sequence.Concat(s, Dafny.Sequence.UnicodeFromString("::")); - } - s = Dafny.Sequence.Concat(s, Defs.__default.escapeName((fullName).Select(_0_i))); - _0_i = (_0_i) + (BigInteger.One); + s = Dafny.Sequence.UnicodeFromString("\nfn main() {"); + if (hasArgs) { + s = Dafny.Sequence.Concat(Dafny.Sequence.Concat(Dafny.Sequence.Concat(s, Dafny.Sequence.UnicodeFromString(@" + let args: Vec = ::std::env::args().collect(); + let dafny_args = + ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence( + &args, |s| + ::dafny_runtime::dafny_runtime_conversions::")), (this).conversions), Dafny.Sequence.UnicodeFromString(@"::string_to_dafny_string(s)); + ")); + } + RAST._IExpr _0_call; + Defs._IOwnership _1___v181; + Dafny.ISet> _2___v182; + RAST._IExpr _out0; + Defs._IOwnership _out1; + Dafny.ISet> _out2; + (this).GenExpr(companion, Defs.SelfInfo.create_NoSelf(), Defs.Environment.Empty(), Defs.Ownership.create_OwnershipOwned(), out _out0, out _out1, out _out2); + _0_call = _out0; + _1___v181 = _out1; + _2___v182 = _out2; + _0_call = (_0_call).FSel(mainMethodName); + if (hasArgs) { + _0_call = (_0_call).Apply1(RAST.__default.Borrow(RAST.Expr.create_Identifier(Dafny.Sequence.UnicodeFromString("dafny_args")))); + } else { + _0_call = (_0_call).Apply(Dafny.Sequence.FromElements()); } - s = Dafny.Sequence.Concat(s, Dafny.Sequence.UnicodeFromString("();\n}")); + s = Dafny.Sequence.Concat(Dafny.Sequence.Concat(s, (_0_call)._ToString(Dafny.Sequence.UnicodeFromString(""))), Dafny.Sequence.UnicodeFromString(";\n}")); return s; } public Defs._IRootType _rootType {get; set;} @@ -6755,6 +6771,13 @@ public Dafny.ISequence DafnyChar { get { return Dafny.Sequence.UnicodeFromString("DafnyCharUTF16"); } } } + public Dafny.ISequence conversions { get { + if (((this).charType).is_UTF32) { + return Dafny.Sequence.UnicodeFromString("unicode_chars_true"); + } else { + return Dafny.Sequence.UnicodeFromString("unicode_chars_false"); + } + } } public RAST._IType DafnyCharUnderlying { get { if (((this).charType).is_UTF32) { return RAST.__default.RawType(Dafny.Sequence.UnicodeFromString("char")); diff --git a/Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs b/Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs index b62b79525a8..b545bb2a8e1 100644 --- a/Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs +++ b/Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs @@ -26,7 +26,7 @@ public COMP() { s = _out0; return s; } - public static Dafny.ISequence EmitCallToMain(Dafny.ISequence> fullName) + public static Dafny.ISequence EmitCallToMain(DAST._IExpression fullName) { Dafny.ISequence s = Dafny.Sequence.Empty; s = Dafny.Sequence.UnicodeFromString(""); diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs index 38144c2d35e..dc2e4082403 100644 --- a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs +++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs @@ -200,7 +200,7 @@ pub mod dafny_runtime_conversions { DafnyMap::::from_hashmap(map, converter_k, converter_v) } - // --unicode-chars:true + // --unicode-char:true pub mod unicode_chars_true { use crate::Sequence; @@ -216,7 +216,7 @@ pub mod dafny_runtime_conversions { } } - // --unicode-chars:false + // --unicode-char:false pub mod unicode_chars_false { use crate::Sequence; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy index 1b83a453b58..e431975b417 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy @@ -1,7 +1,22 @@ -// NONUNIFORM: Demonstration of the use of the external Rust Option<> type +// NONUNIFORM: Test of the Dafny-to-Rust tests // RUN: %baredafny test --target=rs "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %diff "%s.expect" "%t +// RUN: %baredafny build --compile-suffix --target=rs "%s" > "%t" +// RUN: "%S/tests-rust/cargo" run -- Hello > "%t" +// RUN: %diff "%s.main.expect" "%t" method {:test} TestIfTestsAreWorking() { expect 1 == 1, "Ok"; +} + +module WrappedTests { + method {:test} TestIfTestsAreWorking() { + expect 1 == 1, "Ok"; + } + method Main(args: seq) { + print "Detected main\n"; + if |args| > 1 { + print args[1]; + } + } } \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy.expect index f5269b4546c..7115860dfa1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy.expect @@ -1,3 +1,4 @@ -Dafny program verifier finished with 0 verified, 0 errors +Dafny program verifier finished with 1 verified, 0 errors +WrappedTests.TestIfTestsAreWorking: PASSED TestIfTestsAreWorking: PASSED diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy.main.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy.main.expect new file mode 100644 index 00000000000..27a68b1bd3c --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/tests.dfy.main.expect @@ -0,0 +1,2 @@ +Detected main +Hello \ No newline at end of file