From 5c8806f7c7c8a703b6f0d85fe26bd2a6e85a91e1 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 3 Apr 2024 18:03:47 +0200 Subject: [PATCH] Migrate almost all CLI tests to use the command based CLI (#5255) ### Description - Migrate almost all CLI tests to use the command based CLI - Tests that use options that are only available in the old CLI have not been migrated ### How has this been tested? - The tests themselves have changed 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/Dafny/BuilderSyntaxTree.cs | 2 +- .../Backends/Dafny/DafnyCodeGenerator.cs | 88 +++++++++--------- Source/IntegrationTests/LitTests.cs | 15 +++- .../TestFiles/LitTests/LitTest/c++/extern.dfy | 2 +- .../LitTests/LitTest/c++/functions.dfy | 2 +- .../TestFiles/LitTests/LitTest/c++/tuple.dfy | 2 +- .../LitTests/LitTest/c++/tuple.dfy.expect | 2 +- .../LitTests/LitTest/comp/CSharpStyling.dfy | 2 +- .../LitTest/comp/CSharpStyling.dfy.expect | 2 +- .../LitTest/comp/CompileWithArguments.dfy | 4 +- .../LitTest/comp/CompileWithArgumentsFail.dfy | 2 +- .../comp/CompileWithArgumentsFail2.dfy | 2 +- .../LitTests/LitTest/comp/Extern.dfy | 10 +-- .../LitTest/comp/ExternCopyFromTrait.dfy | 2 +- .../LitTests/LitTest/comp/ExternCtors.dfy | 6 +- .../LitTest/comp/ExternDafnyString.dfy | 2 +- .../LitTest/comp/ExternJavaString.dfy | 2 +- .../LitTest/comp/ExternNestedModule.dfy | 2 +- .../LitTests/LitTest/comp/JsModule.dfy | 3 +- .../LitTest/comp/Libraries/consumer.dfy | 2 +- .../LitTests/LitTest/comp/MainMethod.dfy | 90 +++++++++---------- .../TestFiles/LitTests/LitTest/comp/Print.dfy | 8 +- .../comp/compile1quiet/CompileRunQuietly.dfy | 14 +-- .../compile1verbose/CompileAndThenRun.dfy | 14 +-- .../LitTest/comp/compile3/JustRun.dfy | 24 ++--- .../comp/manualcompile/ManualCompile.dfy | 12 +-- ...edExterns.dfy => TestedExterns.legacy.dfy} | 2 +- ...expect => TestedExterns.legacy.dfy.expect} | 4 +- ...cs => TestedExterns.legacy.dfy.externs.cs} | 0 .../LitTest/dafny0/ArrayElementInit.dfy | 4 +- .../LitTest/dafny0/ArrayElementInitERR.dfy | 4 +- .../dafny0/ArrayElementInitResolution.dfy | 2 +- .../AsIs-SimplifiedExpanded-Resolve.dfy | 2 +- .../LitTest/dafny0/ByMethodResolution.dfy | 2 +- .../LitTest/dafny0/CompilationErrors.dfy | 6 +- .../LitTest/dafny0/DiamondImports.dfy | 2 +- .../dafny0/EqualityTypesModuleExports.dfy | 2 +- .../LitTest/dafny0/ErrorsInRelatedModules.dfy | 2 +- .../LitTest/dafny0/ForLoops-Resolution.dfy | 2 +- ...ation.dfy => ForallCompilation.legacy.dfy} | 0 ...ct => ForallCompilation.legacy.dfy.expect} | 0 .../dafny0/GeneralNewtypeResolution.dfy | 4 +- .../LitTest/dafny0/GeneralNewtypeVerify.dfy | 2 +- .../dafny0/GhostAllocations-Resolution.dfy | 2 +- .../LitTests/LitTest/dafny0/GhostGuards.dfy | 3 +- .../LitTest/dafny0/GhostGuards.dfy.expect | 10 +-- .../LitTest/dafny0/JavaUseRuntimeLib.dfy | 2 +- .../LitTest/dafny0/LabeledAsserts.dfy | 2 +- .../dafny0/LabeledAssertsResolution.dfy | 2 +- .../LitTest/dafny0/MapMergeSubtraction.dfy | 2 +- .../LitTest/dafny0/MiscTypeInferenceTests.dfy | 2 +- .../LitTest/dafny0/ModuleInsertion.dfy | 4 +- .../LitTest/dafny0/ModuleInsertion.dfy.expect | 2 + .../LitTest/dafny0/NativeTypeResolution.dfy | 2 +- .../LitTests/LitTest/dafny0/Newtypes.dfy | 4 +- .../LitTest/dafny0/ParameterResolution.dfy | 2 +- .../LitTest/dafny0/PrettyPrinting.dfy | 4 +- .../LitTest/dafny0/PrintEffectsResolution.dfy | 4 +- .../QuantificationNewSyntaxResolution.dfy | 2 +- .../LitTest/dafny0/RuntimeTypeTests1.dfy | 2 +- .../LitTest/dafny0/RuntimeTypeTests2.dfy | 2 +- .../LitTests/LitTest/dafny0/Simple.dfy | 4 +- .../LitTests/LitTest/dafny0/SubsetTypes.dfy | 2 +- .../LitTest/dafny0/SubsetTypesERR.dfy | 2 +- .../LitTest/dafny0/Twostate-Verification.dfy | 2 +- .../dafny0/Twostate-Verification.dfy.expect | 1 + .../LitTest/dafny0/TypeConstraints.dfy | 2 +- .../LitTest/dafny0/TypeConstraintsRefresh.dfy | 2 +- .../LitTest/dafny2/SnapshotableTrees.dfy | 2 +- .../LitTest/dafny2/Z-BirthdayBook.dfy | 2 +- .../LitTests/LitTest/dafny4/Bug62.dfy | 2 +- .../LitTests/LitTest/dafny4/Bug88.dfy | 2 +- .../LitTests/LitTest/dafny4/Regression11.dfy | 2 +- .../LitTests/LitTest/dafny4/Regression12.dfy | 2 +- .../LitTests/LitTest/dafny4/Regression15.dfy | 2 +- .../LitTests/LitTest/dafny4/git-issue167.dfy | 2 +- .../LitTests/LitTest/dafny4/git-issue228.dfy | 4 +- ...git-issue59.dfy => git-issue59.legacy.dfy} | 2 +- ...y.expect => git-issue59.legacy.dfy.expect} | 2 +- ...t-issue59.dfyi => git-issue59.legacy.dfyi} | 0 .../LitTests/LitTest/dafny4/git-issue70.dfy | 2 +- .../standardLibraryOptionMismatch.dfy | 2 +- .../standardLibraryOptionMismatch.dfy.expect | 4 +- .../examples/Simple_compiler/Compiler.dfy | 6 +- .../LitTest/examples/parser_combinators.dfy | 4 +- .../examples/parser_combinators.dfy.expect | 2 + .../exceptions/TestAttributeErrors.dfy | 2 +- .../expectations/ExpectAndExceptions.dfy | 8 +- .../expectations/ExpectWithMessage.dfy | 8 +- .../ExpectWithNonStringMessage.dfy | 10 +-- .../LitTest/exports/ExportRefinement.dfy | 6 +- .../exports/ExportRefinement.dfy.expect | 2 + .../LitTest/exports/ExportResolve.dfy | 2 +- .../LitTests/LitTest/exports/ExportVerify.dfy | 2 +- .../LitTests/LitTest/exports/xrefine1.dfy | 2 +- .../LitTest/git-issues/git-issue-1005.dfy | 2 +- .../LitTest/git-issues/git-issue-1074.dfy | 2 +- .../LitTest/git-issues/git-issue-1111.dfy | 2 +- .../LitTest/git-issues/git-issue-1129.dfy | 10 +-- .../git-issues/git-issue-1151-more.dfy | 12 +-- .../LitTest/git-issues/git-issue-1151.dfy | 2 +- .../LitTest/git-issues/git-issue-1172.dfy | 2 +- .../LitTest/git-issues/git-issue-1199.dfy | 2 +- .../LitTest/git-issues/git-issue-1212.dfy | 2 +- .../LitTest/git-issues/git-issue-1229.dfy | 2 +- .../LitTest/git-issues/git-issue-1248.dfy | 2 +- .../LitTest/git-issues/git-issue-1256.dfy | 2 +- .../LitTest/git-issues/git-issue-1377.dfy | 2 +- .../LitTest/git-issues/git-issue-1419.dfy | 2 +- .../LitTest/git-issues/git-issue-1604c.dfy | 2 +- .../LitTest/git-issues/git-issue-1619.dfy | 2 +- .../LitTest/git-issues/git-issue-1731.dfy | 2 +- .../LitTest/git-issues/git-issue-1762.dfy | 2 +- .../LitTest/git-issues/git-issue-179.dfy | 8 +- .../LitTest/git-issues/git-issue-1887.dfy | 2 +- .../LitTest/git-issues/git-issue-2071.dfy | 2 +- .../LitTest/git-issues/git-issue-2134.dfy | 2 +- .../LitTest/git-issues/git-issue-2216.dfy | 2 +- .../LitTest/git-issues/git-issue-2726.dfy | 2 +- .../LitTest/git-issues/git-issue-2828.dfy | 2 +- .../LitTest/git-issues/git-issue-2852.dfy | 5 +- .../LitTest/git-issues/git-issue-2885.dfy | 2 +- .../LitTest/git-issues/git-issue-3273.dfy | 2 +- .../LitTest/git-issues/git-issue-3918.dfy | 2 +- .../LitTest/git-issues/git-issue-3921.dfy | 2 +- .../LitTest/git-issues/git-issue-3922.dfy | 2 +- .../LitTest/git-issues/git-issue-3962.dfy | 2 +- .../LitTest/git-issues/git-issue-403.dfy | 3 +- .../LitTest/git-issues/git-issue-4131.dfy | 2 +- .../LitTest/git-issues/git-issue-4162.dfy | 10 +-- .../LitTest/git-issues/git-issue-448.dfy | 2 +- .../LitTest/git-issues/git-issue-4724.dfy | 2 +- .../LitTest/git-issues/git-issue-484.dfy | 2 +- .../LitTest/git-issues/git-issue-495.dfy | 2 +- .../LitTest/git-issues/git-issue-555.dfy | 8 +- .../LitTest/git-issues/git-issue-590.dfy | 2 +- .../LitTest/git-issues/git-issue-633.dfy | 10 +-- .../LitTest/git-issues/git-issue-643.dfy | 8 +- .../LitTest/git-issues/git-issue-643a.dfy | 8 +- .../LitTest/git-issues/git-issue-663.dfy | 2 +- .../LitTest/git-issues/git-issue-666.dfy | 2 +- .../LitTest/git-issues/git-issue-697c.dfy | 2 +- .../LitTest/git-issues/git-issue-755.dfy | 8 +- .../LitTest/git-issues/git-issue-856.dfy | 8 +- .../LitTest/git-issues/git-issue-889a.dfy | 2 +- .../LitTest/git-issues/git-issue-889b.dfy | 2 +- .../LitTest/git-issues/git-issue-907.dfy | 2 +- .../LitTest/git-issues/git-issue-Main.dfy | 8 +- .../LitTest/git-issues/git-issue-Main0.dfy | 16 ++-- .../LitTest/git-issues/git-issue-Main2.dfy | 8 +- .../LitTest/git-issues/git-issue-Main4.dfy | 48 +++++----- .../LitTest/git-issues/git-issue-MainE.dfy | 30 +++---- .../git-issues/git-issue-MainE.dfy.expect | 3 - .../LitTest/git-issues/github-issue-305-b.dfy | 2 +- .../LitTest/git-issues/github-issue-305-c.dfy | 2 +- .../git-issues/github-issue-305-c.dfy.expect | 1 - .../TestFiles/LitTests/LitTest/hofs/Apply.dfy | 4 +- .../LitTest/hofs/ArrowTypeOptimizations.dfy | 3 +- .../hofs/ArrowTypeOptimizations.dfy.expect | 41 ++++----- .../LitTests/LitTest/hofs/Classes.dfy | 4 +- .../hofs/{Folding.dfy => Folding.legacy.dfy} | 0 ...g.dfy.expect => Folding.legacy.dfy.expect} | 0 .../LitTest/hofs/ReadsReadsOnMethods.dfy | 2 +- .../LitTests/LitTest/hofs/ResolveError.dfy | 2 +- .../TestFiles/LitTests/LitTest/hofs/Types.dfy | 2 +- .../LitTest/irondafny0/opened_workaround.dfy | 2 +- .../LitTests/LitTest/lambdas/StateMonad.dfy | 2 +- .../LitTests/LitTest/logger/JsonLogger.dfy | 1 + .../logger/ProofDependencyWarnings.dfy | 1 + .../LitTests/LitTest/logger/VerboseName.dfy | 8 +- .../metatests/ConsistentWhenSupported.dfy | 12 +-- .../LitTests/LitTest/name with space/run.dfy | 2 +- .../patterns/PatternMatchingErrors.dfy | 2 +- .../LitTests/LitTest/traits/GeneralTraits.dfy | 2 +- .../LitTest/traits/GeneralTraitsVerify.dfy | 2 +- .../traits/GeneralTraitsVerify.dfy.expect | 2 +- .../LitTest/traits/NonReferenceTraits.dfy | 4 +- .../traits/NonReferenceTraitsVerify.dfy | 2 +- .../LitTest/traits/TraitCompileErrors.dfy | 2 +- .../LitTests/LitTest/traits/TraitVariance.dfy | 2 +- .../LitTests/LitTest/traits/TraitVerify.dfy | 6 +- .../LitTest/traits/TraitVerify.dfy.expect | 2 +- .../comp/CompileWithArguments.dfy | 4 +- .../unicodechars/comp/ExternDafnyString.dfy | 2 +- .../unicodechars/comp/ExternJavaString.dfy | 2 +- .../expectations/ExpectAndExceptions.dfy | 10 +-- .../expectations/ExpectWithMessage.dfy | 10 +-- .../ExpectWithNonStringMessage.dfy | 10 +-- .../LitTests/LitTest/wishlist/GoModule.dfy | 3 +- 189 files changed, 484 insertions(+), 475 deletions(-) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/{TestedExterns.dfy => TestedExterns.legacy.dfy} (86%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/{TestedExterns.dfy.expect => TestedExterns.legacy.dfy.expect} (85%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/{TestedExterns.dfy.externs.cs => TestedExterns.legacy.dfy.externs.cs} (100%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/{ForallCompilation.dfy => ForallCompilation.legacy.dfy} (100%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/{ForallCompilation.dfy.expect => ForallCompilation.legacy.dfy.expect} (100%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/{git-issue59.dfy => git-issue59.legacy.dfy} (80%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/{git-issue59.dfy.expect => git-issue59.legacy.dfy.expect} (56%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/{git-issue59.dfyi => git-issue59.legacy.dfyi} (100%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/{Folding.dfy => Folding.legacy.dfy} (100%) rename Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/{Folding.dfy.expect => Folding.legacy.dfy.expect} (100%) diff --git a/Source/DafnyCore/Backends/Dafny/BuilderSyntaxTree.cs b/Source/DafnyCore/Backends/Dafny/BuilderSyntaxTree.cs index f1b225bd72..8cb941f875 100644 --- a/Source/DafnyCore/Backends/Dafny/BuilderSyntaxTree.cs +++ b/Source/DafnyCore/Backends/Dafny/BuilderSyntaxTree.cs @@ -17,7 +17,7 @@ public override ConcreteSyntaxTree Fork(int relativeIndent = 0) { if (Builder is StatementContainer statementContainer) { return new BuilderSyntaxTree(statementContainer.Fork()); } else { - DafnyCodeGenerator.throwGeneralUnsupported(); // Warning: this is an invalid operation: cannot fork builder of type Builder.GetType() + DafnyCodeGenerator.ThrowGeneralUnsupported(); // Warning: this is an invalid operation: cannot fork builder of type Builder.GetType() throw new InvalidOperationException(); } } diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index 523a2b4123..c205bd9eb7 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -38,7 +38,7 @@ public DafnyCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(o } } - public static void throwGeneralUnsupported() { + public static void ThrowGeneralUnsupported() { // throw new InvalidOperationException(); // (useful for debugging) throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests); } @@ -81,12 +81,12 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { } public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); throw new InvalidOperationException(); } protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); throw new InvalidOperationException(); } @@ -151,7 +151,7 @@ protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to if (from == null || to == null || from.Equals(to, true)) { return wr; } else { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); throw new InvalidOperationException(); } } @@ -163,7 +163,7 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool List typeParams = new(); foreach (var tp in typeParameters) { if (!isTpSupported(tp)) { - throwGeneralUnsupported(); //("Contravariance in type parameters"); + ThrowGeneralUnsupported(); //("Contravariance in type parameters"); } typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(IdProtect(tp.GetCompileName(Options))))); @@ -206,7 +206,7 @@ protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxT List typeParams = new(); foreach (var tp in dt.TypeArgs) { if (!isTpSupported(tp) && !(dt is TupleTypeDecl)) { - throwGeneralUnsupported(); //("Contravariance in type parameters"); + ThrowGeneralUnsupported(); //("Contravariance in type parameters"); } typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(IdProtect(tp.GetCompileName(Options))))); @@ -307,10 +307,10 @@ private DAST.Type GenType(Type typ) { var valueType = map.Range; return (DAST.Type)DAST.Type.create_Map(GenType(keyType), GenType(valueType)); } else if (xType is BitvectorType) { - throwGeneralUnsupported(); //("Bitvector types"); + ThrowGeneralUnsupported(); //("Bitvector types"); throw new InvalidOperationException(); } else { - throwGeneralUnsupported(); //("Type name for " + xType + " (" + typ.GetType() + ")"); + ThrowGeneralUnsupported(); //("Type name for " + xType + " (" + typ.GetType() + ")"); throw new InvalidOperationException(); } } @@ -336,7 +336,7 @@ protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree List typeParams = new(); foreach (var tp in sst.TypeArgs) { if (!isTpSupported(tp)) { - throwGeneralUnsupported(); //("Contravariance in type parameters"); + ThrowGeneralUnsupported(); //("Contravariance in type parameters"); } typeParams.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(tp.Name))); @@ -369,13 +369,13 @@ public ClassWriter(DafnyCodeGenerator compiler, bool hasTypeArgs, ClassLike buil public ConcreteSyntaxTree CreateMethod(Method m, List typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) { if (m.IsStatic && this.hasTypeArgs) { - throwGeneralUnsupported(); //("Static methods with type arguments"); + ThrowGeneralUnsupported(); //("Static methods with type arguments"); } List astTypeArgs = new(); foreach (var typeArg in typeArgs) { if (!isTpSupported(typeArg.Formal)) { - throwGeneralUnsupported(); //("Contravariance in type parameters") + ThrowGeneralUnsupported(); //("Contravariance in type parameters") } astTypeArgs.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(compiler.IdProtect(typeArg.Formal.GetCompileName(compiler.Options))))); @@ -423,13 +423,13 @@ public ConcreteSyntaxTree CreateFunction(string name, List formals, Type resultType, IToken tok, bool isStatic, bool createBody, MemberDecl member, bool forBodyInheritance, bool lookasideBody) { if (isStatic && this.hasTypeArgs) { - throwGeneralUnsupported(); //("Static methods with type arguments"); + ThrowGeneralUnsupported(); //("Static methods with type arguments"); } List astTypeArgs = new(); foreach (var typeArg in typeArgs) { if (!isTpSupported(typeArg.Formal)) { - throwGeneralUnsupported(); //("Contravariance in type parameters"); + ThrowGeneralUnsupported(); //("Contravariance in type parameters"); } astTypeArgs.Add((DAST.Type)DAST.Type.create_TypeArg(Sequence.UnicodeFromString(compiler.IdProtect(typeArg.Formal.GetCompileName(compiler.Options))))); @@ -465,7 +465,7 @@ public ConcreteSyntaxTree CreateFunction(string name, List.create_Some( @@ -679,7 +679,7 @@ protected override void EmitNameAndActualTypeArgs(string protectedName, List st2 && st2.Builder is CallStmtBuilder callStmt) { callStmt.SetName(protectedName); } else { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } base.EmitNameAndActualTypeArgs(protectedName, typeArgs, tok, wr); @@ -691,7 +691,7 @@ protected override void TypeArgDescriptorUse(bool isStatic, bool lookasideBody, } protected override bool DeclareFormal(string prefix, string name, Type type, IToken tok, bool isInParam, ConcreteSyntaxTree wr) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); throw new InvalidOperationException(); } @@ -901,7 +901,7 @@ protected override ILvalue SeqSelectLvalue(SeqSelectExpr ll, ConcreteSyntaxTree } protected override ILvalue MultiSelectLvalue(MultiSelectExpr ll, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); throw new InvalidOperationException(); } @@ -1032,11 +1032,11 @@ protected override ConcreteSyntaxTree CreateDoublingForLoop(string indexVar, int } protected override void EmitIncrementVar(string varName, ConcreteSyntaxTree wr) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } protected override void EmitDecrementVar(string varName, ConcreteSyntaxTree wr) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } protected override ConcreteSyntaxTree EmitQuantifierExpr(Action collection, bool isForall, Type collectionElementType, BoundVar bv, ConcreteSyntaxTree wr) { @@ -1080,7 +1080,7 @@ protected override void EmitDowncastVariableAssignment(string boundVarName, Type protected override ConcreteSyntaxTree CreateForeachIngredientLoop(string boundVarName, int L, string tupleTypeArgs, out ConcreteSyntaxTree collectionWriter, ConcreteSyntaxTree wr) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); throw new InvalidOperationException(); } @@ -1157,7 +1157,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { new Rune(codePoint) )); } else { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); throw new InvalidOperationException(); } break; @@ -1229,13 +1229,13 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { } protected override void EmitStringLiteral(string str, bool isVerbatim, ConcreteSyntaxTree wr) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); throw new InvalidOperationException(); } protected override ConcreteSyntaxTree EmitBitvectorTruncation(BitvectorType bvType, [CanBeNull] NativeType nativeType, bool surroundByUnchecked, ConcreteSyntaxTree wr) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); throw new InvalidOperationException(); } @@ -1269,7 +1269,7 @@ public override string PublicIdProtect(string name) { } protected override string FullTypeName(UserDefinedType udt, MemberDecl member = null) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); throw new InvalidOperationException(); } @@ -1465,7 +1465,7 @@ protected override void GetSpecialFieldInfo(SpecialField.ID id, object idParam, case SpecialField.ID.ArrayLength: break; default: - throwGeneralUnsupported(); //("Special field: " + id); + ThrowGeneralUnsupported(); //("Special field: " + id); throw new InvalidOperationException(); } } @@ -1656,7 +1656,7 @@ protected override void EmitIndexCollectionSelect(Expression source, Expression protected override void EmitIndexCollectionUpdate(Expression source, Expression index, Expression value, CollectionType resultCollectionType, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } protected override void EmitSeqSelectRange(Expression source, Expression lo, Expression hi, bool fromArray, @@ -1852,11 +1852,11 @@ protected override void EmitBoolBoundedPool(bool inLetExprBody, ConcreteSyntaxTr } protected override void EmitCharBoundedPool(bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } protected override void EmitWiggleWaggleBoundedPool(bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } protected override void EmitSetBoundedPool(Expression of, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { @@ -1873,15 +1873,15 @@ protected override void EmitSetBoundedPool(Expression of, string propertySuffix, } protected override void EmitMultiSetBoundedPool(Expression of, bool includeDuplicates, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } protected override void EmitSubSetBoundedPool(Expression of, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } protected override void EmitMapBoundedPool(Expression map, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } protected override void EmitSeqBoundedPool(Expression of, bool includeDuplicates, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { @@ -1899,7 +1899,7 @@ protected override void EmitSeqBoundedPool(Expression of, bool includeDuplicates } protected override void EmitDatatypeBoundedPool(IVariable bv, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } protected override void CreateIIFE(string bvName, Type bvType, IToken bvTok, Type bodyType, IToken bodyTok, @@ -2083,7 +2083,7 @@ protected override void EmitITE(Expression guard, Expression thn, Expression els } protected override void EmitIsZero(string varName, ConcreteSyntaxTree wr) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } protected override void EmitConversionExpr(Expression fromExpr, Type fromType, Type toType, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { @@ -2144,7 +2144,7 @@ protected override void EmitCollectionDisplay(CollectionType ct, IToken tok, Lis Sequence.FromArray(elementsAST.ToArray()) )); } else if (ct is MultiSetType multiSet) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } else if (ct is SeqType seq) { builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_SeqValue( Sequence.FromArray(elementsAST.ToArray()), @@ -2182,24 +2182,24 @@ protected override void EmitMapDisplay(MapType mt, IToken tok, List GetSubtypeCondition(string tmpVarN baseExpr = DAST.Expression.create_Literal(DAST.Literal.create_BoolLiteral(true)); } else { // typeTest = $"{tmpVarName} instanceof {TypeName(boundVarType, wPreconditions, tok)}"; - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); throw new InvalidOperationException(); } @@ -2257,7 +2257,7 @@ protected override Action GetSubtypeCondition(string tmpVarN } protected override string GetCollectionBuilder_Build(CollectionType ct, IToken tok, string collName, ConcreteSyntaxTree wr) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); throw new InvalidOperationException(); } @@ -2288,7 +2288,7 @@ protected override (Type, Action) EmitIntegerRange(Type type } protected override void EmitNull(Type _, ConcreteSyntaxTree wr) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBody, string type, @@ -2297,7 +2297,7 @@ protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBod } protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr) { - throwGeneralUnsupported(); + ThrowGeneralUnsupported(); } } diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs index e3b29b9a06..f770c2141f 100644 --- a/Source/IntegrationTests/LitTests.cs +++ b/Source/IntegrationTests/LitTests.cs @@ -62,7 +62,7 @@ IEnumerable AddExtraArgs(IEnumerable args, IEnumerable l string[] defaultResolveArgs = new[] { "resolve", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false" }; string[] defaultVerifyArgs = new[] { "verify", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false", "--cores:2", "--verification-time-limit:300", "--resource-limit:50e6" }; - //string[] defaultTranslateArgs = new[] { "translate", "--use-basename-for-filename", "--cores:2", "--standard-libraries:false", "--verification-time-limit:300", "--resource-limit:50e6" }; + string[] defaultTranslateArgs = new[] { "--use-basename-for-filename", "--cores:2", "--standard-libraries:false", "--verification-time-limit:300", "--resource-limit:50e6" }; string[] defaultBuildArgs = new[] { "build", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false", "--cores:2", "--verification-time-limit:300", "--resource-limit:50e6" }; string[] defaultRunArgs = new[] { "run", "--use-basename-for-filename", "--show-snippets:false", "--standard-libraries:false", "--cores:2", "--verification-time-limit:300", "--resource-limit:50e6" }; @@ -82,8 +82,17 @@ IEnumerable AddExtraArgs(IEnumerable args, IEnumerable l "%resolve", (args, config) => DafnyCommand(AddExtraArgs(defaultResolveArgs, args), config, InvokeMainMethodsDirectly) }, { - "%translate", (args, config) => - DafnyCommand(AddExtraArgs(new[] { "translate" }, args), config, InvokeMainMethodsDirectly) + "%translate", (args, config) => { + var totalArgs = args.ToList(); + if (totalArgs.Any()) { + var target = totalArgs.First(); + totalArgs = new[] { target }.Concat(defaultTranslateArgs).Concat(totalArgs.Skip(1)).ToList(); + } else { + totalArgs = defaultTranslateArgs.ToList(); + } + return DafnyCommand(AddExtraArgs(new[] { "translate" }, totalArgs), config, + InvokeMainMethodsDirectly); + } }, { "%verify", (args, config) => DafnyCommand(AddExtraArgs(defaultVerifyArgs, args), config, InvokeMainMethodsDirectly) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/extern.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/extern.dfy index 5c2d6c17d0..d320709136 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/extern.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/extern.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" ExternDefs.h > "%t" +// RUN: %run --target cpp --unicode-char false "%s" --input ExternDefs.h > "%t" // RUN: %diff "%s.expect" "%t" module {:extern "Extern"} Extern { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/functions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/functions.dfy index be47392637..a5a0c65721 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/functions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/functions.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 "%s" ExternDefs.h > "%t" +// RUN: %run --target cpp --unicode-char false "%s" --input ExternDefs.h > "%t" // RUN: %diff "%s.expect" "%t" module {:extern "Extern"} Extern { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/tuple.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/tuple.dfy index 45e12e7322..9f2997cfaa 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/tuple.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/tuple.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cpp /unicodeChar:0 ExternDefs.h "%s" > "%t" +// RUN: %run --target cpp --unicode-char false --input ExternDefs.h "%s" > "%t" // RUN: %diff "%s.expect" "%t" newtype uint32 = i:int | 0 <= i < 0x100000000 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/tuple.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/tuple.dfy.expect index 08a237fe13..ad056416a8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/tuple.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/c++/tuple.dfy.expect @@ -1,3 +1,3 @@ -Dafny program verifier finished with 6 verified, 0 errors +Dafny program verifier finished with 7 verified, 0 errors 1 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CSharpStyling.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CSharpStyling.dfy index 584eac0b88..a9ec4d4142 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CSharpStyling.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CSharpStyling.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cs "%s" %S/CSharpStyling2.cs > "%t" +// RUN: %run "%s" --input %S/CSharpStyling2.cs > "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CSharpStyling.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CSharpStyling.dfy.expect index ad4acd57b9..a62b408f2f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CSharpStyling.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CSharpStyling.dfy.expect @@ -1,5 +1,5 @@ -Dafny program verifier finished with 1 verified, 0 errors +Dafny program verifier finished with 3 verified, 0 errors 50 2 3 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArguments.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArguments.dfy index 9530cdc597..25baebae41 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArguments.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArguments.dfy @@ -4,8 +4,8 @@ // RUN: %run --no-verify --target:cpp --unicode-char:false "%s" Cpp Yipee >> "%t" // RUN: %run --no-verify --target:java "%s" -- Java --heya >> "%t" // RUN: %run --no-verify --target:js "%s" -- Javascript 2 >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" --args Python 1 >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" --args "Go go" 1 >> "%t" +// RUN: %run --no-verify --target py "%s" Python 1 >> "%t" +// RUN: %run --no-verify --target go "%s" "Go go" 1 >> "%t" // RUN: %build --no-verify --target:cs "%s" --output:%s.dll // RUN: dotnet %s.dll "dotnet" "howdy" >> "%t" // RUN: dotnet %s.dll "dotnet" "hello" >> "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArgumentsFail.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArgumentsFail.dfy index c23739cb13..74341340f9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArgumentsFail.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArgumentsFail.dfy @@ -1,5 +1,5 @@ // RUN: %verify "%s" > "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:cs "%s" --args csharp 1 >> "%t" +// RUN: %exits-with 3 %run --no-verify --target cs "%s" csharp 1 >> "%t" // RUN: %diff "%s.expect" "%t" method Main(args: int) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArgumentsFail2.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArgumentsFail2.dfy index b9e00473ae..5341dfb900 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArgumentsFail2.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/CompileWithArgumentsFail2.dfy @@ -1,5 +1,5 @@ // RUN: %verify "%s" > "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:cs "%s" --args csharp 1 >> "%t" +// RUN: %exits-with 3 %run --no-verify --target cs "%s" csharp 1 >> "%t" // RUN: %diff "%s.expect" "%t" method Main(args: array, dummy: int) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Extern.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Extern.dfy index 4b5717c7d6..7d1e55c39f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Extern.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Extern.dfy @@ -1,9 +1,9 @@ // RUN: %verify "%s" > "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" %S/Extern2.cs >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" %S/Extern3.js >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" %S/Extern4.go >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" %S/SingletonOptimization.java %S/LibClass.java %S/OtherClass.java %S/AllDafny.java %S/Mixed.java %S/AllExtern.java >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" %S/Extern5.py >> "%t" +// RUN: %run --no-verify --target cs "%s" --input %S/Extern2.cs >> "%t" +// RUN: %run --no-verify --target js "%s" --input %S/Extern3.js >> "%t" +// RUN: %run --no-verify --target go "%s" --input %S/Extern4.go >> "%t" +// RUN: %run --no-verify --target java "%s" --input %S/SingletonOptimization.java --input %S/LibClass.java --input %S/OtherClass.java --input %S/AllDafny.java --input %S/Mixed.java --input %S/AllExtern.java >> "%t" +// RUN: %run --no-verify --target py "%s" --input %S/Extern5.py >> "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCopyFromTrait.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCopyFromTrait.dfy index aab0976fb4..c4f2acf0ba 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCopyFromTrait.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCopyFromTrait.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:4 /compileTarget:cs "%s" %S/ExternCopyFromTraitLibrary.cs > "%t" +// RUN: %run --target cs "%s" --input %S/ExternCopyFromTraitLibrary.cs > "%t" // RUN: %diff "%s.expect" "%t" /// This file tests inheritance of `:extern` annotation in traits. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy index 19977ece6d..d0d50d7383 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternCtors.dfy @@ -1,6 +1,6 @@ -// RUN: %dafny /compile:3 /compileTarget:cs "%s" %S/ExternCtors-externs/Library.cs > "%t" -// RUN: %dafny /compile:3 /compileTarget:java "%s" %S/ExternCtors-externs/Class.java >> "%t" -// RUN: %dafny /compile:3 /compileTarget:py "%s" %S/ExternCtors-externs/Library.py >> "%t" +// RUN: %run --target cs "%s" --input %S/ExternCtors-externs/Library.cs > "%t" +// RUN: %run --target java "%s" --input %S/ExternCtors-externs/Class.java >> "%t" +// RUN: %run --target py "%s" --input %S/ExternCtors-externs/Library.py >> "%t" // RUN: %diff "%s.expect" "%t" // FIXME: Extern constructors are currently broken in Go and JavaScript, diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternDafnyString.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternDafnyString.dfy index bcb67e80ea..ec0cfa8386 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternDafnyString.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternDafnyString.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /unicodeChar:0 /compileTarget:java "%s" %S/Conversions.java %S/ExternDafnyString.java > "%t" +// RUN: %run --unicode-char false --target java "%s" --input %S/Conversions.java --input %S/ExternDafnyString.java > "%t" // RUN: %diff "%s.expect" "%t" // In this example, the extern method obtains a Java string and returns it as a Dafny string. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternJavaString.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternJavaString.dfy index 42b9fbe50c..c92aff8408 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternJavaString.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternJavaString.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /unicodeChar:0 /compileTarget:java "%s" %S/Conversions.java %S/ExternJavaString.java > "%t" +// RUN: %run --unicode-char false --target java "%s" --input %S/Conversions.java --input %S/ExternJavaString.java > "%t" // RUN: %diff "%s.expect" "%t" // In this example, the extern method obtains a Java string and returns it as such. // The Dafny code converts that Java string to a Dafny string. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternNestedModule.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternNestedModule.dfy index fb6e834bdc..ecddd019e0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternNestedModule.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/ExternNestedModule.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:4 /spillTargetCode:2 /compileTarget:py %S/ExternNestedModule.py "%s" > "%t" +// RUN: %run --target py "%s" --input %S/ExternNestedModule.py > "%t" // RUN: %diff "%s.expect" "%t" method Main(){ diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/JsModule.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/JsModule.dfy index e9f40640f4..961d3921ab 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/JsModule.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/JsModule.dfy @@ -1,6 +1,5 @@ // NONUNIFORM: Javascript-specific extern test -// RUN: %dafny /compile:3 /unicodeChar:0 "%s" /compileTarget:js > "%t" -// note: putting /compileTarget:js after "%s" overrides user-provided option +// RUN: %run --unicode-char false --target js "%s" > "%t" // RUN: %diff "%s.expect" "%t" // "url" is a built-in package in node, so it should be accessible to the diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Libraries/consumer.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Libraries/consumer.dfy index efd3484bd6..45bc8e4a22 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Libraries/consumer.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Libraries/consumer.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /library:"%S/Inputs/directLibrary.dfy" /library:"%S/Inputs/secondLibrary.dfy" /compile:0 /spillTargetCode:3 "%s" > "%t" +// RUN: %translate cs --library "%S/Inputs/directLibrary.dfy" --library "%S/Inputs/secondLibrary.dfy" "%s" > "%t" // RUN: %diff "%s.expect" "%t" // RUN: %OutputCheck "%s" --file-to-check="%S/consumer.cs" // CHECK: GloballyUniqueProducer diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/MainMethod.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/MainMethod.dfy index bedd340b4e..85692695e3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/MainMethod.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/MainMethod.dfy @@ -1,55 +1,55 @@ // NONUNIFORM: multiple testing scenarios (could be split into several uniform tests) // RUN: %verify "%s" > "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:cs "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:cs "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:cs "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:cs "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:cs "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:cs "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:cs "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:cs "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:cs "%s" >> "%t" +// RUN: %run --no-verify --main-method Cl.Static --target cs "%s" >> "%t" +// RUN: %run --no-verify --main-method Cl.Instance --target cs "%s" >> "%t" +// RUN: %run --no-verify --main-method Tr.Static --target cs "%s" >> "%t" +// RUN: %run --no-verify --main-method Dt.Static --target cs "%s" >> "%t" +// RUN: %run --no-verify --main-method Dt.Instance --target cs "%s" >> "%t" +// RUN: %run --no-verify --main-method Co.Static --target cs "%s" >> "%t" +// RUN: %run --no-verify --main-method Co.Instance --target cs "%s" >> "%t" +// RUN: %run --no-verify --main-method Nt.Static --target cs "%s" >> "%t" +// RUN: %run --no-verify --main-method Nt.Instance --target cs "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:js "%s" >> "%t" +// RUN: %run --no-verify --main-method Cl.Static --target js "%s" >> "%t" +// RUN: %run --no-verify --main-method Cl.Instance --target js "%s" >> "%t" +// RUN: %run --no-verify --main-method Tr.Static --target js "%s" >> "%t" +// RUN: %run --no-verify --main-method Dt.Static --target js "%s" >> "%t" +// RUN: %run --no-verify --main-method Dt.Instance --target js "%s" >> "%t" +// RUN: %run --no-verify --main-method Co.Static --target js "%s" >> "%t" +// RUN: %run --no-verify --main-method Co.Instance --target js "%s" >> "%t" +// RUN: %run --no-verify --main-method Nt.Static --target js "%s" >> "%t" +// RUN: %run --no-verify --main-method Nt.Instance --target js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:go "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:go "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:go "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:go "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:go "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:go "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:go "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:go "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:go "%s" >> "%t" +// RUN: %run --no-verify --main-method Cl.Static --target go "%s" >> "%t" +// RUN: %run --no-verify --main-method Cl.Instance --target go "%s" >> "%t" +// RUN: %run --no-verify --main-method Tr.Static --target go "%s" >> "%t" +// RUN: %run --no-verify --main-method Dt.Static --target go "%s" >> "%t" +// RUN: %run --no-verify --main-method Dt.Instance --target go "%s" >> "%t" +// RUN: %run --no-verify --main-method Co.Static --target go "%s" >> "%t" +// RUN: %run --no-verify --main-method Co.Instance --target go "%s" >> "%t" +// RUN: %run --no-verify --main-method Nt.Static --target go "%s" >> "%t" +// RUN: %run --no-verify --main-method Nt.Instance --target go "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:java "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:java "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:java "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:java "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:java "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:java "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:java "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:java "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:java "%s" >> "%t" +// RUN: %run --no-verify --main-method Cl.Static --target java "%s" >> "%t" +// RUN: %run --no-verify --main-method Cl.Instance --target java "%s" >> "%t" +// RUN: %run --no-verify --main-method Tr.Static --target java "%s" >> "%t" +// RUN: %run --no-verify --main-method Dt.Static --target java "%s" >> "%t" +// RUN: %run --no-verify --main-method Dt.Instance --target java "%s" >> "%t" +// RUN: %run --no-verify --main-method Co.Static --target java "%s" >> "%t" +// RUN: %run --no-verify --main-method Co.Instance --target java "%s" >> "%t" +// RUN: %run --no-verify --main-method Nt.Static --target java "%s" >> "%t" +// RUN: %run --no-verify --main-method Nt.Instance --target java "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Cl.Static /compileTarget:py "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Cl.Instance /compileTarget:py "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Tr.Static /compileTarget:py "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Dt.Static /compileTarget:py "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Dt.Instance /compileTarget:py "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Co.Static /compileTarget:py "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Co.Instance /compileTarget:py "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Nt.Static /compileTarget:py "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:Nt.Instance /compileTarget:py "%s" >> "%t" +// RUN: %run --no-verify --main-method Cl.Static --target py "%s" >> "%t" +// RUN: %run --no-verify --main-method Cl.Instance --target py "%s" >> "%t" +// RUN: %run --no-verify --main-method Tr.Static --target py "%s" >> "%t" +// RUN: %run --no-verify --main-method Dt.Static --target py "%s" >> "%t" +// RUN: %run --no-verify --main-method Dt.Instance --target py "%s" >> "%t" +// RUN: %run --no-verify --main-method Co.Static --target py "%s" >> "%t" +// RUN: %run --no-verify --main-method Co.Instance --target py "%s" >> "%t" +// RUN: %run --no-verify --main-method Nt.Static --target py "%s" >> "%t" +// RUN: %run --no-verify --main-method Nt.Instance --target py "%s" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Print.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Print.dfy index 0a7412248a..3eddc3ce15 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Print.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Print.dfy @@ -1,9 +1,9 @@ // NONUNIFORM: https://github.com/dafny-lang/dafny/issues/4108 and https://github.com/dafny-lang/dafny/issues/2582 // RUN: %verify --unicode-char false --relax-definite-assignment "%s" > "%t" -// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:cs "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:go "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:java "%s" >> "%t" +// RUN: %run --no-verify --unicode-char false --target cs "%s" >> "%t" +// RUN: %run --no-verify --unicode-char false --target js "%s" >> "%t" +// RUN: %run --no-verify --unicode-char false --target go "%s" >> "%t" +// RUN: %run --no-verify --unicode-char false --target java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" // Python salts hashes so they are not deterministic. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1quiet/CompileRunQuietly.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1quiet/CompileRunQuietly.dfy index 379841059b..a811b377b8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1quiet/CompileRunQuietly.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1quiet/CompileRunQuietly.dfy @@ -1,19 +1,19 @@ -// RUN: %dafny /unicodeChar:0 /compileTarget:cs "%s" > "%t" +// RUN: %build --unicode-char false --target cs "%s" > "%t" // RUN: dotnet %S/CompileRunQuietly.dll >> "%t" -// RUN: %dafny /unicodeChar:0 /compileTarget:js "%s" >> "%t" +// RUN: %build --unicode-char false --target js "%s" >> "%t" // RUN: node %S/CompileRunQuietly.js >> "%t" -// RUN: %dafny /unicodeChar:0 /compileTarget:go "%s" >> "%t" +// RUN: %build --unicode-char false --target go "%s" >> "%t" // RUN: %S/CompileRunQuietly >> "%t" -// RUN: %dafny /unicodeChar:0 /compileTarget:java "%s" >> "%t" -// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/CompileRunQuietly-java CompileRunQuietly >> "%t" +// RUN: %build --unicode-char false --target java "%s" >> "%t" +// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/CompileRunQuietly.jar CompileRunQuietly >> "%t" -// RUN: %dafny /unicodeChar:0 /compileTarget:cpp "%s" >> "%t" +// RUN: %build --unicode-char false --target cpp "%s" >> "%t" // RUN: %S/CompileRunQuietly.exe >> "%t" -// RUN: %dafny /unicodeChar:0 /compileTarget:py "%s" >> "%t" +// RUN: %build --unicode-char false --target py "%s" >> "%t" // RUN: python3 %S/CompileRunQuietly-py >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy index fbba2baa79..487d7b6ba7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile1verbose/CompileAndThenRun.dfy @@ -1,19 +1,19 @@ -// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:cs "%s" > "%t" +// RUN: %build --unicode-char false --verbose --target cs "%s" > "%t" // RUN: dotnet %S/CompileAndThenRun.dll >> "%t" -// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:js "%s" >> "%t" +// RUN: %build --unicode-char false --verbose --target js "%s" >> "%t" // RUN: node %S/CompileAndThenRun.js >> "%t" -// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:go "%s" >> "%t" +// RUN: %build --unicode-char false --verbose --target go "%s" >> "%t" // RUN: %S/CompileAndThenRun >> "%t" -// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:java "%s" >> "%t" -// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/CompileAndThenRun-java CompileAndThenRun >> "%t" +// RUN: %build --unicode-char false --verbose --target java "%s" >> "%t" +// RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/CompileAndThenRun.jar CompileAndThenRun >> "%t" -// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:cpp "%s" >> "%t" +// RUN: %build --unicode-char false --verbose --target cpp "%s" >> "%t" // RUN: %S/CompileAndThenRun.exe >> "%t" -// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:py "%s" >> "%t" +// RUN: %build --unicode-char false --verbose --target py "%s" >> "%t" // RUN: python3 %S/CompileAndThenRun-py >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy index 298221d5e3..bbbfff8cb8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/compile3/JustRun.dfy @@ -1,17 +1,17 @@ // NONUNIFORM: /compileVerbose:1 output is backend sensitive // (although the second set of comamnds could be separated out) -// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:cs /compile:3 "%s" > "%t" -// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:js /compile:3 "%s" >> "%t" -// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:go /compile:3 "%s" >> "%t" -// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:java /compile:3 "%s" >> "%t" -// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:cpp /compile:3 "%s" >> "%t" -// RUN: %dafny /unicodeChar:0 /compileVerbose:1 /compileTarget:py /compile:3 "%s" >> "%t" -// RUN: %dafny /unicodeChar:0 /compileTarget:cs /compile:3 "%s" >> "%t" -// RUN: %dafny /unicodeChar:0 /compileTarget:js /compile:3 "%s" >> "%t" -// RUN: %dafny /unicodeChar:0 /compileTarget:go /compile:3 "%s" >> "%t" -// RUN: %dafny /unicodeChar:0 /compileTarget:java /compile:3 "%s" >> "%t" -// RUN: %dafny /unicodeChar:0 /compileTarget:cpp /compile:3 "%s" >> "%t" -// RUN: %dafny /unicodeChar:0 /compileTarget:py /compile:3 "%s" >> "%t" +// RUN: %run --target cs --unicode-char false --verbose "%s" > "%t" +// RUN: %run --target js --unicode-char false --verbose "%s" >> "%t" +// RUN: %run --target go --unicode-char false --verbose "%s" >> "%t" +// RUN: %run --target java --unicode-char false --verbose "%s" >> "%t" +// RUN: %run --target cpp --unicode-char false --verbose "%s" >> "%t" +// RUN: %run --target py --unicode-char false --verbose "%s" >> "%t" +// RUN: %run --target cs --unicode-char false "%s" >> "%t" +// RUN: %run --target js --unicode-char false "%s" >> "%t" +// RUN: %run --target go --unicode-char false "%s" >> "%t" +// RUN: %run --target java --unicode-char false "%s" >> "%t" +// RUN: %run --target cpp --unicode-char false "%s" >> "%t" +// RUN: %run --target py --unicode-char false "%s" >> "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy index 6d08a2b3d1..b521245c0d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy @@ -1,24 +1,24 @@ // NONUNIFORM: Highly target language specific -// RUN: %baredafny translate cs %args --verbose --include-runtime "%s" > "%t" +// RUN: %translate cs --verbose --include-runtime "%s" > "%t" // RUN: dotnet build %S/ManualCompile.csproj // RUN: dotnet %S/bin/Debug/net6.0/ManualCompile.dll >> "%t" -// RUN: %dafny /compileVerbose:1 /compile:0 /spillTargetCode:2 /compileTarget:js "%s" >> "%t" +// RUN: %translate js --verbose --include-runtime "%s" >> "%t" // RUN: node %S/ManualCompile.js >> "%t" -// RUN: %dafny /compileVerbose:1 /compile:0 /spillTargetCode:2 /compileTarget:go "%s" >> "%t" +// RUN: %translate go --verbose --include-runtime "%s" >> "%t" // RUN: env GO111MODULE=auto GOPATH=%S/ManualCompile-go go run %S/ManualCompile-go/src/ManualCompile.go >> "%t" -// RUN: %baredafny translate java %args --verbose --include-runtime "%s" >> "%t" +// RUN: %translate java --verbose --include-runtime "%s" >> "%t" // RUN: javac %S/ManualCompile-java/ManualCompile.java %S/ManualCompile-java/**/*.java // RUN: java -cp %S/ManualCompile-java ManualCompile >> "%t" -// RUN: %dafny /compileVerbose:1 /compile:0 /unicodeChar:0 /spillTargetCode:2 /compileTarget:cpp "%s" >> "%t" +// RUN: %translate cpp --verbose --unicode-char=false --include-runtime "%s" >> "%t" // RUN: g++ -g -Wall -Wextra -Wpedantic -Wno-unused-variable -std=c++17 -I %binaryDir -o %S/ManualCompile.exe %S/ManualCompile.cpp // RUN: %S/ManualCompile.exe >> "%t" -// RUN: %dafny /compileVerbose:1 /compile:0 /spillTargetCode:2 /compileTarget:py "%s" >> "%t" +// RUN: %translate py --verbose "%s" --include-runtime >> "%t" // RUN: python3 %S/ManualCompile-py >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy similarity index 86% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy index 8986374753..1668615aba 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy @@ -1,6 +1,6 @@ // RUN: ! %dafny /compile:4 /runAllTests:1 /spillTargetCode:3 /testContracts:TestedExterns %s %s.externs.cs > %t // RUN: %diff "%s.expect" "%t" -// RUN: %OutputCheck --file-to-check "%S/TestedExterns.cs" "%s" +// RUN: %OutputCheck --file-to-check "%S/TestedExterns.legacy.cs" "%s" // CHECK-NOT: .*Foo____dafny__checked\(x\).* // CHECK: .*Foo____dafny__checked\(new BigInteger\(3\)\).* // CHECK-NOT: .*Bar____dafny__checked\(x\).* diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy.expect similarity index 85% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy.expect index f247ee2efd..33db6e1df8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy.expect @@ -2,7 +2,7 @@ Dafny program verifier finished with 0 verified, 0 errors CheckExtern.dfy(20,13): Warning: The requires clause at this location cannot be compiled to be tested at runtime because it references ghost state. CheckExtern.dfy(22,12): Warning: The ensures clause at this location cannot be compiled to be tested at runtime because it references ghost state. -TestedExterns.dfy(10,17): Warning: No :test code calls NotCalled +TestedExterns.legacy.dfy(10,17): Warning: No :test code calls NotCalled FooTest: FAILED CheckExtern.dfy(3,12): Runtime failure of ensures clause from CheckExtern.dfy(3,12) BarTest: FAILED @@ -15,5 +15,5 @@ GenMethodTest: FAILED CheckExtern.dfy(59,13): Runtime failure of requires clause from CheckExtern.dfy(59,13) BazTest: PASSED CallFunctionByMethod: PASSED -[Program halted] TestedExterns.dfy(8,0): Test failures occurred: see above. +[Program halted] TestedExterns.legacy.dfy(8,0): Test failures occurred: see above. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.externs.cs b/Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy.externs.cs similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.dfy.externs.cs rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/contract-wrappers/TestedExterns.legacy.dfy.externs.cs diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInit.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInit.dfy index b7d37fc63f..e1b6e8b30f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInit.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInit.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /print:"%t.print" /rprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %verify "%s" > "%t" // RUN: %diff "%s.expect" "%t" method M0(d: int) @@ -90,7 +90,7 @@ method Q1(s: D, n: int) returns (a: array) method QCaller() { - var s: Six; + var s: Six := *; var a := Q0(s, 217); var b := Q1(s, 2); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInitERR.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInitERR.dfy index b7d37fc63f..e1b6e8b30f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInitERR.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInitERR.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /print:"%t.print" /rprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %verify "%s" > "%t" // RUN: %diff "%s.expect" "%t" method M0(d: int) @@ -90,7 +90,7 @@ method Q1(s: D, n: int) returns (a: array) method QCaller() { - var s: Six; + var s: Six := *; var a := Q0(s, 217); var b := Q1(s, 2); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInitResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInitResolution.dfy index 216cd8bae6..a63923e7eb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInitResolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ArrayElementInitResolution.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /print:"%t.print" /rprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 2 %verify "%s" > "%t" // RUN: %diff "%s.expect" "%t" module AM { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-SimplifiedExpanded-Resolve.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-SimplifiedExpanded-Resolve.dfy index d0fc9cca20..86fd6423aa 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-SimplifiedExpanded-Resolve.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AsIs-SimplifiedExpanded-Resolve.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /typeSystemRefresh:1 /generalTraits:datatype /generalNewtypes:1 "%s" > "%t" +// RUN: %exits-with 2 %verify --type-system-refresh --general-traits=datatype --general-newtypes "%s" > "%t" // RUN: %diff "%s.expect" "%t" method IsBasicTypes(a0: bool, a1: char, a2: int, a3: bv7, a4: bv13, a5: ORDINAL, a6: real) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ByMethodResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ByMethodResolution.dfy index 2866fdf475..bea6843f60 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ByMethodResolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ByMethodResolution.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %verify "%s" > "%t" // RUN: %diff "%s.expect" "%t" module Resolution { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CompilationErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CompilationErrors.dfy index 4fa2996728..d246666961 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CompilationErrors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CompilationErrors.dfy @@ -1,8 +1,8 @@ -// RUN: %exits-with 3 %dafny /allowAxioms:0 "%s" > "%t" +// RUN: %exits-with 3 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" -type MyType // compile error: abstract type -iterator Iter() // compile error: body-less iterator +type MyType +iterator Iter() ghost method M() ensures false // compile error: body-less ghost method method P() ensures false // compile error: body-less method class TestClass { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiamondImports.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiamondImports.dfy index 933de66c14..038ddc1ee2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiamondImports.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DiamondImports.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %verify "%s" --relax-definite-assignment > "%t" // RUN: %diff "%s.expect" "%t" module ImportByName { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypesModuleExports.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypesModuleExports.dfy index 8ef104a02e..5caedcc7d3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypesModuleExports.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/EqualityTypesModuleExports.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /rprint:"%t.rprint" "%s" > "%t" +// RUN: %exits-with 2 %verify "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This module contains checks that (==) types are inferred and required as they should. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ErrorsInRelatedModules.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ErrorsInRelatedModules.dfy index 75f0907ccb..183a88bae3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ErrorsInRelatedModules.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ErrorsInRelatedModules.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 2 %verify "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This file gives some regression tests, where Dafny once had crashed when an imported module diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForLoops-Resolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForLoops-Resolution.dfy index 8370f33ff6..de18a83c95 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForLoops-Resolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForLoops-Resolution.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %verify "%s" > "%t" // RUN: %diff "%s.expect" "%t" module Tests { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.legacy.dfy similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.legacy.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.legacy.dfy.expect similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.dfy.expect rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ForallCompilation.legacy.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy index f71b678223..f48444bef0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 2 %dafny /typeSystemRefresh:1 /generalTraits:datatype /generalNewtypes:0 "%s" > "%t" -// RUN: %exits-with 2 %dafny /typeSystemRefresh:1 /generalTraits:datatype /generalNewtypes:1 "%s" >> "%t" +// RUN: %exits-with 2 %build --type-system-refresh --general-traits datatype --general-newtypes false "%s" > "%t" +// RUN: %exits-with 2 %build --type-system-refresh --general-traits datatype --general-newtypes true "%s" >> "%t" // RUN: %diff "%s.expect" "%t" module VariousBaseTypes { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeVerify.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeVerify.dfy index 57ea63f98c..a848c77e64 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeVerify.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeVerify.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /typeSystemRefresh:1 /generalNewtypes:1 "%s" > "%t" +// RUN: %exits-with 4 %build --type-system-refresh true --general-newtypes true --relax-definite-assignment "%s" > "%t" // RUN: %diff "%s.expect" "%t" module EmptyBool { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostAllocations-Resolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostAllocations-Resolution.dfy index 63edbcc132..82f164f6d3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostAllocations-Resolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostAllocations-Resolution.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" // ------- A constructor-less class can be allocated as either ghost or non-ghost diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostGuards.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostGuards.dfy index 78f49e644d..dcd0f424b4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostGuards.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostGuards.dfy @@ -1,5 +1,4 @@ -// NONUNIFORM: need to add support for tooltips to the new CLI (if that makes sense) -// RUN: %dafny /compile:3 /printTooltips "%s" > "%t" +// RUN: %verify --show-inference --relax-definite-assignment "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype Dt = Green | Dog diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostGuards.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostGuards.dfy.expect index e21d6f3470..8bb8a71d69 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostGuards.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GhostGuards.dfy.expect @@ -1,7 +1,7 @@ -GhostGuards.dfy(13,9): Info: ghost if -GhostGuards.dfy(19,2): Info: ghost if -GhostGuards.dfy(29,2): Info: ghost while -GhostGuards.dfy(42,2): Info: ghost while -GhostGuards.dfy(55,2): Info: ghost match +GhostGuards.dfy(12,9): Info: ghost if +GhostGuards.dfy(18,2): Info: ghost if +GhostGuards.dfy(28,2): Info: ghost while +GhostGuards.dfy(41,2): Info: ghost while +GhostGuards.dfy(54,2): Info: ghost match Dafny program verifier finished with 1 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JavaUseRuntimeLib.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JavaUseRuntimeLib.dfy index 244e310be9..bb108d3f9c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JavaUseRuntimeLib.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/JavaUseRuntimeLib.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny "%s" /useRuntimeLib /out:%S/Output/DafnyConsole.jar /compileTarget:java > "%t" +// RUN: %dafny "%s" /useRuntimeLib /out:%S/Output/DafnyConsole.jar /compileTarget java > "%t" // RUN: java -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Output/DafnyConsole.jar DafnyConsole >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAsserts.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAsserts.dfy index cc9f45c131..39a424ce3e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAsserts.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAsserts.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" class C { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy index e20225e520..a92da5fd06 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/LabeledAssertsResolution.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" module ResolutionTests { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/MapMergeSubtraction.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/MapMergeSubtraction.dfy index 07b7a8f1d3..da033795d8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/MapMergeSubtraction.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/MapMergeSubtraction.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Simple(m: map, n: map, s: set) returns (r: map) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/MiscTypeInferenceTests.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/MiscTypeInferenceTests.dfy index 0b9b22f260..1e2ca7fc23 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/MiscTypeInferenceTests.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/MiscTypeInferenceTests.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny "%s" > "%t" +// RUN: %exits-with 4 %build "%s" --relax-definite-assignment --allow-axioms > "%t" // RUN: %diff "%s.expect" "%t" // All of the examples in this file should type check (but some produce diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ModuleInsertion.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ModuleInsertion.dfy index 75d77035a3..a0c774722c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ModuleInsertion.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ModuleInsertion.dfy @@ -1,6 +1,6 @@ // NONUNIFORM: Tests printing much more than compilation -// RUN: %dafny /env:0 /dprint:- /dafnyVerify:0 "%s" > "%t" -// RUN: %dafny /env:0 /rprint:- /compile:3 "%s" >> "%t" +// RUN: %build --print:- --no-verify "%s" > "%t" +// RUN: %run --rprint:- "%s" >> "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ModuleInsertion.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ModuleInsertion.dfy.expect index 8a3ec5308e..047de96e16 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ModuleInsertion.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ModuleInsertion.dfy.expect @@ -104,6 +104,8 @@ module U.V { module U.V.W { const x1 := 12 * X.x0 } + +Dafny program verifier did not attempt verification // ModuleInsertion.dfy /* diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy index 9c5a04bf83..b331acd03d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/NativeTypeResolution.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /printTooltips /compileTarget:cs "%s" > "%t" +// RUN: %exits-with 2 %build --show-inference --target cs "%s" > "%t" // RUN: %diff "%s.expect" "%t" newtype V = x | 0 <= x < 200 // byte diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Newtypes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Newtypes.dfy index 6a0e8bbc0a..ea451650a3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Newtypes.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Newtypes.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %build "%s" --relax-definite-assignment > "%t" // RUN: %diff "%s.expect" "%t" newtype int32 = int @@ -88,7 +88,7 @@ module PredicateTests { } method N() { - var y: char8; + var y: char8 := *; if * { y := y / 2; y := y + 1; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParameterResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParameterResolution.dfy index bc07ac6688..ec6412bfeb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParameterResolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ParameterResolution.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" /dprint:"%t.dprint" > "%t" +// RUN: %exits-with 2 %build "%s" --allow-axioms > "%t" // RUN: %diff "%s.expect" "%t" module Actuals { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy index c8b35acf2b..76911f0b87 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrettyPrinting.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 2 %dafny /env:0 /dprint:- /noVerify "%s" > "%t" -// RUN: %exits-with 2 %dafny /env:0 /dprint:- /noVerify /typeSystemRefresh:1 "%s" > "%t.refresh" +// RUN: %exits-with 2 %build --print:- --no-verify "%s" > "%t" +// RUN: %exits-with 2 %build --print:- --no-verify --type-system-refresh "%s" > "%t.refresh" // RUN: %diff "%s.expect" "%t" // RUN: %diff "%s.expect" "%t.refresh" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrintEffectsResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrintEffectsResolution.dfy index bb014114b8..283191308e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrintEffectsResolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/PrintEffectsResolution.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 2 %dafny /compile:3 "%s" > "%t" -// RUN: %exits-with 2 %dafny /compile:3 /trackPrintEffects:1 "%s" >> "%t" +// RUN: %exits-with 2 %run "%s" > "%t" +// RUN: %exits-with 2 %run --track-print-effects "%s" >> "%t" // RUN: %diff "%s.expect" "%t" // The errors in this file are produced regardless of /trackPrintEffects setting. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/QuantificationNewSyntaxResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/QuantificationNewSyntaxResolution.dfy index 5ef3034b88..bad392cf9f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/QuantificationNewSyntaxResolution.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/QuantificationNewSyntaxResolution.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" module {:options "/quantifierSyntax:4"} NewSyntax { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests1.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests1.dfy index 79dbeb3e1c..71ebb859fe 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests1.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests1.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /compile:3 "%s" > "%t" +// RUN: %exits-with 2 %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" // The code in this file demonstrates how correct compilation of some features diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests2.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests2.dfy index c2776a83aa..6ce6420a78 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests2.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/RuntimeTypeTests2.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 3 %dafny /compile:3 "%s" /compileTarget:cs > "%t" +// RUN: %exits-with 3 %run "%s" --target cs > "%t" // RUN: %diff "%s.expect" "%t" // The errors in this file are produced by the compiler diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Simple.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Simple.dfy index b37c6d2758..d9f0e50d1f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Simple.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Simple.dfy @@ -1,5 +1,5 @@ -// RUN: %dafny /env:0 /dprint:- /noVerify "%s" > "%t" -// RUN: %dafny /env:0 /dprint:- /noVerify /typeSystemRefresh:1 "%s" > "%t.refresh" +// RUN: %resolve --allow-warnings --print:- "%s" > "%t" +// RUN: %resolve --allow-warnings --print:- --type-system-refresh "%s" > "%t.refresh" // RUN: %diff "%s.expect" "%t" // RUN: %diff "%s.expect" "%t.refresh" // My first Dafny program diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy index 7e46f921de..0e7e8a516a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /print:"%t.print" "%s" > "%t" +// RUN: %exits-with 4 %build "%s" --relax-definite-assignment --allow-axioms > "%t" // RUN: %diff "%s.expect" "%t" module AssignmentToNat { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypesERR.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypesERR.dfy index 9ef8b32bfa..cb500b5120 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypesERR.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypesERR.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /print:"%t.print" "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" module AssignmentsFromNewAllocation { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy index badb0d1ec6..bff60008fc 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy.expect index 6e44d6b503..d0d8f3462d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy.expect @@ -20,6 +20,7 @@ Twostate-Verification.dfy(679,22): Warning: Argument to 'old' does not dereferen Twostate-Verification.dfy(680,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect Twostate-Verification.dfy(681,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect Twostate-Verification.dfy(682,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(189,23): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning Twostate-Verification.dfy(33,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect Twostate-Verification.dfy(313,38): Error: assertion might not hold Twostate-Verification.dfy(337,23): Error: a precondition for this call could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConstraints.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConstraints.dfy index 4b33623216..db6404ba63 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConstraints.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConstraints.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /env:0 /rprint:- "%s" > "%t" +// RUN: %exits-with 2 %build --rprint:- "%s" > "%t" // RUN: %diff "%s.expect" "%t" module Tests { class CC { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConstraintsRefresh.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConstraintsRefresh.dfy index 2b73552d34..109e8f58f6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConstraintsRefresh.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/TypeConstraintsRefresh.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /typeSystemRefresh:1 "%s" > "%t" +// RUN: %exits-with 2 %build --type-system-refresh "%s" > "%t" // RUN: %diff "%s.expect" "%t" module Tests { class CC { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SnapshotableTrees.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SnapshotableTrees.dfy index 6e30255ef1..ee0308e3f6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SnapshotableTrees.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/SnapshotableTrees.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /compile:3 /proverOpt:O:smt.qi.eager_threshold=80 /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %run --solver-option="O:smt.qi.eager_threshold=80" "%s" > "%t" // re-enable the following before long // %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/Z-BirthdayBook.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/Z-BirthdayBook.dfy index 5f838ac0d2..c7e4e8f9ec 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/Z-BirthdayBook.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny2/Z-BirthdayBook.dfy @@ -1,5 +1,5 @@ // NONUNIFORM: https://github.com/dafny-lang/dafny/issues/4108 -// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" // The birthday book example from the Z Reference Manual diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug62.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug62.dfy index e6e57c9c9e..8afa77def8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug62.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug62.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 3 %dafny /compile:3 "%s" > "%t" +// RUN: %exits-with 3 %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" class C { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug88.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug88.dfy index e1dd95fc42..59e1601010 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug88.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug88.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny "%s" > "%t" +// RUN: %exits-with 4 %build "%s" --relax-definite-assignment > "%t" // RUN: %diff "%s.expect" "%t" lemma T(a: int) returns (b: int) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression11.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression11.dfy index c8a3cbd165..787b49c61e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression11.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression11.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /rprint:"%t.rprint" "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Once upon a time, several of these would crash the resolver after it had reported diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression12.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression12.dfy index 0d9cdda914..9da1016ad5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression12.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression12.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny "%s" > "%t" +// RUN: %exits-with 4 %build --relax-definite-assignment "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Some tests for the type inference that was revamped diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression15.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression15.dfy index c5f3de710d..508850dc5e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression15.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Regression15.dfy @@ -1,5 +1,5 @@ // NONUNIFORM: https://github.com/dafny-lang/dafny/issues/4108 -// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %run --relax-definite-assignment "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue167.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue167.dfy index 7dd835b3f8..cc3c0bf9fa 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue167.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue167.dfy @@ -1,5 +1,5 @@ // NONUNIFORM: https://github.com/dafny-lang/dafny/issues/4108 -// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue228.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue228.dfy index a3357958c0..acd46d458e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue228.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue228.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 4 %dafny /env:0 /dprint:- "%s" > "%t" -// RUN: %exits-with 4 %dafny /env:0 /rprint:- "%s" >> "%t" +// RUN: %exits-with 4 %build --print:- "%s" --relax-definite-assignment > "%t" +// RUN: %exits-with 4 %build --rprint:- "%s" --relax-definite-assignment >> "%t" // RUN: %diff "%s.expect" "%t" // Tests the pretty printing of + and * diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfy similarity index 80% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfy index 5a01793813..6046871520 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfy @@ -1,7 +1,7 @@ // RUN: %exits-with 4 %dafny /tracePOs /compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -include "git-issue59.dfyi" +include "git-issue59.legacy.dfyi" method foo(x:byte) { var y:byte := x+1; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfy.expect similarity index 56% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.dfy.expect rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfy.expect index 3204e9e1f0..600aed809a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfy.expect @@ -1,6 +1,6 @@ Verifying foo (correctness) ... [1 proof obligation] error -git-issue59.dfy(7,17): Error: value does not satisfy the subset constraints of 'byte' +git-issue59.legacy.dfy(7,17): Error: value does not satisfy the subset constraints of 'byte' Dafny program verifier finished with 0 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.dfyi b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfyi similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.dfyi rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue59.legacy.dfyi diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue70.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue70.dfy index b7297cd9e2..0d8bef888a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue70.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/git-issue70.dfy @@ -1,5 +1,5 @@ // NONUNIFORM: https://github.com/dafny-lang/dafny/issues/4108 -// RUN: %dafny /compile:3 "%s" > "%t" +// RUN: %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Main() diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/standardLibraryOptionMismatch.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/standardLibraryOptionMismatch.dfy index 884977f714..926598b065 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/standardLibraryOptionMismatch.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/standardLibraryOptionMismatch.dfy @@ -1,4 +1,4 @@ -// RUN: %translate cs %s --standard-libraries --unicode-char=false > "%t" +// RUN: %translate cs --unicode-char false --standard-libraries true %s &> "%t" // RUN: %diff "%s.expect" "%t" method Foo() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/standardLibraryOptionMismatch.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/standardLibraryOptionMismatch.dfy.expect index 40aa49a098..a0990cf70f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/standardLibraryOptionMismatch.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/standardLibraryOptionMismatch.dfy.expect @@ -1,4 +1,4 @@ -CLI: Error: cannot load /DafnyStandardLibraries-cs.doo: --unicode-char is set locally to False, but the library was built with True -CLI: Error: cannot load /DafnyStandardLibraries.doo: --unicode-char is set locally to False, but the library was built with True +CLI: Error: cannot load DafnyStandardLibraries-cs.doo: --unicode-char is set locally to False, but the library was built with True +CLI: Error: cannot load DafnyStandardLibraries.doo: --unicode-char is set locally to False, but the library was built with True Dafny program verifier finished with 0 verified, 0 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/Compiler.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/Compiler.dfy index 9e808ab3d8..207f037f11 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/Compiler.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/Compiler.dfy @@ -1,5 +1,5 @@ // RUN: cp %S/Simple.g4 %S/csharp/Simple.g4 -// RUN: %dafny -compile:0 -unicodeChar:0 -spillTargetCode:3 "-out:%S/csharp/Compiler.cs" "%s" +// RUN: %translate cs --include-runtime --unicode-char false --output:%S/csharp/Compiler.cs "%s" // RUN: dotnet run --project %S/csharp/SimpleCompiler.csproj -- %S/example_input.calc > "%t" // RUN: %diff "%s.expect" "%t" @@ -237,7 +237,7 @@ module StackMachine { } } - const EmptyState := State(Nil, map[], []); + const EmptyState := State(Nil, map[], []) function interpProg(p: Prog, input: RegisterFile) : seq { interpProg'(p, EmptyState.(regs := input)).output @@ -461,7 +461,7 @@ module {:extern "SimpleCompiler.CSharpAST"} CSharpAST { } trait {:compile false} {:extern} Assign extends Stmt { - var v: System.String; + var v: System.String var e: Expr } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy index d0fb2f92db..f9e1d10dc8 100755 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy @@ -316,5 +316,7 @@ module {:options "-functionSyntax:4"} Parsers { /// } /// ``` -// RUN: %exits-with 4 %dafny -compile:4 "%s" --args "((()))" "((()))no" "((())" > "%t" +// NONUNIFORM: testDafnyForEachCompiler does not support program argument +// RUN: %exits-with 4 %verify "%s" > "%t" +// RUN: %run --no-verify "%s" "((()))" "((()))no" "((())" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy.expect index 463e63c293..0e95cee245 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/parser_combinators.dfy.expect @@ -2,6 +2,8 @@ parser_combinators.dfy(38,27): Error: cannot use naked function in recursive set parser_combinators.dfy(39,33): Error: cannot prove termination; try supplying a decreases clause Dafny program verifier finished with 8 verified, 2 errors + +Dafny program verifier did not attempt verification "((()))": 3 nested parentheses "((()))no": no valid parse "((())": no valid parse diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TestAttributeErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TestAttributeErrors.dfy index 30dccb434a..a8b8dccebd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TestAttributeErrors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TestAttributeErrors.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 3 %dafny "%s" > "%t" +// RUN: %exits-with 3 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" include "../exceptions/VoidOutcomeDt.dfy" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy index aaa8d8024e..bd20d9f503 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy @@ -1,7 +1,7 @@ -// RUN: ! %dafny /compile:3 /compileTarget:cs /unicodeChar:0 "%s" > "%t" -// RUN: ! %dafny /compile:3 /compileTarget:go /unicodeChar:0 "%s" >> "%t" -// RUN: ! %dafny /compile:3 /compileTarget:java /unicodeChar:0 "%s" >> "%t" -// RUN: ! %dafny /compile:3 /compileTarget:js /unicodeChar:0 "%s" >> "%t" +// RUN: ! %run --target cs --unicode-char false "%s" > "%t" +// RUN: ! %run --target go --unicode-char false "%s" >> "%t" +// RUN: ! %run --target java --unicode-char false "%s" >> "%t" +// RUN: ! %run --target js --unicode-char false "%s" >> "%t" // RUN: %diff "%s.expect" "%t" include "../exceptions/NatOutcomeDt.dfy" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectWithMessage.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectWithMessage.dfy index afe2e1806b..ce7b6675ab 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectWithMessage.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectWithMessage.dfy @@ -1,7 +1,7 @@ -// RUN: ! %dafny /compile:3 /compileTarget:cs "%s" > "%t" -// RUN: ! %dafny /compile:3 /compileTarget:go "%s" >> "%t" -// RUN: ! %dafny /compile:3 /compileTarget:java "%s" >> "%t" -// RUN: ! %dafny /compile:3 /compileTarget:js "%s" >> "%t" +// RUN: ! %run --target cs "%s" > "%t" +// RUN: ! %run --target go "%s" >> "%t" +// RUN: ! %run --target java "%s" >> "%t" +// RUN: ! %run --target js "%s" >> "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectWithNonStringMessage.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectWithNonStringMessage.dfy index b45cb0a5e1..cb01702e50 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectWithNonStringMessage.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectWithNonStringMessage.dfy @@ -1,9 +1,9 @@ // RUN: %verify --unicode-char false "%s" > "%t" -// RUN: ! %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:cs "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:go "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:java "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:js "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:py "%s" >> "%t" +// RUN: ! %run --no-verify --unicode-char false --target cs "%s" >> "%t" +// RUN: ! %run --no-verify --unicode-char false --target go "%s" >> "%t" +// RUN: ! %run --no-verify --unicode-char false --target java "%s" >> "%t" +// RUN: ! %run --no-verify --unicode-char false --target js "%s" >> "%t" +// RUN: ! %run --no-verify --unicode-char false --target py "%s" >> "%t" // RUN: %diff "%s.expect" "%t" datatype Option = None | Some(get: T) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportRefinement.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportRefinement.dfy index fd34c4864e..0be60f13bb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportRefinement.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportRefinement.dfy @@ -1,7 +1,7 @@ // NONUNIFORM: Multiple testing scenarios (could be split) -// RUN: %dafny /env:0 /compile:3 /dprint:"%t.dfy" "%s" > "%t.result" -// RUN: %dafny /env:0 /printMode:DllEmbed /dprint:"%t1.dfy" "%t.dfy" -// RUN: %dafny /env:0 /printMode:DllEmbed /dprint:"%t2.dfy" /compile:3 "%t1.dfy" > "%t" +// RUN: %run --print:"%t.dfy" "%s" &> "%t.result" +// RUN: %build --print-mode Serialization --print:"%t1.dfy" "%t.dfy" &> "%t" +// RUN: %run --print-mode Serialization --print:"%t2.dfy" "%t1.dfy" &>> "%t" // RUN: %diff "%t1.dfy" "%t2.dfy" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportRefinement.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportRefinement.dfy.expect index 4c28d2a1aa..56529cadb4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportRefinement.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportRefinement.dfy.expect @@ -1,4 +1,6 @@ +Dafny program verifier finished with 2 verified, 0 errors + Dafny program verifier finished with 2 verified, 0 errors A2 B2.m() diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportResolve.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportResolve.dfy index 426e7f0777..df42866061 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportResolve.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportResolve.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" module NamesThatDontExist { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportVerify.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportVerify.dfy index b13669202a..8a10bbb047 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportVerify.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/ExportVerify.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" module Lib { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/xrefine1.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/xrefine1.dfy index ede328a092..87fc521b5c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/xrefine1.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/exports/xrefine1.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1005.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1005.dfy index b12de83f9c..b890fec043 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1005.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1005.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype S0 = S0() diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1074.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1074.dfy index ea8b7e0ad5..1599ecb4f0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1074.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1074.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compileVerbose:1 /compile:1 "%s" > "%t" +// RUN: %build --verbose "%s" > "%t" // RUN: %diff "%s.expect" "%t" module A { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1111.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1111.dfy index cd1743c196..e3644a1081 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1111.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1111.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compileTarget:java "%s" > "%t" +// RUN: %build --target java "%s" > "%t" // RUN: %diff "%s.expect" "%t" module Foo { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1129.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1129.dfy index 2d0a3ba7fa..7cf71717f6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1129.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1129.dfy @@ -1,10 +1,10 @@ // NONUNIFORM: Program expected to fail in backend-specific ways // RUN: %verify "%s" > "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:cs "%s" > "%t".abyss -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:java "%s" > "%t".abyss -// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" > "%t".abyss -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:go "%s" > "%t".abyss -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:cpp "%s" > "%t".abyss +// RUN: %exits-with 3 %run --no-verify --target cs "%s" > "%t".abyss +// RUN: %exits-with 3 %run --no-verify --target java "%s" > "%t".abyss +// RUN: %run --no-verify --target js "%s" > "%t".abyss +// RUN: %exits-with 3 %run --no-verify --target go "%s" > "%t".abyss +// RUN: %exits-with 3 %run --no-verify --target cpp "%s" > "%t".abyss // RUN: %diff "%s.expect" "%t" // Without providing extern code for the :extern C, Dafny will output diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1151-more.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1151-more.dfy index 6f1e53888c..b8d81ad96d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1151-more.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1151-more.dfy @@ -1,10 +1,10 @@ // RUN: %verify --relax-definite-assignment --unicode-char false "%s" > "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:cs "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:java "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:js "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:go "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:cpp "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /unicodeChar:0 /compileTarget:py "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --unicode-char false --target cs "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --unicode-char false --target java "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --unicode-char false --target js "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --unicode-char false --target go "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --unicode-char false --target cpp "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --unicode-char false --target py "%s" >> "%t" // RUN: %diff "%s.expect" "%t" // The following example should produce a compilation error, since there's diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1151.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1151.dfy index b58b4f21d1..3211026d9b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1151.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1151.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 "%s" %S/git-issue-1151-concrete.cs > "%t" +// RUN: %run "%s" --relax-definite-assignment --input %S/git-issue-1151-concrete.cs > "%t" // RUN: %diff "%s.expect" "%t" module {:extern "M"} M { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1172.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1172.dfy index 5b641a3e65..d4b338bd9c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1172.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1172.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /compile:3 "%s" > "%t" +// RUN: %exits-with 2 %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" // The following examples show that verification would be unsound if ghost methods would diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1199.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1199.dfy index 50c1a5c92c..d1ea43716f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1199.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1199.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:1 /compileTarget:cs "%s" %S/git-issue-1199-extern.cs > "%t" +// RUN: %build "%s" %S/git-issue-1199-extern.cs > "%t" // RUN: %diff "%s.expect" "%t" module {:extern "Microsoft"} Microsoft { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1212.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1212.dfy index 1706050c00..3807479488 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1212.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1212.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /compile:3 "%s" > "%t" +// RUN: %exits-with 4 %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" trait H { var data: Y } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1229.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1229.dfy index 192f14ae3c..8191b8a6e1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1229.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1229.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:1 /compileTarget:cs "%s" %S/git-issue-1229-extern.cs > "%t" +// RUN: %build "%s" %S/git-issue-1229-extern.cs > "%t" // RUN: %diff "%s.expect" "%t" module {:extern "MyModule2"} MyModule2 { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1248.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1248.dfy index 3080aaa2d7..4435df3cee 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1248.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1248.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny "%s" > "%t" +// RUN: %exits-with 4 %build "%s" > "%t" // RUN: %exits-with 4 %dafny /arith:10 "%s" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1256.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1256.dfy index 4ee798cdd0..b952c42bc3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1256.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1256.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny "%s" > "%t" +// RUN: %exits-with 4 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" ghost function f(): X diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1377.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1377.dfy index c45ca76284..8012494cb7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1377.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1377.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /compile:3 "%s" > "%t" +// RUN: %exits-with 2 %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" class Cell { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1419.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1419.dfy index b83e54065a..d6a34979e3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1419.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1419.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /compile:4 /compileTarget:cs "%s" > "%t" +// RUN: %exits-with 2 %run --target cs "%s" > "%t" // RUN: %diff "%s.expect" "%t" module FromBugReport { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1604c.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1604c.dfy index 82d4c04784..77b0e02a72 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1604c.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1604c.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /compile:1 /errorLimit:0 "%s" > "%t" +// RUN: %exits-with 4 %build --error-limit 0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" ghost predicate EvenNat(n: nat) { n % 2 == 0 } ghost predicate TrueInt(x: int) { true } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1619.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1619.dfy index 2966be7e14..e86deab782 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1619.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1619.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny "%s" > "%t" +// RUN: %exits-with 4 %build "%s" --relax-definite-assignment --allow-axioms > "%t" // RUN: %diff "%s.expect" "%t" predicate {:opaque} P(w: W) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1731.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1731.dfy index b3409be332..c9d9ccb6d6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1731.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1731.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /typeSystemRefresh:1 "%s" > "%t" +// RUN: %build --type-system-refresh "%s" > "%t" // RUN: %diff "%s.expect" "%t" module PreviouslyAProblem { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1762.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1762.dfy index 2356ef40e8..67c46e3013 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1762.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1762.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 "%s" %S/git-issue-1761-extern.cs > "%t" +// RUN: %run "%s" --input %S/git-issue-1761-extern.cs > "%t" // RUN: %diff "%s.expect" "%t" class {:extern "ABC"} XYZ { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-179.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-179.dfy index cf295ede37..3a26f3f5e0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-179.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-179.dfy @@ -1,9 +1,9 @@ // NONUNIFORM: https://github.com/dafny-lang/dafny/issues/4108 // RUN: %verify --relax-definite-assignment "%s" > "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" +// RUN: %run --no-verify --target cs "%s" >> "%t" +// RUN: %run --no-verify --target js "%s" >> "%t" +// RUN: %run --no-verify --target go "%s" >> "%t" +// RUN: %run --no-verify --target java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1887.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1887.dfy index 4fec96a720..1a000986fd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1887.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-1887.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" function selectOneConstraint(s: seq): seq { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2071.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2071.dfy index 535116c243..773732a1ec 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2071.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2071.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:1 /spillTargetCode:2 /compileTarget:java "%s" > "%t" +// RUN: %translate java "%s" > "%t" // RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/git-issue-2071-java %S/git-issue-2071-java/git_issue_2071.java %S/git-issue-2071-java/*/*.java >> "%t" // RUN: java -ea -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/git-issue-2071-java git_issue_2071 >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2134.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2134.dfy index d51222bec4..f1ba492310 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2134.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2134.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /typeSystemRefresh:1 "%s" > "%t" +// RUN: %exits-with 2 %build --type-system-refresh "%s" > "%t" // RUN: %diff "%s.expect" "%t" module NewtypeCycle0 { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2216.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2216.dfy index 277af09736..9c5bf3d14a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2216.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2216.dfy @@ -1,5 +1,5 @@ // NONUNIFORM: Too slow on other backends -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" +// RUN: %run --no-verify --target cs "%s" >> "%t" const REPEAT := 100_000 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2726.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2726.dfy index be87be33b5..ff9cd3d4a6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2726.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2726.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:1 /compileTarget:cs "%s" > "%t" +// RUN: %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype Formula = diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2828.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2828.dfy index b7526139af..4a2e392af5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2828.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2828.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" method M() diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2852.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2852.dfy index 1879c7e211..9c5fae3f1b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2852.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2852.dfy @@ -1,5 +1,6 @@ -// RUN: %dafny -compile:3 -compileTarget:cs "%s" > "%t" -// RUN: %dafny -noVerify -compile:4 -compileTarget:js "%s" >> "%t" +// NONUNIFORM: regression test +// RUN: %run --target cs "%s" > "%t" +// RUN: %run --no-verify --target js "%s" >> "%t" // RUN: %diff "%s.expect" "%t" // Returns a function that computes the sum of n consecutive integers starting at pos diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2885.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2885.dfy index 2401aa08fc..6709485588 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2885.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2885.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:1 /compileTarget:cs "%s" > "%t" +// RUN: %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" datatype KeyValues = Store(underlying: map := map[]) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3273.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3273.dfy index 01ee9b2353..11ad0dfca6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3273.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3273.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" iterator Iter(u: set) // this infers Y to be (==) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3918.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3918.dfy index a340eb511b..61beea271e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3918.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3918.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" // The two errors below had previously slipped by the resolver, causing malformed compiled code. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3921.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3921.dfy index 9c9b334945..fad4fe6c05 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3921.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3921.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" module A { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3922.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3922.dfy index 14f3095d1a..abf30d9c57 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3922.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3922.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" module A { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3962.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3962.dfy index 3c027c2d66..a34f4da0fe 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3962.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3962.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /printTooltips "%s" > "%t" +// RUN: %exits-with 4 %build --show-inference "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Issues(a: bool, s: set) { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-403.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-403.dfy index b2c3f9d355..ce6e006b7a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-403.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-403.dfy @@ -1,4 +1,5 @@ -// RUN: %dafny -compile:4 -compileTarget:java "%s" > "%t" +// NONUNIFORM: nativeType has back-end specific behavior +// RUN: %run --target java "%s" > "%t" // RUN: %diff "%s.expect" "%t" newtype {:nativeType "byte"} uint8 = x:int | 0 <= x < 0x100 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4131.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4131.dfy index 1a30cd5996..087bf02ddd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4131.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4131.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /typeSystemRefresh:1 "%s" > "%t" +// RUN: %verify --type-system-refresh "%s" > "%t" // RUN: %diff "%s.expect" "%t" class Element { } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4162.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4162.dfy index 4c5fd03f68..84fc1d040a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4162.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4162.dfy @@ -1,9 +1,9 @@ // NONUNIFORM: %testDafnyForEachCompiler doesn't support /out -// RUN: %dafny /compile:4 /compileTarget:py /out:M "%s" > "%t" -// RUN: %dafny /compile:4 /compileTarget:cs /out:M "%s" >> "%t" -// RUN: %dafny /compile:4 /compileTarget:java /out:M "%s" >> "%t" -// RUN: %dafny /compile:4 /compileTarget:js /out:M "%s" >> "%t" -// RUN: %dafny /compile:4 /compileTarget:go /out:M "%s" >> "%t" +// RUN: %run --target py --build M "%s" > "%t" +// RUN: %run --target cs --build M "%s" >> "%t" +// RUN: %run --target java --build M "%s" >> "%t" +// RUN: %run --target js --build M "%s" >> "%t" +// RUN: %run --target go --build M "%s" >> "%t" // RUN: %diff "%s.expect" "%t" module M { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-448.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-448.dfy index ace17d6fe0..24cc2a514c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-448.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-448.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /compile:3 "%s" > "%t" +// RUN: %exits-with 4 %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" class C { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4724.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4724.dfy index ccf59ee20d..7768592ed0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4724.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4724.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /compile:0 "%s" > "%t" +// RUN: %exits-with 4 %verify "%s" > "%t" // RUN: %diff "%s.expect" "%t" type seq31 = x: seq | |x| <= 31 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-484.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-484.dfy index 61dcfa2c22..240bb45bd0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-484.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-484.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" newtype MyInt = int diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-495.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-495.dfy index a065790c2a..b23aaeed51 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-495.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-495.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny "%s" > "%t" +// RUN: %exits-with 4 %build "%s" --relax-definite-assignment > "%t" // RUN: %diff "%s.expect" "%t" datatype Dt = Make(d: int) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-555.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-555.dfy index c75e5602c6..f821897df8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-555.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-555.dfy @@ -1,8 +1,8 @@ // RUN: %exits-with 4 %verify "%s" > "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" +// RUN: ! %run --no-verify --target cs "%s" >> "%t" +// RUN: ! %run --no-verify --target js "%s" >> "%t" +// RUN: ! %run --no-verify --target go "%s" >> "%t" +// RUN: ! %run --no-verify --target java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-590.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-590.dfy index 9dfa672759..6de0506d46 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-590.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-590.dfy @@ -1,3 +1,3 @@ // dafny should emit exit value 1 -// RUN: ! %dafny /compile:3 x.cs > "%t" +// RUN: ! %run x.cs > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-633.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-633.dfy index a1f3bc82f9..32c02b441c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-633.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-633.dfy @@ -1,10 +1,10 @@ // NONUNIFORM: need to add support for --input when running to %testDafnyForEachCompiler // RUN: %verify "%s" %S/git-issue-633A.dfy > "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs /spillTargetCode:3 "%s" %S/git-issue-633A.dfy >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js /spillTargetCode:3 "%s" %S/git-issue-633A.dfy >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go /spillTargetCode:3 "%s" %S/git-issue-633A.dfy >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java /spillTargetCode:3 "%s" %S/git-issue-633A.dfy >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:py /spillTargetCode:3 "%s" %S/git-issue-633A.dfy >> "%t" +// RUN: %run --no-verify --target cs "%s" --input %S/git-issue-633A.dfy >> "%t" +// RUN: %run --no-verify --target js "%s" --input %S/git-issue-633A.dfy >> "%t" +// RUN: %run --no-verify --target go "%s" --input %S/git-issue-633A.dfy >> "%t" +// RUN: %run --no-verify --target java "%s" --input %S/git-issue-633A.dfy >> "%t" +// RUN: %run --no-verify --target py "%s" --input %S/git-issue-633A.dfy >> "%t" // RUN: %diff "%s.expect" "%t" method m() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-643.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-643.dfy index 84e9aca5c4..e263748461 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-643.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-643.dfy @@ -1,8 +1,8 @@ // RUN: %verify "%s" > "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" +// RUN: ! %run --no-verify --target cs "%s" >> "%t" +// RUN: ! %run --no-verify --target java "%s" >> "%t" +// RUN: ! %run --no-verify --target js "%s" >> "%t" +// RUN: ! %run --no-verify --target go "%s" >> "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-643a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-643a.dfy index 6b5a304917..bbdb84edb7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-643a.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-643a.dfy @@ -1,8 +1,8 @@ // RUN: %verify "%s" > "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" +// RUN: ! %run --no-verify --target cs "%s" >> "%t" +// RUN: ! %run --no-verify --target java "%s" >> "%t" +// RUN: ! %run --no-verify --target js "%s" >> "%t" +// RUN: ! %run --no-verify --target go "%s" >> "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-663.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-663.dfy index 3854768e56..2609e32fb9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-663.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-663.dfy @@ -1,4 +1,4 @@ -// RUN: ! %dafny /compile:1 /allowAxioms:0 /warningsAsErrors "%s" > "%t" +// RUN: ! %build "%s" &> "%t" // RUN: %diff "%s.expect" "%t" method StatementsInCompiledMethod() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-666.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-666.dfy index 583bb982b9..e438b0765f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-666.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-666.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" trait O { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697c.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697c.dfy index da9dbc3155..2ebb178d65 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697c.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-697c.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /compile:3 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %exits-with 2 %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" ghost function ghostPredicate(x: int): bool { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-755.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-755.dfy index 098331005a..2d52ee2c73 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-755.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-755.dfy @@ -1,9 +1,9 @@ // NONUNIFORM: https://github.com/dafny-lang/dafny/issues/4108 // RUN: %verify "%s" > "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" +// RUN: %run --no-verify --target cs "%s" >> "%t" +// RUN: %run --no-verify --target js "%s" >> "%t" +// RUN: %run --no-verify --target go "%s" >> "%t" +// RUN: %run --no-verify --target java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-856.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-856.dfy index 4b1e2eb726..58001e80c9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-856.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-856.dfy @@ -1,8 +1,8 @@ // RUN: %verify "%s" > "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" +// RUN: ! %run --no-verify --target cs "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target js "%s" >> "%t" +// RUN: ! %run --no-verify --target go "%s" >> "%t" +// RUN: ! %run --no-verify --target java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" method Main() diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-889a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-889a.dfy index 265c50edf1..37f11d63a1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-889a.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-889a.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny "%s" > "%t" +// RUN: %exits-with 4 %build "%s" --relax-definite-assignment > "%t" // RUN: %diff "%s.expect" "%t" // This file includes verification tests diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-889b.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-889b.dfy index 824c29a573..5c115315e3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-889b.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-889b.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" // This file tests resolution errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-907.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-907.dfy index ed81c320ae..87b31b3f2a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-907.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-907.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:1 /compileTarget:java /spillTargetCode:1 "%s" > "%t" +// RUN: %translate java "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Checks that the Java runtime library is present diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main.dfy index 40d52f5bda..da38b911aa 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main.dfy @@ -1,8 +1,8 @@ // RUN: %verify "%s" > "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target cs "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target js "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target go "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" module A { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main0.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main0.dfy index db25bf631a..3179f489ef 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main0.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main0.dfy @@ -1,13 +1,13 @@ // NONUNIFORM: Multiple test scenarios (could be split) // RUN: %verify "%s" > "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs /Main:A.B.Main "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js /Main:A.B.Main "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go /Main:A.B.Main "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js /Main:A.B.Main "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs /Main:A.C.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js /Main:A.C.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go /Main:A.C.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java /Main:A.C.Test "%s" >> "%t" +// RUN: %run --no-verify --target cs --main-method A.B.Main "%s" >> "%t" +// RUN: %run --no-verify --target js --main-method A.B.Main "%s" >> "%t" +// RUN: %run --no-verify --target go --main-method A.B.Main "%s" >> "%t" +// RUN: %run --no-verify --target js --main-method A.B.Main "%s" >> "%t" +// RUN: %run --no-verify --target cs --main-method A.C.Test "%s" >> "%t" +// RUN: %run --no-verify --target js --main-method A.C.Test "%s" >> "%t" +// RUN: %run --no-verify --target go --main-method A.C.Test "%s" >> "%t" +// RUN: %run --no-verify --target java --main-method A.C.Test "%s" >> "%t" // RUN: %diff "%s.expect" "%t" module A { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main2.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main2.dfy index 781b698afc..ce6e6957a4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main2.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main2.dfy @@ -1,8 +1,8 @@ // RUN: %verify "%s" > "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target cs "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target js "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target go "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" module A { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main4.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main4.dfy index d180bfc4a2..e0fe49893e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main4.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-Main4.dfy @@ -1,29 +1,29 @@ // NONUNIFORM: Multiple test scenarios (could be split) // RUN: %verify "%s" > "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs /Main:A.AA.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js /Main:A.AA.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go /Main:A.AA.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java /Main:A.AA.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs /Main:B.C.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js /Main:B.C.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go /Main:B.C.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java /Main:B.C.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs /Main:B.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js /Main:B.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go /Main:B.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java /Main:B.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs /Main:Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js /Main:Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go /Main:Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java /Main:Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs /Main:C.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js /Main:C.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go /Main:C.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java /Main:C.Test "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:cs /Main:X "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:js /Main:X "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:go /Main:X "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:java /Main:X "%s" >> "%t" +// RUN: %run --no-verify --target cs --main-method A.AA.Test "%s" >> "%t" +// RUN: %run --no-verify --target js --main-method A.AA.Test "%s" >> "%t" +// RUN: %run --no-verify --target go --main-method A.AA.Test "%s" >> "%t" +// RUN: %run --no-verify --target java --main-method A.AA.Test "%s" >> "%t" +// RUN: %run --no-verify --target cs --main-method B.C.Test "%s" >> "%t" +// RUN: %run --no-verify --target js --main-method B.C.Test "%s" >> "%t" +// RUN: %run --no-verify --target go --main-method B.C.Test "%s" >> "%t" +// RUN: %run --no-verify --target java --main-method B.C.Test "%s" >> "%t" +// RUN: %run --no-verify --target cs --main-method B.Test "%s" >> "%t" +// RUN: %run --no-verify --target js --main-method B.Test "%s" >> "%t" +// RUN: %run --no-verify --target go --main-method B.Test "%s" >> "%t" +// RUN: %run --no-verify --target java --main-method B.Test "%s" >> "%t" +// RUN: %run --no-verify --target cs --main-method Test "%s" >> "%t" +// RUN: %run --no-verify --target js --main-method Test "%s" >> "%t" +// RUN: %run --no-verify --target go --main-method Test "%s" >> "%t" +// RUN: %run --no-verify --target java --main-method Test "%s" >> "%t" +// RUN: %run --no-verify --target cs --main-method C.Test "%s" >> "%t" +// RUN: %run --no-verify --target js --main-method C.Test "%s" >> "%t" +// RUN: %run --no-verify --target go --main-method C.Test "%s" >> "%t" +// RUN: %run --no-verify --target java --main-method C.Test "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target cs --main-method X "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target js --main-method X "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target go --main-method X "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target java --main-method X "%s" >> "%t" module A { module AA { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-MainE.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-MainE.dfy index 5df927611c..c6f35fe355 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-MainE.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-MainE.dfy @@ -1,20 +1,20 @@ // NONUNIFORM: Multiple test scenarios (could be split) // RUN: %verify --relax-definite-assignment "%s" > "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /Main:A.Test "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /Main:B.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:C.Test "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /Main:D.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:E.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:G.Test "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /Main:H.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:I.Test "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /Main:J.Test "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /Main:K.Test "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main: "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /Main:- "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /Main:Tr.Instance "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /Main:Opaque.Static "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /Main:Opaque.Instance "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --main-method A.Test "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --main-method B.Test "%s" >> "%t" +// RUN: %run --no-verify --main-method C.Test "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --main-method D.Test "%s" >> "%t" +// RUN: %run --no-verify --main-method E.Test "%s" >> "%t" +// RUN: %run --no-verify --main-method G.Test "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --main-method H.Test "%s" >> "%t" +// RUN: %run --no-verify --main-method I.Test "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --main-method J.Test "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --main-method K.Test "%s" >> "%t" + +// RUN: %run --no-verify --main-method=- "%s" &>> "%t" +// RUN: %exits-with 3 %run --no-verify --main-method Tr.Instance "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --main-method Opaque.Static "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --main-method Opaque.Instance "%s" >> "%t" // RUN: %diff "%s.expect" "%t" class A { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-MainE.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-MainE.dfy.expect index 54ebf05932..f965183af7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-MainE.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-MainE.dfy.expect @@ -37,9 +37,6 @@ Dafny program verifier did not attempt verification git-issue-MainE.dfy(50,9): Error: The method 'K.Test' is not permitted as a main method (the method has modifies clauses). Translation was aborted because errors were found -Dafny program verifier did not attempt verification -Main - Dafny program verifier did not attempt verification Dafny program verifier did not attempt verification diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-305-b.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-305-b.dfy index c8cb980f91..07ad8f636d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-305-b.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-305-b.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 3 %dafny /compile:0 /spillTargetCode:2 /useBaseNameForFileName "%s" > "%t" +// RUN: %exits-with 3 %translate cs --show-snippets=false "%s" > "%t" // RUN: %diff "%s".expect "%t" method hasNoBody() diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-305-c.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-305-c.dfy index 109105ad0c..f0d0a6e3d6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-305-c.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-305-c.dfy @@ -1,4 +1,4 @@ -// RUN: %baredafny /compile:0 /spillTargetCode:2 "%s" > "%t" +// RUN: %translate cs "%s" > "%t" // RUN: %diff "%s.expect" "%t" // At some point (https://github.com/dafny-lang/dafny/pull/307#issuecomment-510191495) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-305-c.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-305-c.dfy.expect index 7a0d776f0c..012f5b9937 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-305-c.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/github-issue-305-c.dfy.expect @@ -1,3 +1,2 @@ Dafny program verifier finished with 0 verified, 0 errors -Wrote textual form of target program to github-issue-305-c.cs diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy index b40f7a3e7b..a81ed26c22 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /print:"%t.print" "%s" > "%t" +// RUN: %exits-with 4 %build --allow-axioms "%s" > "%t" // RUN: %diff "%s.expect" "%t" @@ -51,7 +51,7 @@ method AllocationTest(oldcell: Cell) var j := (c: Cell, b) => if b then c else oldcell; var k := (c: Cell?, b) reads c, oldcell requires b ==> c != null => (if b then c else oldcell).data; - var b; + var b := *; if { case true => assert j(y, b).data < 50; case true => assert old(j(y, false).data) == 48; // error: argument y is not allocated in old state diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy index 93cf7e4d1d..71e24a1920 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy @@ -1,4 +1,5 @@ -// RUN: %exits-with 4 %dafny /compile:0 /tracePOs "%s" > "%t" +// RUN: %exits-with 4 %verify --cores 1 --progress "%s" > "%t".raw +// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t // RUN: %diff "%s.expect" "%t" // These tests make sure that the built-in arrow types are taken into account when diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect index 9ef977121c..0090517f56 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect @@ -1,26 +1,19 @@ - -Verifying CheckReads (well-formedness) ... - [3 proof obligations] errors -ArrowTypeOptimizations.dfy(10,2): Error: function precondition could not be proved -ArrowTypeOptimizations.dfy(10,2): Error: insufficient reads clause to invoke function - -Verifying CheckPre (well-formedness) ... - [2 proof obligations] error -ArrowTypeOptimizations.dfy(16,2): Error: function precondition could not be proved - -Verifying CheckReadsTot (well-formedness) ... - [1 proof obligation] verified - -Verifying CheckReadsParens (well-formedness) ... - [1 proof obligation] verified - -Verifying CheckReadsLambdaGeneral (well-formedness) ... - [3 proof obligations] verified - -Verifying CheckReadsLambdaPartial (well-formedness) ... - [2 proof obligations] verified - -Verifying CheckReadsLambdaTotal (well-formedness) ... - [1 proof obligation] verified +Verified 0/7 symbols. Waiting for CheckReads to verify. +Verification part 1/1 of CheckReads, on line 8, could not prove all assertions, redacted and consuming 1.1E+004 resources +ArrowTypeOptimizations.dfy(11,2): Error: function precondition could not be proved +ArrowTypeOptimizations.dfy(11,2): Error: insufficient reads clause to invoke function +Verified 1/7 symbols. Waiting for CheckPre to verify. +Verification part 1/1 of CheckPre, on line 14, could not prove all assertions, redacted and consuming 1.0E+004 resources +ArrowTypeOptimizations.dfy(17,2): Error: function precondition could not be proved +Verified 2/7 symbols. Waiting for CheckReadsTot to verify. +Verification part 1/1 of CheckReadsTot, on line 20, verified successfully, redacted and consuming 1.0E+004 resources +Verified 3/7 symbols. Waiting for CheckReadsParens to verify. +Verification part 1/1 of CheckReadsParens, on line 26, verified successfully, redacted and consuming 1.0E+004 resources +Verified 4/7 symbols. Waiting for CheckReadsLambdaGeneral to verify. +Verification part 1/1 of CheckReadsLambdaGeneral, on line 32, verified successfully, redacted and consuming 1.9E+004 resources +Verified 5/7 symbols. Waiting for CheckReadsLambdaPartial to verify. +Verification part 1/1 of CheckReadsLambdaPartial, on line 38, verified successfully, redacted and consuming 1.7E+004 resources +Verified 6/7 symbols. Waiting for CheckReadsLambdaTotal to verify. +Verification part 1/1 of CheckReadsLambdaTotal, on line 44, verified successfully, redacted and consuming 1.5E+004 resources Dafny program verifier finished with 5 verified, 3 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Classes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Classes.dfy index 0d42448c01..3907a51444 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Classes.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Classes.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny "%s" > "%t" +// RUN: %exits-with 4 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" @@ -11,7 +11,7 @@ class C { method K() { var f := C.Static; - var o : object?; + var o : object? := *; assert o !in f.reads(); assert f.requires(); assert f(); diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.legacy.dfy similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.legacy.dfy diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.legacy.dfy.expect similarity index 100% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.dfy.expect rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Folding.legacy.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ReadsReadsOnMethods.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ReadsReadsOnMethods.dfy index 9fdad7482e..14e9e47ad8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ReadsReadsOnMethods.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ReadsReadsOnMethods.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /print:"%t.print" /readsClausesOnMethods:1 "%s" > "%t" +// RUN: %exits-with 4 %build --reads-clauses-on-methods "%s" > "%t" // RUN: %diff "%s.expect" "%t" // Clone of ReadsReads.dfy but using methods instead of functions diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ResolveError.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ResolveError.dfy index 2d459ea668..203be07583 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ResolveError.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ResolveError.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /print:"%t.print" "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" module Tests { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Types.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Types.dfy index 13edc4663e..1c9a9e6425 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Types.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Types.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /print:"%t.print" "%s" > "%t" +// RUN: %exits-with 2 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" method FnEqGhost() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/opened_workaround.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/opened_workaround.dfy index a055873bd0..38013754b4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/opened_workaround.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/irondafny0/opened_workaround.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 3 %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" /allowAxioms:0 /warningsAsErrors > "%t" +// RUN: %exits-with 3 %build %s > "%t" // RUN: %diff "%s.expect" "%t" module A { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/StateMonad.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/StateMonad.dfy index 2afcf35012..74b667a060 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/StateMonad.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lambdas/StateMonad.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /dprint:"%t.dprint" "%s" > "%t" +// RUN: %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" abstract module Monad { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy index c26da13305..30b324a028 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/JsonLogger.dfy @@ -1,4 +1,5 @@ // RUN: %exits-with 4 %baredafny verify --show-snippets:false --log-format:json --isolate-assertions "%s" > "%t" +// Also test old CLI // RUN: %exits-with 4 %baredafny /compile:0 /verificationLogger:json /vcsSplitOnEveryAssert "%s" >> "%t" // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK: vcNum.:1,.outcome.:.Valid.*vcNum.:3,.outcome.:.Invalid diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy index 5ef994e089..47c5da7a04 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyWarnings.dfy @@ -1,5 +1,6 @@ // RUN: %baredafny verify --use-basename-for-filename --allow-axioms --show-snippets false --verify-included-files --warn-contradictory-assumptions --warn-redundant-assumptions --allow-warnings "%s" > "%t.new" // RUN: %diff "%s.expect" "%t.new" +// Also test old CLI // RUN: %baredafny /compile:0 /useBaseNameForFileName /verifyAllModules /warnContradictoryAssumptions /warnRedundantAssumptions "%s" > "%t.old" // RUN: %diff "%s.expect" "%t.old" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy index 0671646883..8567235715 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/VerboseName.dfy @@ -1,8 +1,8 @@ -// RUN: %dafny /compile:0 /trace "%s" > "%t" +// RUN: %verify --progress --cores 1 "%s" > "%t" // RUN: %OutputCheck --file-to-check "%t" "%s" -// CHECK-L:Verifying AM1.T2Client.Calc (override check) ... -// CHECK-L:Verifying posIdMeth (correctness) ... -// CHECK-L:Verifying smallPrime (well-formedness) ... +// CHECK-L:Verified 0/5 symbols. Waiting for smallPrime to verify. +// CHECK-L:Verified 2/5 symbols. Waiting for posIdMeth to verify. +// CHECK-L:Verified 4/5 symbols. Waiting for AM1.T2Client.Calc to verify. newtype smallPrime = x: int | x in {2, 3, 5, 7} witness 2 function posId(x: smallPrime): smallPrime { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/ConsistentWhenSupported.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/ConsistentWhenSupported.dfy index 6a13c0f386..a0be8cda7c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/ConsistentWhenSupported.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/metatests/ConsistentWhenSupported.dfy @@ -2,12 +2,12 @@ // Old way: // RUN: %exits-with 0 %verify "%s" > "%t" -// RUN: %exits-with 0 %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t" -// RUN: %exits-with 0 %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t" -// RUN: %exits-with 0 %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t" -// RUN: %exits-with 3 %dafny /noVerify /compile:4 /compileTarget:cpp "%s" >> "%t" -// RUN: %exits-with 0 %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t" +// RUN: %exits-with 0 %run --no-verify --target cs "%s" >> "%t" +// RUN: %exits-with 0 %run --no-verify --target js "%s" >> "%t" +// RUN: %exits-with 0 %run --no-verify --target go "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target java "%s" >> "%t" +// RUN: %exits-with 3 %run --no-verify --target cpp "%s" >> "%t" +// RUN: %exits-with 0 %run --no-verify --target py "%s" >> "%t" // RUN: %diff "%s.oldway.expect" "%t" // New way: diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/name with space/run.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/name with space/run.dfy index afd921cd70..b7267316e1 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/name with space/run.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/name with space/run.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 0 %dafny /compile:3 "%s" > "%t" +// RUN: %exits-with 0 %run "%s" > "%t" // RUN: %diff "%s.expect" "%t" method Main() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/PatternMatchingErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/PatternMatchingErrors.dfy index 0b61795d06..5cb0539487 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/PatternMatchingErrors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/patterns/PatternMatchingErrors.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /errorLimit:0 "%s" > "%t" +// RUN: %exits-with 4 %verify --error-limit 0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" /* diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraits.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraits.dfy index ff59ec8b95..fc5bd843ce 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraits.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraits.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /typeSystemRefresh:1 /generalTraits:full "%s" > "%t" +// RUN: %exits-with 2 %build --type-system-refresh --general-traits full "%s" > "%t" // RUN: %diff "%s.expect" "%t" module Tests { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraitsVerify.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraitsVerify.dfy index e3bd85a3dd..148d6b8338 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraitsVerify.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraitsVerify.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /typeSystemRefresh:1 /generalTraits:full "%s" > "%t" +// RUN: %exits-with 4 %build --type-system-refresh --general-traits full "%s" > "%t" // RUN: %diff "%s.expect" "%t" module Tests { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraitsVerify.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraitsVerify.dfy.expect index 518d3c24e9..ba17e06b35 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraitsVerify.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/GeneralTraitsVerify.dfy.expect @@ -6,4 +6,4 @@ GeneralTraitsVerify.dfy(50,13): Error: value of expression (of type 'Parent') is GeneralTraitsVerify.dfy(53,13): Error: value does not satisfy the subset constraints of 'MyConstrainedInt' GeneralTraitsVerify.dfy(419,11): Error: assertion might not hold -Dafny program verifier finished with 48 verified, 7 errors +Dafny program verifier finished with 52 verified, 7 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy index c29d3e4262..6f45dc1048 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraits.dfy @@ -1,5 +1,5 @@ -// RUN: %exits-with 2 %dafny /generalTraits:legacy "%s" > "%t" -// RUN: %exits-with 2 %dafny /generalTraits:datatype "%s" >> "%t" +// RUN: %exits-with 2 %build --general-traits legacy "%s" > "%t" +// RUN: %exits-with 2 %build --general-traits datatype "%s" >> "%t" // RUN: %diff "%s.expect" "%t" module Tests { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraitsVerify.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraitsVerify.dfy index 221b5a8bd8..e93367473c 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraitsVerify.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/NonReferenceTraitsVerify.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /generalTraits:datatype "%s" > "%t" +// RUN: %exits-with 4 %build --general-traits datatype "%s" > "%t" // RUN: %diff "%s.expect" "%t" module ChildIsNonRefTrait { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitCompileErrors.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitCompileErrors.dfy index 6cd9516346..5796663c8b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitCompileErrors.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitCompileErrors.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 3 %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" /allowAxioms:0 > "%t" +// RUN: %exits-with 3 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" module StaticMembers { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitVariance.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitVariance.dfy index bf8b2aa07d..c44a2ae9e5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitVariance.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitVariance.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 2 %dafny /generalTraits:full "%s" > "%t" +// RUN: %exits-with 2 %build --general-traits full "%s" > "%t" // RUN: %diff "%s.expect" "%t" module NoVariance { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitVerify.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitVerify.dfy index f409d3c66d..1c3f3b90bd 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitVerify.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitVerify.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %exits-with 4 %build "%s" > "%t" // RUN: %diff "%s.expect" "%t" trait Tr { } @@ -8,14 +8,14 @@ class B extends Tr { } class C extends Tr { } method M(a: A, b: B) { - var c: C?; + var c: C? := *; var t; // Tr? t := a; t := c; } method N(a: A, b: B) { - var c: C?; + var c: C? := *; var t: Tr; t := a; t := c; // error: c may be null diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitVerify.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitVerify.dfy.expect index d6812d4027..d2b472b38a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitVerify.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/traits/TraitVerify.dfy.expect @@ -2,4 +2,4 @@ TraitVerify.dfy(21,7): Error: value of expression (of type 'C?') is not kno TraitVerify.dfy(25,7): Error: value of expression (of type 'A?') is not known to be an instance of type 'Tr' TraitVerify.dfy(30,7): Error: value of expression (of type 'A?') is not known to be an instance of type 'A', because it might be null -Dafny program verifier finished with 4 verified, 3 errors +Dafny program verifier finished with 5 verified, 3 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/CompileWithArguments.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/CompileWithArguments.dfy index 9875c49679..97ac70bd21 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/CompileWithArguments.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/CompileWithArguments.dfy @@ -5,8 +5,8 @@ // RUN: %baredafny run %args --unicode-char --no-verify --target:cs "%s" Csharp 1 >> "%t" // RUN: %baredafny run %args --unicode-char --no-verify --target:java "%s" -- Java --heya >> "%t" // RUN: %baredafny run %args --unicode-char --no-verify --target:js "%s" -- Javascript 2 >> "%t" -// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /compileTarget:py "%s" --args Python 1 >> "%t" -// RUN: %dafny /noVerify /compile:4 /unicodeChar:1 /compileTarget:go "%s" --args "Go go" 1 >> "%t" +// RUN: %run --no-verify --unicode-char --target py "%s" Python 1 >> "%t" +// RUN: %run --no-verify --unicode-char --target go "%s" "Go go" 1 >> "%t" // RUN: %baredafny build %args --unicode-char --no-verify --target:cs "%s" --output:%s.dll // RUN: dotnet %s.dll "dotnet" "howdy" >> "%t" // RUN: dotnet %s.dll "dotnet" "hello" >> "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/ExternDafnyString.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/ExternDafnyString.dfy index 1e9701857a..472f464f86 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/ExternDafnyString.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/ExternDafnyString.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /unicodeChar:1 /compileTarget:java "%s" %S/ExternDafnyString.java > "%t" +// RUN: %run --unicode-char --target java "%s" --input %S/ExternDafnyString.java > "%t" // RUN: %diff "%s.expect" "%t" // In this example, the extern method obtains a Java string and returns it as a Dafny string. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/ExternJavaString.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/ExternJavaString.dfy index 5fb7bd9adb..c217fc036b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/ExternJavaString.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/comp/ExternJavaString.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:3 /unicodeChar:1 /compileTarget:java "%s" %S/Conversions.java %S/ExternJavaString.java > "%t" +// RUN: %run --unicode-char --target java "%s" --input %S/Conversions.java --input %S/ExternJavaString.java > "%t" // RUN: %diff "%s.expect" "%t" // In this example, the extern method obtains a Java string and returns it as such. // The Dafny code converts that Java string to a Dafny string. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/expectations/ExpectAndExceptions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/expectations/ExpectAndExceptions.dfy index 1884d82b73..7f5bdcc8c2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/expectations/ExpectAndExceptions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/expectations/ExpectAndExceptions.dfy @@ -1,7 +1,7 @@ -// RUN: ! %dafny /compile:3 /compileTarget:cs /unicodeChar:1 "%s" > "%t" -// RUN: ! %dafny /compile:3 /compileTarget:go /unicodeChar:1 "%s" >> "%t" -// RUN: ! %dafny /compile:3 /compileTarget:java /unicodeChar:1 "%s" >> "%t" -// RUN: ! %dafny /compile:3 /compileTarget:js /unicodeChar:1 "%s" >> "%t" -// RUN: ! %dafny /compile:3 /compileTarget:py /unicodeChar:1 "%s" >> "%t" +// RUN: ! %run --target cs "%s" > "%t" +// RUN: ! %run --target go "%s" >> "%t" +// RUN: ! %run --target java "%s" >> "%t" +// RUN: ! %run --target js "%s" >> "%t" +// RUN: ! %run --target py "%s" >> "%t" // RUN: %diff "%s.expect" "%t" include "../../expectations/ExpectAndExceptions.dfy" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/expectations/ExpectWithMessage.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/expectations/ExpectWithMessage.dfy index 6d7f6d0646..cde0cfb17b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/expectations/ExpectWithMessage.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/expectations/ExpectWithMessage.dfy @@ -1,7 +1,7 @@ -// RUN: ! %dafny /compile:3 /compileTarget:cs /unicodeChar:1 "%s" > "%t" -// RUN: ! %dafny /compile:3 /compileTarget:go /unicodeChar:1 "%s" >> "%t" -// RUN: ! %dafny /compile:3 /compileTarget:java /unicodeChar:1 "%s" >> "%t" -// RUN: ! %dafny /compile:3 /compileTarget:js /unicodeChar:1 "%s" >> "%t" -// RUN: ! %dafny /compile:3 /compileTarget:py /unicodeChar:1 "%s" >> "%t" +// RUN: ! %run --target cs "%s" > "%t" +// RUN: ! %run --target go "%s" >> "%t" +// RUN: ! %run --target java "%s" >> "%t" +// RUN: ! %run --target js "%s" >> "%t" +// RUN: ! %run --target py "%s" >> "%t" // RUN: %diff "%s.expect" "%t" include "../../expectations/ExpectWithMessage.dfy" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/expectations/ExpectWithNonStringMessage.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/expectations/ExpectWithNonStringMessage.dfy index 9b609bbb04..60e192d811 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/expectations/ExpectWithNonStringMessage.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodechars/expectations/ExpectWithNonStringMessage.dfy @@ -1,9 +1,9 @@ // RUN: %verify --verify-included-files "%s" > "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:cs /unicodeChar:1 "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:go /unicodeChar:1 "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:java /unicodeChar:1 "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:js /unicodeChar:1 "%s" >> "%t" -// RUN: ! %dafny /noVerify /compile:4 /compileTarget:py /unicodeChar:1 "%s" >> "%t" +// RUN: ! %run --no-verify --target cs "%s" >> "%t" +// RUN: ! %run --no-verify --target go "%s" >> "%t" +// RUN: ! %run --no-verify --target java "%s" >> "%t" +// RUN: ! %run --no-verify --target js "%s" >> "%t" +// RUN: ! %run --no-verify --target py "%s" >> "%t" // RUN: %diff "%s.expect" "%t" // Note this is one good example of printing regressing with /unicodeChar:1 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/GoModule.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/GoModule.dfy index 1b5cdafae6..8e69cdf6c5 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/GoModule.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/wishlist/GoModule.dfy @@ -1,6 +1,5 @@ // NONUNIFORM: Go-specific extern test -// RUN: %exits-with 3 %dafny /compile:3 /unicodeChar:0 /spillTargetCode:2 "%s" /compileTarget:go 2> "%t" -// note: putting /compileTarget:go after "%s" overrides user-provided option +// RUN: %exits-with 3 %run --unicode-char false --target go "%s" &> "%t" // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK: undefined: GoModuleConversions.ParseURL