fix: Uniform backend testing

.github/workflows/msbuild.yml

@@ -58,6 +58,8 @@ jobs:
  run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs
  - name: Create NuGet package (just to make sure it works)
  run: dotnet pack --no-build dafny/Source/Dafny.sln
+ - name: Check uniformity of integration tests that exercise backends
+ run: DAFNY_INTEGRATION_TESTS_MODE=uniformity-check dotnet test dafny/Source/IntegrationTests
 
  xunit-tests:
  needs: check-deep-tests

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -339,7 +339,7 @@ public void PrintTopLevelDecls(Program program, IEnumerable<TopLevelDecl> decls,
  wr.WriteLine();
  }
 
- if (options.DafnyPrintResolvedFile != null) {
+ if (afterResolver) {
  // also print the members that were created as part of the interpretation of the iterator
  Contract.Assert(iter.Members.Count != 0); // filled in during resolution
  Indent(indent); wr.WriteLine("/*---------- iterator members ----------");

Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs

@@ -228,7 +228,7 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
  throw new UnsupportedFeatureException(tok, Feature.ExternalClasses, String.Format("extern in class {0}", name));
  }
  if (superClasses != null && superClasses.Any(trait => !trait.IsObject)) {
- throw new UnsupportedFeatureException(tok, Feature.Traits, String.Format("traits in class {0}", name));
+ throw new UnsupportedFeatureException(tok, Feature.Traits);
  }
 
  var classDeclWriter = modDeclWr;
@@ -270,7 +270,7 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
 
  protected override IClassWriter CreateTrait(string name, bool isExtern, List<TypeParameter> typeParameters /*?*/,
  TopLevelDecl trait, List<Type> superClasses /*?*/, IToken tok, ConcreteSyntaxTree wr) {
- throw new UnsupportedFeatureException(tok, Feature.Traits, String.Format("traits in class {0}", name));
+ throw new UnsupportedFeatureException(tok, Feature.Traits);
  }
 
  protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, ConcreteSyntaxTree wr) {
@@ -610,7 +610,7 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre
  wr.WriteLine("typedef {0} {1};", nt_name_def, nt.Name);
  }
  } else {
- throw new UnsupportedFeatureException(nt.tok, Feature.NonNativeNewtypes, String.Format("non-native newtype {0}", nt));
+ throw new UnsupportedFeatureException(nt.tok, Feature.NonNativeNewtypes);
  }
  var className = "class_" + IdName(nt);
  var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), className, nt, wr) as ClassWriter;
@@ -2168,8 +2168,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
  if (resultType.IsCharType || AsNativeType(resultType) != null) {
  opString = "-";
  } else {
- throw new UnsupportedFeatureException(tok, Feature.NonNativeNewtypes,
- "Subtraction of non-native type");
+ throw new UnsupportedFeatureException(tok, Feature.NonNativeNewtypes);
  }
  break;
  case BinaryExpr.ResolvedOpcode.Mul:
@@ -2179,8 +2178,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
  if (AsNativeType(resultType) != null) {
  opString = "*";
  } else {
- throw new UnsupportedFeatureException(tok, Feature.NonNativeNewtypes,
- "Multiplication of non-native type");
+ throw new UnsupportedFeatureException(tok, Feature.NonNativeNewtypes);
  }
  break;
  case BinaryExpr.ResolvedOpcode.Div:

Source/DafnyCore/Compilers/Java/JavaBackend.cs

@@ -97,7 +97,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
  if (Options.SpillTargetCode == 0) {
  Directory.Delete(targetDirectory, true);
  } else {
- classFiles.ForEach(f => File.Delete(f));
+ classFiles.ForEach(f => File.Delete(Path.Join(targetDirectory, f)));
  }
  }