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 <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>
dafny-lang · Nov 12, 2024 · 5f23301 · 5f23301
1 parent e7a9db1
commit 5f23301
Show file tree

Hide file tree

Showing 20 changed files with 125 additions and 52 deletions.
diff --git 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<TypeParamete
       return s;
     }
 
-    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/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
@@ -1117,7 +1117,7 @@ protected override string TypeName_UDT(string fullCompileName, List<TypeParamete
       return String.Format("std::shared_ptr<{0}{1}>", 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
@@ -468,7 +468,7 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name,
     private Sequence<DAST.Formal> GenFormals(List<Formal> formals) {
       List<DAST.Formal> 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<Rune>.UnicodeFromString(IdProtect(param.CompileName)), GenType(param.Type), ParseAttributes(param.Attributes)));
         }
@@ -821,7 +821,7 @@ protected override string TypeName_UDT(string fullCompileName, List<TypeParamete
       return fullCompileName;
     }
 
-    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) {
       ExprContainer actualBuilder;
       if (wr is BuilderSyntaxTree<ExprContainer> st) {
         actualBuilder = st.Builder;

diff --git 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<ExprContainer>(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<Rune>)Sequence<Rune>.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
@@ -7,7 +7,10 @@ public abstract class DafnyWrittenCodeGenerator {
 
     public abstract void Compile(Sequence<DAST.Module> program, Sequence<ISequence<Rune>> otherFiles, ConcreteSyntaxTree w);
 
-    public abstract ISequence<Rune> EmitCallToMain(string fullName);
+    public abstract ISequence<Rune> EmitCallToMain(
+      DAST.Expression companion,
+      Sequence<Rune> mainMethodName,
+      bool hasArguments);
 
   }
 

diff --git 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
@@ -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
@@ -1064,7 +1064,7 @@ protected override string TypeName_UDT(string fullCompileName, List<TypeParamete
       return s;
     }
 
-    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) {
       // Many (that is, more so than in C# or Java) companion classes in JavaScript are just the same as the type
       type = UserDefinedType.UpcastToMemberEnclosingType(type, member);
       if (type.NormalizeExpandKeepConstraints() is UserDefinedType udt) {

diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
@@ -897,7 +897,7 @@ protected override string TypeName_UDT(string fullCompileName, List<TypeParamete
       return fullCompileName;
     }
 
-    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.NormalizeExpandKeepConstraints() is UserDefinedType udt) {

diff --git a/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/Dafny-compiler-fdafny.dfy b/Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/Dafny-compiler-fdafny.dfy
@@ -9,7 +9,7 @@ module {:extern "ResolvedDesugaredExecutableDafnyPlugin"} ResolvedDesugaredExecu
       s := PrettyPrinter.PrettyPrint(p);
     }
 
-    static method EmitCallToMain(fullName: seq<string>) returns (s: string) {
+    static method EmitCallToMain(fullName: Expression) returns (s: string) {
       s := "";
     }
   }

diff --git a/...ackends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs b/...ackends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs
@@ -12,9 +12,10 @@ public override void Compile(Sequence<DAST.Module> program, Sequence<ISequence<R
     w.Write(COMP.Compile(program).ToVerbatimString(false));
   }
 
-  public override ISequence<Rune> EmitCallToMain(string fullName) {
-    var splitByDot = fullName.Split('.');
-    var convertedToUnicode = Sequence<Sequence<Rune>>.FromArray(splitByDot.Select(s => (Sequence<Rune>)Sequence<Rune>.UnicodeFromString(s)).ToArray());
-    return COMP.EmitCallToMain(convertedToUnicode);
+  public override ISequence<Rune> EmitCallToMain(
+    DAST.Expression companion,
+    Sequence<Rune> 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
@@ -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<Name>) 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<String> = ::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}";
     }
   }
 }
diff --git 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<DAST.Module> program, Sequence<ISequence<Rune>> otherFiles, ConcreteSyntaxTree w) {
+    private COMP CreateCompiler() {
       var c = new DCOMP.COMP();
       var charType = Options.Get(CommonOptionBag.UnicodeCharacters)
         ? Defs.CharType.create_UTF32()
@@ -24,20 +24,32 @@ public override void Compile(Sequence<DAST.Module> program, Sequence<ISequence<R
         ? Defs.PointerType.create_Raw()
         : Defs.PointerType.create_RcMut();
       var rootType = Options.Get(RustBackend.RustModuleNameOption) is { } opt && opt != "" ?
-          Defs.RootType.create_RootPath(Sequence<Rune>.UnicodeFromString(opt))
-          : Defs.RootType.create_RootCrate();
+        Defs.RootType.create_RootPath(Sequence<Rune>.UnicodeFromString(opt))
+        : Defs.RootType.create_RootCrate();
       c.__ctor(charType, pointerType, rootType);
+      return c;
+    }
+
+    public override void Compile(Sequence<DAST.Module> program, Sequence<ISequence<Rune>> 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));
       }
       w.Write(s.ToVerbatimString(false));
     }
 
-    public override ISequence<Rune> EmitCallToMain(string fullName) {
-      var splitByDot = fullName.Split('.');
-      var convertedToUnicode = Sequence<Sequence<Rune>>.FromArray(splitByDot.Select(s => (Sequence<Rune>)Sequence<Rune>.UnicodeFromString(s)).ToArray());
-      return DCOMP.COMP.EmitCallToMain(convertedToUnicode);
+    public override ISequence<Rune> EmitCallToMain(
+      DAST.Expression companion,
+      Sequence<Rune> 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
@@ -376,12 +376,12 @@ protected string TypeName_UDT(string fullCompileName, UserDefinedType udt, Concr
     }
     protected abstract string TypeName_UDT(string fullCompileName, List<TypeParameter.TPVariance> variance, List<Type> 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
@@ -6717,20 +6717,36 @@ public RAST._IExpr Error(Dafny.ISequence<Dafny.Rune> message, RAST._IExpr defaul
     after_0: ;
       return s;
     }
-    public static Dafny.ISequence<Dafny.Rune> EmitCallToMain(Dafny.ISequence<Dafny.ISequence<Dafny.Rune>> fullName)
+    public Dafny.ISequence<Dafny.Rune> EmitCallToMain(DAST._IExpression companion, Dafny.ISequence<Dafny.Rune> mainMethodName, bool hasArgs)
     {
       Dafny.ISequence<Dafny.Rune> s = Dafny.Sequence<Dafny.Rune>.Empty;
-      s = Dafny.Sequence<Dafny.Rune>.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<Dafny.Rune>.Concat(s, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("::"));
-        }
-        s = Dafny.Sequence<Dafny.Rune>.Concat(s, Defs.__default.escapeName((fullName).Select(_0_i)));
-        _0_i = (_0_i) + (BigInteger.One);
+      s = Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\nfn main() {");
+      if (hasArgs) {
+        s = Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(s, Dafny.Sequence<Dafny.Rune>.UnicodeFromString(@"
+  let args: Vec<String> = ::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<Dafny.Rune>.UnicodeFromString(@"::string_to_dafny_string(s));
+  "));
+      }
+      RAST._IExpr _0_call;
+      Defs._IOwnership _1___v181;
+      Dafny.ISet<Dafny.ISequence<Dafny.Rune>> _2___v182;
+      RAST._IExpr _out0;
+      Defs._IOwnership _out1;
+      Dafny.ISet<Dafny.ISequence<Dafny.Rune>> _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<Dafny.Rune>.UnicodeFromString("dafny_args"))));
+      } else {
+        _0_call = (_0_call).Apply(Dafny.Sequence<RAST._IExpr>.FromElements());
       }
-      s = Dafny.Sequence<Dafny.Rune>.Concat(s, Dafny.Sequence<Dafny.Rune>.UnicodeFromString("();\n}"));
+      s = Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(s, (_0_call)._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(";\n}"));
       return s;
     }
     public Defs._IRootType _rootType {get; set;}
@@ -6755,6 +6771,13 @@ public Dafny.ISequence<Dafny.Rune> DafnyChar { get {
         return Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyCharUTF16");
       }
     } }
+    public Dafny.ISequence<Dafny.Rune> conversions { get {
+      if (((this).charType).is_UTF32) {
+        return Dafny.Sequence<Dafny.Rune>.UnicodeFromString("unicode_chars_true");
+      } else {
+        return Dafny.Sequence<Dafny.Rune>.UnicodeFromString("unicode_chars_false");
+      }
+    } }
     public RAST._IType DafnyCharUnderlying { get {
       if (((this).charType).is_UTF32) {
         return RAST.__default.RawType(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("char"));

diff --git 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<Dafny.Rune> EmitCallToMain(Dafny.ISequence<Dafny.ISequence<Dafny.Rune>> fullName)
+    public static Dafny.ISequence<Dafny.Rune> EmitCallToMain(DAST._IExpression fullName)
     {
       Dafny.ISequence<Dafny.Rune> s = Dafny.Sequence<Dafny.Rune>.Empty;
       s = Dafny.Sequence<Dafny.Rune>.UnicodeFromString("");

diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
@@ -200,7 +200,7 @@ pub mod dafny_runtime_conversions {
         DafnyMap::<K, V>::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
@@ -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<string>) {
+    print "Detected main\n";
+    if |args| > 1 {
+      print args[1];
+    }
+  }
 }
diff --git 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
@@ -0,0 +1,2 @@
+Detected main
+Hello