From 0831717dfa65c37cc5163675774d7c835697bbfe Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 8 Jan 2025 09:24:45 -0800 Subject: [PATCH 1/4] Update to .NET 8 (#5322) ### Description - Use .NET 8.0 instead of 6.0 throughout the project - Make the ordering of diagnostics deterministic even when multiple diagnostics differ only in their related locations ### How has this been tested? - Updated existing tests to match well-defined ordering 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). --------- Co-authored-by: Remy Willems --- .github/workflows/doc-tests.yml | 6 -- .../workflows/integration-tests-reusable.yml | 2 +- .github/workflows/msbuild.yml | 2 +- .../workflows/publish-release-reusable.yml | 2 +- .github/workflows/publish-release.yml | 2 +- .github/workflows/refman.yml | 2 +- .github/workflows/release-downloads-nuget.yml | 2 +- .github/workflows/runtime-tests.yml | 6 -- .github/workflows/xunit-tests-reusable.yml | 2 +- CONTRIBUTING.md | 2 +- Scripts/use-local-boogie.sh | 2 +- Source/AutoExtern.Test/AutoExtern.Test.csproj | 1 - Source/AutoExtern.Test/Minimal/Library.csproj | 2 +- .../Tutorial/ClientApp/ClientApp.csproj | 4 +- .../Tutorial/Library/Library.csproj | 2 +- Source/AutoExtern/AutoExtern.csproj | 2 +- Source/Dafny/Dafny.csproj | 3 +- .../DafnyBenchmarkingPlugin.csproj | 1 - Source/DafnyCore.Test/DafnyCore.Test.csproj | 1 - .../DafnyToRustCompilerCoverage.cs | 2 +- .../GeneratedFromDafny/DefsCoverage.cs | 2 +- .../FactorPathsOptimizationTest.cs | 2 +- .../GeneratedFromDafny/RASTCoverage.cs | 2 +- Source/DafnyCore/AST/SystemModuleManager.cs | 2 +- .../Backends/CSharp/CsharpBackend.cs | 2 +- .../Backends/CSharp/CsharpCodeGenerator.cs | 2 +- Source/DafnyCore/DafnyCore.csproj | 7 +- Source/DafnyCore/DafnyGeneratedFromDafny.sh | 2 +- .../GeneratedFromDafny/D2DPrettyPrinter.cs | 2 +- Source/DafnyCore/GeneratedFromDafny/DAST.cs | 2 +- .../GeneratedFromDafny/DAST_Format.cs | 2 +- Source/DafnyCore/GeneratedFromDafny/DCOMP.cs | 2 +- .../DafnyCompilerRustUtils.cs | 2 +- Source/DafnyCore/GeneratedFromDafny/Defs.cs | 2 +- .../ExpressionOptimization.cs | 2 +- .../FactorPathsOptimization.cs | 2 +- .../GeneratedFromDafny/Formatting.cs | 2 +- .../GeneratedFromDafny/FuncExtensions.cs | 2 +- Source/DafnyCore/GeneratedFromDafny/RAST.cs | 2 +- .../ResolvedDesugaredExecutableDafnyPlugin.cs | 2 +- .../Std_Arithmetic_DivInternals.cs | 2 +- .../Std_Arithmetic_DivInternalsNonlinear.cs | 2 +- .../Std_Arithmetic_DivMod.cs | 2 +- .../Std_Arithmetic_GeneralInternals.cs | 2 +- .../Std_Arithmetic_Logarithm.cs | 2 +- .../Std_Arithmetic_ModInternals.cs | 2 +- .../Std_Arithmetic_ModInternalsNonlinear.cs | 2 +- .../GeneratedFromDafny/Std_Arithmetic_Mul.cs | 2 +- .../Std_Arithmetic_MulInternals.cs | 2 +- .../Std_Arithmetic_MulInternalsNonlinear.cs | 2 +- .../Std_Arithmetic_Power.cs | 2 +- .../Std_Arithmetic_Power2.cs | 2 +- .../GeneratedFromDafny/Std_Collections_Seq.cs | 2 +- .../DafnyCore/GeneratedFromDafny/Std_Math.cs | 2 +- .../GeneratedFromDafny/Std_Strings.cs | 2 +- .../Std_Strings_CharStrEscaping.cs | 2 +- .../Std_Strings_DecimalConversion.cs | 2 +- .../Std_Strings_HexConversion.cs | 2 +- .../GeneratedFromDafny/Std_Wrappers.cs | 2 +- Source/DafnyCore/Generic/DafnyDiagnostic.cs | 59 ++++++++++++++++ Source/DafnyCore/Generic/Reporting.cs | 3 - .../DafnyDriver.Test/DafnyDriver.Test.csproj | 1 - .../LanguageServerProcessTest.cs | 4 +- Source/DafnyDriver/Commands/VerifyCommand.cs | 4 +- Source/DafnyDriver/DafnyDriver.csproj | 5 +- .../DafnyLanguageServer.Test.csproj | 1 - .../Performance/LargeFilesTest.cs | 4 +- .../DafnyLanguageServer.csproj | 5 +- .../Language/CachingParser.cs | 4 +- .../Language/CachingResolver.cs | 4 +- .../DafnyPipeline.Test.csproj | 1 - .../DafnyPipeline.Test/ProverLogStability.cs | 2 +- Source/DafnyPipeline/DafnyPipeline.csproj | 5 +- .../DafnyRuntime.Tests.csproj | 1 - Source/DafnyRuntime/DafnyRuntime.csproj | 1 + .../DafnyRuntime/DafnyRuntimeSystemModule.cs | 2 +- Source/DafnyServer/DafnyServer.csproj | 5 +- Source/DafnyServer/SuperLegacySymbolTable.cs | 12 +--- .../DafnyTestGeneration.Test.csproj | 1 - .../DafnyTestGeneration.csproj | 3 +- Source/Directory.Build.props | 1 + .../IntegrationTests/IntegrationTests.csproj | 1 - Source/IntegrationTests/LitTests.cs | 2 +- .../DafnyTests/RunAllTests/RunAllTests.csproj | 2 +- .../TestAttribute/TestAttribute.csproj | 2 +- .../comp/manualcompile/ManualCompile.csproj | 2 +- .../comp/manualcompile/ManualCompile.dfy | 2 +- .../consumer/Consumer.csproj | 2 +- .../LitTest/dafny0/AutoReq.dfy.expect | 6 +- .../dafny0/{Fuel.legacy.dfy => Fuel.dfy} | 2 +- .../LitTests/LitTest/dafny0/Fuel.dfy.expect | 67 +++++++++++++++++++ .../LitTest/dafny0/Fuel.legacy.dfy.expect | 67 ------------------- .../LitTest/dafny0/Input/IncludesTuples.dfy | 2 +- ...message-per-failed-precondition.dfy.expect | 8 +-- .../LitTest/examples/Simple_compiler/Makefile | 2 +- .../csharp/SimpleCompiler.csproj | 4 +- .../git-issues/git-issue-2299.dfy.expect | 6 +- .../git-issues/git-issue-3549a.dfy.expect | 2 +- .../InductionWithoutTriggers.dfy.expect | 6 +- ...nductionWithoutTriggers.dfy.refresh.expect | 6 +- Source/TestDafny/TestDafny.csproj | 2 +- Source/XUnitExtensions/Lit/DiffCommand.cs | 2 +- Source/XUnitExtensions/XUnitExtensions.csproj | 2 +- customBoogie.patch | 2 +- docs/DafnyRef/Plugins.md | 2 +- docs/DafnyRef/UserGuide.md | 2 +- docs/Installation.md | 22 +++--- docs/OnlineTutorial/guide.10.expect | 8 +-- 108 files changed, 259 insertions(+), 233 deletions(-) create mode 100644 Source/DafnyCore/Generic/DafnyDiagnostic.cs rename Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/{Fuel.legacy.dfy => Fuel.dfy} (99%) create mode 100755 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy.expect delete mode 100755 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect diff --git a/.github/workflows/doc-tests.yml b/.github/workflows/doc-tests.yml index 919b1aeece1..99dc121ca7f 100644 --- a/.github/workflows/doc-tests.yml +++ b/.github/workflows/doc-tests.yml @@ -32,12 +32,6 @@ jobs: uses: actions/setup-dotnet@v4 with: dotnet-version: 8.0.x - # If we do not also install .NET 6 as well, then our doc-tests fail for an unknown reason - # Failing run: https://github.com/dafny-lang/dafny/actions/runs/12276984671/job/34255376460 - - name: Setup dotnet - uses: actions/setup-dotnet@v4 - with: - dotnet-version: 6.0.x - name: Checkout Dafny uses: actions/checkout@v4 with: diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index ed6ee6687f3..3109c167ccb 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.github/workflows/integration-tests-reusable.yml @@ -19,7 +19,7 @@ on: default: "" env: - dotnet-version: 6.0.x # SDK Version for building Dafny + dotnet-version: 8.0.x # SDK Version for building Dafny jobs: # This job is used to dynamically calculate the matrix dimensions. diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml index c8c8e173e00..5e779c576a8 100644 --- a/.github/workflows/msbuild.yml +++ b/.github/workflows/msbuild.yml @@ -12,7 +12,7 @@ concurrency: env: - dotnet-version: 6.0.x # SDK Version for building Dafny + dotnet-version: 8.0.x # SDK Version for building Dafny jobs: check-deep-tests: diff --git a/.github/workflows/publish-release-reusable.yml b/.github/workflows/publish-release-reusable.yml index d288548bf83..adee22747dc 100644 --- a/.github/workflows/publish-release-reusable.yml +++ b/.github/workflows/publish-release-reusable.yml @@ -30,7 +30,7 @@ on: required: false env: - dotnet-version: 6.0.x # SDK Version for building Dafny + dotnet-version: 8.0.x # SDK Version for building Dafny jobs: diff --git a/.github/workflows/publish-release.yml b/.github/workflows/publish-release.yml index 7600affd731..7b3ee73a7ef 100644 --- a/.github/workflows/publish-release.yml +++ b/.github/workflows/publish-release.yml @@ -7,7 +7,7 @@ on: - 'v*' env: - dotnet-version: 6.0.x # SDK Version for building Dafny + dotnet-version: 8.0.x # SDK Version for building Dafny jobs: deep-integration-tests: diff --git a/.github/workflows/refman.yml b/.github/workflows/refman.yml index 72caa203bfb..93a65d4470b 100644 --- a/.github/workflows/refman.yml +++ b/.github/workflows/refman.yml @@ -28,7 +28,7 @@ jobs: - name: Setup dotnet uses: actions/setup-dotnet@v4 with: - dotnet-version: 6.0.x + dotnet-version: 8.0.x - name: Checkout Dafny uses: actions/checkout@v4 with: diff --git a/.github/workflows/release-downloads-nuget.yml b/.github/workflows/release-downloads-nuget.yml index 09c25932a11..1d08a00ba40 100644 --- a/.github/workflows/release-downloads-nuget.yml +++ b/.github/workflows/release-downloads-nuget.yml @@ -17,7 +17,7 @@ on: workflow_dispatch: env: - dotnet-version: 6.0.x # SDK Version for running Dafny (TODO: should this be an older version?) + dotnet-version: 8.0.x # SDK Version for running Dafny (TODO: should this be an older version?) z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02 concurrency: diff --git a/.github/workflows/runtime-tests.yml b/.github/workflows/runtime-tests.yml index 8a5719110b2..0d5888a133d 100644 --- a/.github/workflows/runtime-tests.yml +++ b/.github/workflows/runtime-tests.yml @@ -31,12 +31,6 @@ jobs: uses: actions/setup-dotnet@v4 with: dotnet-version: 8.0.x - # If we do not also install .NET 6 as well, then our doc-tests fail for an unknown reason - # Failing run: https://github.com/dafny-lang/dafny/actions/runs/12276984671/job/34255376460 - - name: Setup dotnet - uses: actions/setup-dotnet@v4 - with: - dotnet-version: 6.0.x - name: Set up JDK 18 uses: actions/setup-java@v4 with: diff --git a/.github/workflows/xunit-tests-reusable.yml b/.github/workflows/xunit-tests-reusable.yml index 68576f2315f..d6b768e6f3a 100644 --- a/.github/workflows/xunit-tests-reusable.yml +++ b/.github/workflows/xunit-tests-reusable.yml @@ -73,7 +73,7 @@ jobs: - name: Setup .NET uses: actions/setup-dotnet@v4 with: - dotnet-version: 6.0.x + dotnet-version: 8.0.x - name: Install dependencies run: | dotnet restore ${{env.solutionPath}} diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b181dac5d1d..ddaf0541814 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -85,7 +85,7 @@ Subsequent CI runs should pick up the successful `deep-tests` run and make the ` ### How can I write portions of Dafny in Dafny itself? Since https://github.com/dafny-lang/dafny/pull/2399, it is possible to add \*.dfy files next to other source files. -The plugin `dafny-msbuild` takes all the dafny files and compiles them into a single file `Source/DafnyCore/obj/Debug/net6.0/GeneratedFromDafny.cs` +The plugin `dafny-msbuild` takes all the dafny files and compiles them into a single file `Source/DafnyCore/obj/Debug/net8.0/GeneratedFromDafny.cs` that is automatically included in the build process. This file contains also the Dafny run-time in C#. One example of such file is `Source/DafnyCore/AST/Formatting.dfy`, and you can use it as a starting point. diff --git a/Scripts/use-local-boogie.sh b/Scripts/use-local-boogie.sh index e3e23d2c0b2..49f1f45613d 100755 --- a/Scripts/use-local-boogie.sh +++ b/Scripts/use-local-boogie.sh @@ -2,5 +2,5 @@ BOOGIE_PATH="boogie/" allDlls=("Boogie.AbstractInterpretation.dll" "Boogie.BaseTypes.dll" "Boogie.CodeContractsExtender.dll" "Boogie.Concurrency.dll" "Boogie.Core.dll" "Boogie.ExecutionEngine.dll" "Boogie.Graph.dll" "Boogie.Houdini.dll" "Boogie.Model.dll" "Boogie.Predication.dll" "Boogie.Provers.SMTLib.dll" "Boogie.VCExpr.dll" "Boogie.VCGeneration.dll" "BoogieDriver.dll" "System.Configuration.ConfigurationManager.dll" "System.Runtime.Caching.dll" "System.Security.Cryptography.ProtectedData.dll" "System.Security.Permissions.dll") for t in "${allDlls[@]}" do - cp "${BOOGIE_PATH}Source/BoogieDriver/bin/Release/net6.0/${t}" Binaries/ + cp "${BOOGIE_PATH}Source/BoogieDriver/bin/Release/net8.0/${t}" Binaries/ done diff --git a/Source/AutoExtern.Test/AutoExtern.Test.csproj b/Source/AutoExtern.Test/AutoExtern.Test.csproj index 0c4e1dc0b51..08593d7dba6 100644 --- a/Source/AutoExtern.Test/AutoExtern.Test.csproj +++ b/Source/AutoExtern.Test/AutoExtern.Test.csproj @@ -2,7 +2,6 @@ Exe - net6.0 enable enable false diff --git a/Source/AutoExtern.Test/Minimal/Library.csproj b/Source/AutoExtern.Test/Minimal/Library.csproj index 132c02c59c2..30402ac0e7a 100644 --- a/Source/AutoExtern.Test/Minimal/Library.csproj +++ b/Source/AutoExtern.Test/Minimal/Library.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable enable diff --git a/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj b/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj index 86b01ff865f..7ba274e8ce9 100644 --- a/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj +++ b/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj @@ -2,9 +2,9 @@ Exe - net6.0 + net8.0 enable - CS3021; CS0162 + CS8981; CS3021; CS0162 diff --git a/Source/AutoExtern.Test/Tutorial/Library/Library.csproj b/Source/AutoExtern.Test/Tutorial/Library/Library.csproj index 132c02c59c2..30402ac0e7a 100644 --- a/Source/AutoExtern.Test/Tutorial/Library/Library.csproj +++ b/Source/AutoExtern.Test/Tutorial/Library/Library.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable enable diff --git a/Source/AutoExtern/AutoExtern.csproj b/Source/AutoExtern/AutoExtern.csproj index 0c00890cffc..f44de5524b4 100644 --- a/Source/AutoExtern/AutoExtern.csproj +++ b/Source/AutoExtern/AutoExtern.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 enable enable false diff --git a/Source/Dafny/Dafny.csproj b/Source/Dafny/Dafny.csproj index ff383440c30..7c639eb2b7e 100644 --- a/Source/Dafny/Dafny.csproj +++ b/Source/Dafny/Dafny.csproj @@ -5,7 +5,6 @@ Dafny true TRACE - net6.0 Major ..\..\Binaries\ false @@ -16,7 +15,7 @@ README.md - + false false diff --git a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj index 9cf987817bc..85823c27a94 100644 --- a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj +++ b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj @@ -1,7 +1,6 @@ - net6.0 Major enable enable diff --git a/Source/DafnyCore.Test/DafnyCore.Test.csproj b/Source/DafnyCore.Test/DafnyCore.Test.csproj index 8e9d3e8aeba..e585e29faf8 100644 --- a/Source/DafnyCore.Test/DafnyCore.Test.csproj +++ b/Source/DafnyCore.Test/DafnyCore.Test.csproj @@ -1,7 +1,6 @@ - net6.0 enable enable diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs index fc783dccf8c..699aeffaaf2 100644 --- a/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs +++ b/Source/DafnyCore.Test/GeneratedFromDafny/DafnyToRustCompilerCoverage.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs index 9ea4308a4f6..c31e0447b04 100644 --- a/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs +++ b/Source/DafnyCore.Test/GeneratedFromDafny/DefsCoverage.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs index 7b3f9367309..04573118e97 100644 --- a/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs +++ b/Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs b/Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs index 8b8833e5adb..bebebfe2763 100644 --- a/Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs +++ b/Source/DafnyCore.Test/GeneratedFromDafny/RASTCoverage.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs index e153c76bfe7..2c8c02fa49f 100644 --- a/Source/DafnyCore/AST/SystemModuleManager.cs +++ b/Source/DafnyCore/AST/SystemModuleManager.cs @@ -62,7 +62,7 @@ public byte[] MyHash { Concat(TotalArrowTypeDecls.Keys.OrderBy(x => x)). Concat(tupleInts.OrderBy(x => x)); var bytes = ints.SelectMany(BitConverter.GetBytes).ToArray(); - hash = HashAlgorithm.Create("SHA256")!.ComputeHash(bytes); + hash = SHA256.Create()!.ComputeHash(bytes); } return hash; diff --git a/Source/DafnyCore/Backends/CSharp/CsharpBackend.cs b/Source/DafnyCore/Backends/CSharp/CsharpBackend.cs index 82e8606a0f9..50c293c1f0c 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpBackend.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpBackend.cs @@ -92,7 +92,7 @@ public override string GetCompileName(bool isDefaultModule, string moduleName, s {outputType} - net6.0 + net8.0 enable false CS8600;CS8603;CS8604;CS8605;CS8625;CS8629;CS8714;CS8765;CS8769;CS8981 diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index cccbd96d392..9bbc493116e 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -67,7 +67,7 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { wr.WriteLine("// Dafny program {0} compiled into C#", program.Name); wr.WriteLine("// To recompile, you will need the libraries"); wr.WriteLine("// System.Runtime.Numerics.dll System.Collections.Immutable.dll"); - wr.WriteLine("// but the 'dotnet' tool in net6.0 should pick those up automatically."); + wr.WriteLine("// but the 'dotnet' tool in .NET should pick those up automatically."); wr.WriteLine("// Optionally, you may want to include compiler switches like"); wr.WriteLine("// /debug /nowarn:162,164,168,183,219,436,1717,1718"); wr.WriteLine(); diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 3ac2ed66bb6..56f845c656d 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -17,11 +17,12 @@ true ..\..\Binaries\ TRACE - net6.0 Major MIT - $(NoWarn);NU5104 + $(NoWarn);NU5104;CS8981 + + true @@ -35,7 +36,7 @@ - + diff --git a/Source/DafnyCore/DafnyGeneratedFromDafny.sh b/Source/DafnyCore/DafnyGeneratedFromDafny.sh index 2ae61370ed8..44210dad646 100755 --- a/Source/DafnyCore/DafnyGeneratedFromDafny.sh +++ b/Source/DafnyCore/DafnyGeneratedFromDafny.sh @@ -4,7 +4,7 @@ # 1. Delete the file GeneratedFromDafny.cs # 2. Add a dependency to # -# That's it! The same file will now be automatically generated as obj/Debug/net6.0/GeneratedFromDafny.cs +# That's it! The same file will now be automatically generated as obj/Debug/net8.0/GeneratedFromDafny.cs # 3. Remove the following dependencies that are being taken care by dafny-msbuild # # diff --git a/Source/DafnyCore/GeneratedFromDafny/D2DPrettyPrinter.cs b/Source/DafnyCore/GeneratedFromDafny/D2DPrettyPrinter.cs index eaf1d9b97eb..9216519c02e 100644 --- a/Source/DafnyCore/GeneratedFromDafny/D2DPrettyPrinter.cs +++ b/Source/DafnyCore/GeneratedFromDafny/D2DPrettyPrinter.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/DAST.cs b/Source/DafnyCore/GeneratedFromDafny/DAST.cs index 17306167c65..b6152f6d382 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DAST.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DAST.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs b/Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs index 1efc61a86e8..b7550c51a94 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DAST_Format.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs index 01c84f6080a..154c7d9a08a 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DCOMP.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs b/Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs index 061db1db0df..e83a87fbeb1 100644 --- a/Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs +++ b/Source/DafnyCore/GeneratedFromDafny/DafnyCompilerRustUtils.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Defs.cs b/Source/DafnyCore/GeneratedFromDafny/Defs.cs index cd86606bcf3..e8e90c99a84 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Defs.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Defs.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/ExpressionOptimization.cs b/Source/DafnyCore/GeneratedFromDafny/ExpressionOptimization.cs index 2b9201f0b84..2ffd8bd8980 100644 --- a/Source/DafnyCore/GeneratedFromDafny/ExpressionOptimization.cs +++ b/Source/DafnyCore/GeneratedFromDafny/ExpressionOptimization.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs b/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs index 2308d3c7675..6d755a587c1 100644 --- a/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs +++ b/Source/DafnyCore/GeneratedFromDafny/FactorPathsOptimization.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Formatting.cs b/Source/DafnyCore/GeneratedFromDafny/Formatting.cs index 07d403c955d..f8026126c1e 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Formatting.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Formatting.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs b/Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs index 39894fcdf07..af326244b50 100644 --- a/Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs +++ b/Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/RAST.cs b/Source/DafnyCore/GeneratedFromDafny/RAST.cs index 8c0c742cf26..eeceeaf7c4c 100644 --- a/Source/DafnyCore/GeneratedFromDafny/RAST.cs +++ b/Source/DafnyCore/GeneratedFromDafny/RAST.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs b/Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs index b545bb2a8e1..b6eb208ee5b 100644 --- a/Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs +++ b/Source/DafnyCore/GeneratedFromDafny/ResolvedDesugaredExecutableDafnyPlugin.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternals.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternals.cs index 997d1b461c8..cf1aa8ccbe0 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternals.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternals.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternalsNonlinear.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternalsNonlinear.cs index 42ee76c580c..317eb9149b8 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternalsNonlinear.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternalsNonlinear.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivMod.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivMod.cs index 0cacb4aa840..75a36f1e97b 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivMod.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivMod.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_GeneralInternals.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_GeneralInternals.cs index bfbf27c915b..189d7f348bb 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_GeneralInternals.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_GeneralInternals.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Logarithm.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Logarithm.cs index de30d84acaf..081f1d7848c 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Logarithm.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Logarithm.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternals.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternals.cs index 956c44501c2..5b8f8865153 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternals.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternals.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternalsNonlinear.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternalsNonlinear.cs index 30cf7f2c8e8..7643658879a 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternalsNonlinear.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_ModInternalsNonlinear.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Mul.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Mul.cs index 9def4d585f7..fe0b79e122a 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Mul.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Mul.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternals.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternals.cs index dbbe9443722..9d4cccdf0cc 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternals.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternals.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternalsNonlinear.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternalsNonlinear.cs index 28123ed8dd2..58e0b3e074c 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternalsNonlinear.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternalsNonlinear.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power.cs index 5d473618d6f..f5cfdce6f45 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power2.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power2.cs index 8251fce2577..3022cf48023 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power2.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power2.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs index d17cdc366bc..32faed2a001 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Math.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Math.cs index 8e22eb16897..19b08102629 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Math.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Math.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Strings.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Strings.cs index dbda9bad3da..0b2540af5a8 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Strings.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Strings.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Strings_CharStrEscaping.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Strings_CharStrEscaping.cs index c7bcf7b8e0c..54dbb0c05df 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Strings_CharStrEscaping.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Strings_CharStrEscaping.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Strings_DecimalConversion.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Strings_DecimalConversion.cs index a408b172517..3d3cb3c89d7 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Strings_DecimalConversion.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Strings_DecimalConversion.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Strings_HexConversion.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Strings_HexConversion.cs index 57a20d539c8..0217a2ac0c1 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Strings_HexConversion.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Strings_HexConversion.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/GeneratedFromDafny/Std_Wrappers.cs b/Source/DafnyCore/GeneratedFromDafny/Std_Wrappers.cs index bd2a8af634a..6d224dc262e 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Std_Wrappers.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Std_Wrappers.cs @@ -1,7 +1,7 @@ // Dafny program the_program compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyCore/Generic/DafnyDiagnostic.cs b/Source/DafnyCore/Generic/DafnyDiagnostic.cs new file mode 100644 index 00000000000..71f016ede9b --- /dev/null +++ b/Source/DafnyCore/Generic/DafnyDiagnostic.cs @@ -0,0 +1,59 @@ +#nullable enable +using System; +using System.Collections.Generic; + +namespace Microsoft.Dafny; + +public record DafnyDiagnostic(MessageSource Source, string ErrorId, IOrigin Token, string Message, ErrorLevel Level, + IReadOnlyList RelatedInformation) : IComparable { + public int CompareTo(DafnyDiagnostic? other) { + if (other == null) { + return 1; + } + var r0 = OriginCenterComparer.Instance.Compare(Token, other.Token); + if (r0 != 0) { + return r0; + } + + for (var index = 0; index < RelatedInformation.Count; index++) { + if (other.RelatedInformation.Count > index) { + var r1 = RelatedInformation[index].Token.Center.CompareTo(other.RelatedInformation[index].Token.Center); + if (r1 != 0) { + return r1; + } + } else { + return 1; + } + } + + if (other.RelatedInformation.Count > RelatedInformation.Count) { + return -1; + } + + return 0; + } +} + +class OriginCenterComparer : IComparer { + public static readonly OriginCenterComparer Instance = new(); + + public int Compare(IOrigin? x, IOrigin? y) { + if (x == null) { + return -1; + } + + if (y == null) { + return 1; + } + + if (x is NestedOrigin nestedX && y is NestedOrigin nestedY) { + var outer = Compare(nestedX.Outer, nestedY.Outer); + if (outer != 0) { + return outer; + } + + return Compare(nestedX.Inner, nestedY.Inner); + } + return x.Center.CompareTo(y.Center); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs index def369b1672..de600c10c73 100644 --- a/Source/DafnyCore/Generic/Reporting.cs +++ b/Source/DafnyCore/Generic/Reporting.cs @@ -1,7 +1,6 @@ // Copyright by the contributors to the Dafny Project // SPDX-License-Identifier: MIT #nullable enable -using System.Collections.Generic; using System.CommandLine; using System.Linq; @@ -16,8 +15,6 @@ public enum MessageSource { } public record DafnyRelatedInformation(IOrigin Token, string Message); - public record DafnyDiagnostic(MessageSource Source, string ErrorId, IOrigin Token, string Message, ErrorLevel Level, - IReadOnlyList RelatedInformation); public class ErrorReporterSink : ErrorReporter { public ErrorReporterSink(DafnyOptions options) : base(options) { } diff --git a/Source/DafnyDriver.Test/DafnyDriver.Test.csproj b/Source/DafnyDriver.Test/DafnyDriver.Test.csproj index b1681b47cb1..670c6f2ec65 100644 --- a/Source/DafnyDriver.Test/DafnyDriver.Test.csproj +++ b/Source/DafnyDriver.Test/DafnyDriver.Test.csproj @@ -1,7 +1,6 @@ - net6.0 enable enable diff --git a/Source/DafnyDriver.Test/LanguageServerProcessTest.cs b/Source/DafnyDriver.Test/LanguageServerProcessTest.cs index d42c8f4d26a..a180c2401a2 100644 --- a/Source/DafnyDriver.Test/LanguageServerProcessTest.cs +++ b/Source/DafnyDriver.Test/LanguageServerProcessTest.cs @@ -204,10 +204,10 @@ public static async Task Main(string[] args) {{ var configuration = JsonSerializer.Serialize( new { runtimeOptions = new { - tfm = "net6.0", + tfm = "net8.0", framework = new { name = "Microsoft.NETCore.App", - version = "6.0.0", + version = "8.0.0", rollForward = "LatestMinor" } } diff --git a/Source/DafnyDriver/Commands/VerifyCommand.cs b/Source/DafnyDriver/Commands/VerifyCommand.cs index ff8ca57160f..789db4ee4b9 100644 --- a/Source/DafnyDriver/Commands/VerifyCommand.cs +++ b/Source/DafnyDriver/Commands/VerifyCommand.cs @@ -193,13 +193,13 @@ public static void ReportVerificationDiagnostics(CliCompilation compilation, IOb completed.Result, batchReporter); } - foreach (var diagnostic in batchReporter.AllMessages.OrderBy(m => m.Token.Center)) { + foreach (var diagnostic in batchReporter.AllMessages.Order()) { compilation.Compilation.Reporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token, diagnostic.Message); } }); - } + } public static async Task LogVerificationResults(CliCompilation cliCompilation, ResolutionResult resolution, IObservable verificationResults) { diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index d7655e67674..f928e3f5043 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -5,8 +5,7 @@ DafnyDriver false TRACE - net6.0 -Major + Major ..\..\Binaries\ false @@ -15,7 +14,7 @@ true - + false false diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj index e25f0c91a99..16d4a63d5fb 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj @@ -1,7 +1,6 @@  - net6.0 false Microsoft.Dafny.LanguageServer.IntegrationTest diff --git a/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs b/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs index 359ab1ee16a..62c857c2203 100644 --- a/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs +++ b/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs @@ -68,7 +68,7 @@ public async Task QuickEditsInLargeFile() { var afterChange = DateTime.Now; var changeMilliseconds = (afterChange - afterOpen).TotalMilliseconds; await AssertNoDiagnosticsAreComing(CancellationTokenWithHighTimeout); - threadPoolSchedulingCancellationToken.Cancel(); + await threadPoolSchedulingCancellationToken.CancelAsync(); var averageTimeToSchedule = await threadPoolSchedulingTimeTask; var division = changeMilliseconds / openMilliseconds; @@ -124,4 +124,4 @@ await Task.Run(() => { public LargeFilesTest(ITestOutputHelper output) : base(output) { } -} \ No newline at end of file +} diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj index 756bb1eb5a4..67513425d4e 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj @@ -1,8 +1,7 @@  - net6.0 -Major + Major true enable Microsoft.Dafny.LanguageServer @@ -13,7 +12,7 @@ README.md - + false false diff --git a/Source/DafnyLanguageServer/Language/CachingParser.cs b/Source/DafnyLanguageServer/Language/CachingParser.cs index 5a2ec13606f..9973bea5873 100644 --- a/Source/DafnyLanguageServer/Language/CachingParser.cs +++ b/Source/DafnyLanguageServer/Language/CachingParser.cs @@ -36,7 +36,7 @@ protected override DfyParseFileResult ParseFile(DafnyOptions options, FileSnapsh // Add NUL delimiter to avoid collisions (otherwise hash("A" + "BC") == hash("AB" + "C")) var uriBytes = Encoding.UTF8.GetBytes(uri + "\0"); - var (newReader, hash) = ComputeHashFromReader(uriBytes, reader, HashAlgorithm.Create("SHA256")!); + var (newReader, hash) = ComputeHashFromReader(uriBytes, reader, SHA256.Create()!); if (!parseCache.TryGet(hash, out var result)) { logger.LogDebug($"Parse cache miss for {uri}"); result = base.ParseFile(options, fileSnapshot with { Reader = newReader }, uri, cancellationToken); @@ -84,4 +84,4 @@ private static (TextReader reader, byte[] hash) ComputeHashFromReader(byte[] sta result.Add(chunk); } } -} \ No newline at end of file +} diff --git a/Source/DafnyLanguageServer/Language/CachingResolver.cs b/Source/DafnyLanguageServer/Language/CachingResolver.cs index 1bfc9021266..1418549d187 100644 --- a/Source/DafnyLanguageServer/Language/CachingResolver.cs +++ b/Source/DafnyLanguageServer/Language/CachingResolver.cs @@ -75,7 +75,7 @@ protected override ModuleResolutionResult ResolveModuleDeclaration(CompilationDa private byte[] GetHash(ModuleDecl moduleDeclaration) { if (!hashes.TryGetValue(moduleDeclaration, out var result)) { var moduleVertex = dependencies.FindVertex(moduleDeclaration); - var hashAlgorithm = HashAlgorithm.Create("SHA256")!; + var hashAlgorithm = SHA256.Create()!; hashAlgorithm.Initialize(); // We don't want the order of Successors to influence the hash, so we order by the content hash, for which CloneId is currently a proxy var orderedSuccessors = moduleVertex.Successors.OrderBy(s => s.N.CloneId); @@ -98,4 +98,4 @@ private byte[] GetHash(ModuleDecl moduleDeclaration) { return result; } -} \ No newline at end of file +} diff --git a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj index a98109bebaf..34ec4c877a0 100644 --- a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj +++ b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj @@ -1,7 +1,6 @@ - net6.0 false diff --git a/Source/DafnyPipeline.Test/ProverLogStability.cs b/Source/DafnyPipeline.Test/ProverLogStability.cs index 7931d8118e4..18b4e529a75 100644 --- a/Source/DafnyPipeline.Test/ProverLogStability.cs +++ b/Source/DafnyPipeline.Test/ProverLogStability.cs @@ -119,7 +119,7 @@ public async Task ProverLogRegression() { var regularProverLog = await GetProverLogForProgramAsync(options, await GetBoogie(options, originalProgram)); regularProverLog = regularProverLog.Replace("\r", ""); if (updateProverLog) { - var path = Path.GetFullPath(filePath).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net6.0" + Path.DirectorySeparatorChar, ""); + var path = Path.GetFullPath(filePath).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net8.0" + Path.DirectorySeparatorChar, ""); await File.WriteAllTextAsync(path, regularProverLog); await Console.Out.WriteLineAsync("Updated prover log file at " + path); } else { diff --git a/Source/DafnyPipeline/DafnyPipeline.csproj b/Source/DafnyPipeline/DafnyPipeline.csproj index 759c23f348d..559c7781cb2 100644 --- a/Source/DafnyPipeline/DafnyPipeline.csproj +++ b/Source/DafnyPipeline/DafnyPipeline.csproj @@ -7,12 +7,11 @@ false ..\..\Binaries\ TRACE - net6.0 -Major + Major MIT - + false false diff --git a/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj b/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj index f90c85ef0bf..bc05a98a47d 100644 --- a/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj +++ b/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj @@ -1,7 +1,6 @@ - net6.0 enable false diff --git a/Source/DafnyRuntime/DafnyRuntime.csproj b/Source/DafnyRuntime/DafnyRuntime.csproj index 3943da7ce01..8cfbf6fab40 100644 --- a/Source/DafnyRuntime/DafnyRuntime.csproj +++ b/Source/DafnyRuntime/DafnyRuntime.csproj @@ -6,6 +6,7 @@ true false TRACE;ISDAFNYRUNTIMELIB + netstandard2.0;net452 ..\..\Binaries\ 7.3 diff --git a/Source/DafnyRuntime/DafnyRuntimeSystemModule.cs b/Source/DafnyRuntime/DafnyRuntimeSystemModule.cs index b5b6988b139..d0e8ea5dea7 100644 --- a/Source/DafnyRuntime/DafnyRuntimeSystemModule.cs +++ b/Source/DafnyRuntime/DafnyRuntimeSystemModule.cs @@ -1,7 +1,7 @@ // Dafny program systemModulePopulator.dfy compiled into C# // To recompile, you will need the libraries // System.Runtime.Numerics.dll System.Collections.Immutable.dll -// but the 'dotnet' tool in net6.0 should pick those up automatically. +// but the 'dotnet' tool in .NET should pick those up automatically. // Optionally, you may want to include compiler switches like // /debug /nowarn:162,164,168,183,219,436,1717,1718 diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index 38ee3311f28..d736ee1074e 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -5,13 +5,12 @@ DafnyServer false TRACE - net6.0 -Major + Major ..\..\Binaries\ MIT - + false false diff --git a/Source/DafnyServer/SuperLegacySymbolTable.cs b/Source/DafnyServer/SuperLegacySymbolTable.cs index f394a28b074..acec53486a7 100644 --- a/Source/DafnyServer/SuperLegacySymbolTable.cs +++ b/Source/DafnyServer/SuperLegacySymbolTable.cs @@ -227,9 +227,7 @@ private static void ParseUpdateStatement(Statement statement, List(); - var rightSideDots = rightSide.OfType(); - var allExprDotNames = leftSideDots.Concat(rightSideDots); + var allExprDotNames = leftSide.OfType(); foreach (var exprDotName in allExprDotNames) { if (!(exprDotName.Lhs.Type is UserDefinedType)) { continue; @@ -304,12 +302,8 @@ private static IEnumerable ParseBodyForFieldReferences(IEn var updateStmt = (AssignStatement)statement; var leftSide = updateStmt.Lhss; var rightSide = updateStmt.Rhss; - var leftSideDots = leftSide.OfType(); - var rightSideDots = rightSide.OfType(); - var exprDotNames = leftSideDots.Concat(rightSideDots); - var leftSideNameSegments = leftSide.OfType(); - var rightSideNameSegments = rightSide.OfType(); - var nameSegments = leftSideNameSegments.Concat(rightSideNameSegments); + var exprDotNames = leftSide.OfType(); + var nameSegments = leftSide.OfType(); var allRightSideExpressions = rightSide.SelectMany(e => e.SubExpressions.SelectMany(GetAllSubExpressions)); var allLeftSideExpressions = leftSide.SelectMany(e => e.SubExpressions.SelectMany(GetAllSubExpressions)); diff --git a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj index b4920e58810..1ec68cb84bd 100644 --- a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj +++ b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj @@ -1,7 +1,6 @@ - net6.0 false diff --git a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj index 6631561a0ed..016cf01c491 100644 --- a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj +++ b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj @@ -8,8 +8,7 @@ ..\..\Binaries\ true TRACE - net6.0 -Major + Major enable false MIT diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index f7bb029a0e9..3c096675bb1 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -1,6 +1,7 @@ + net8.0 4.9.2 1701;1702;VSTHRD200 diff --git a/Source/IntegrationTests/IntegrationTests.csproj b/Source/IntegrationTests/IntegrationTests.csproj index 5370699a473..cfb699f0622 100644 --- a/Source/IntegrationTests/IntegrationTests.csproj +++ b/Source/IntegrationTests/IntegrationTests.csproj @@ -1,7 +1,6 @@ - net6.0 true false enable diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs index b91a4b5fa44..11e8f226edc 100644 --- a/Source/IntegrationTests/LitTests.cs +++ b/Source/IntegrationTests/LitTests.cs @@ -25,7 +25,7 @@ public class LitTests { private static readonly Assembly TestDafnyAssembly = typeof(MultiBackendTest).Assembly; private static readonly Assembly DafnyServerAssembly = typeof(Server).Assembly; - private static readonly string RepositoryRoot = Path.GetFullPath("../../../../../"); // Up from Source/IntegrationTests/bin/Debug/net6.0/ + private static readonly string RepositoryRoot = Path.GetFullPath("../../../../../"); // Up from Source/IntegrationTests/bin/Debug/net8.0/ private static readonly string[] DefaultBoogieArguments = new[] { "/infer:j", diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj index d8b5e8b41ad..eefc01ebbeb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 false diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj index 768e4f6f829..58a723cd452 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj @@ -1,7 +1,7 @@  - net6.0 + net8.0 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj index 41f1d5ad4b2..a269962b552 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy index b521245c0d1..7adf33da4c7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.dfy @@ -2,7 +2,7 @@ // 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: dotnet %S/bin/Debug/net8.0/ManualCompile.dll >> "%t" // RUN: %translate js --verbose --include-runtime "%s" >> "%t" // RUN: node %S/ManualCompile.js >> "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj index e6bb653223b..b32966d460e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/consumer/Consumer.csproj @@ -2,7 +2,7 @@ - net6.0 + net8.0 Exe diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoReq.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoReq.dfy.expect index a1ede7a9704..f149c64f7bb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoReq.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/AutoReq.dfy.expect @@ -2,16 +2,16 @@ AutoReq.dfy(13,2): Error: function precondition could not be proved AutoReq.dfy(5,13): Related location: this proposition could not be proved AutoReq.dfy(25,2): Error: function precondition could not be proved AutoReq.dfy(5,13): Related location: this proposition could not be proved +AutoReq.dfy(38,11): Error: function precondition could not be proved +AutoReq.dfy(5,13): Related location: this proposition could not be proved AutoReq.dfy(38,11): Error: assertion might not hold AutoReq.dfy(31,12): Related location: this proposition could not be proved AutoReq.dfy(7,4): Related location: this proposition could not be proved -AutoReq.dfy(38,11): Error: function precondition could not be proved +AutoReq.dfy(40,11): Error: function precondition could not be proved AutoReq.dfy(5,13): Related location: this proposition could not be proved AutoReq.dfy(40,11): Error: assertion might not hold AutoReq.dfy(31,26): Related location: this proposition could not be proved AutoReq.dfy(7,4): Related location: this proposition could not be proved -AutoReq.dfy(40,11): Error: function precondition could not be proved -AutoReq.dfy(5,13): Related location: this proposition could not be proved AutoReq.dfy(45,11): Error: assertion might not hold AutoReq.dfy(31,12): Related location: this proposition could not be proved AutoReq.dfy(7,4): Related location: this proposition could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy similarity index 99% rename from Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy rename to Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy index 91e3ea6426e..ce78a8795ba 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy @@ -1,4 +1,4 @@ -// RUN: %exits-with 4 %dafny /compile:0 /deprecation:0 /autoTriggers:0 /optimizeResolution:0 /errorLimit:0 "%s" > "%t" +// RUN: %exits-with 4 %verify --allow-deprecation --manual-triggers --error-limit 0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" module TestModule1 { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy.expect new file mode 100755 index 00000000000..9263a740963 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.dfy.expect @@ -0,0 +1,67 @@ +Fuel.dfy(17,22): Error: assertion might not hold +Fuel.dfy(66,27): Error: assertion might not hold +Fuel.dfy(71,27): Error: assertion might not hold +Fuel.dfy(92,22): Error: assertion might not hold +Fuel.dfy(93,23): Error: assertion might not hold +Fuel.dfy(94,22): Error: assertion might not hold +Fuel.dfy(129,8): Error: Fuel can only increase within a given scope. +Fuel.dfy(120,22): Error: assertion might not hold +Fuel.dfy(121,23): Error: assertion might not hold +Fuel.dfy(122,22): Error: assertion might not hold +Fuel.dfy(132,26): Error: assertion might not hold +Fuel.dfy(133,26): Error: assertion might not hold +Fuel.dfy(157,22): Error: assertion might not hold +Fuel.dfy(200,55): Error: assertion might not hold +Fuel.dfy(245,22): Error: assertion might not hold +Fuel.dfy(247,22): Error: assertion might not hold +Fuel.dfy(280,26): Error: assertion might not hold +Fuel.dfy(335,26): Error: function precondition could not be proved +Fuel.dfy(324,21): Related location: this proposition could not be proved +Fuel.dfy(312,43): Related location: this proposition could not be proved +Fuel.dfy(335,26): Error: function precondition could not be proved +Fuel.dfy(324,21): Related location: this proposition could not be proved +Fuel.dfy(312,58): Related location: this proposition could not be proved +Fuel.dfy(335,26): Error: function precondition could not be proved +Fuel.dfy(324,21): Related location: this proposition could not be proved +Fuel.dfy(313,41): Related location: this proposition could not be proved +Fuel.dfy(335,26): Error: function precondition could not be proved +Fuel.dfy(324,21): Related location: this proposition could not be proved +Fuel.dfy(314,46): Related location: this proposition could not be proved +Fuel.dfy(335,26): Error: function precondition could not be proved +Fuel.dfy(324,21): Related location: this proposition could not be proved +Fuel.dfy(314,72): Related location: this proposition could not be proved +Fuel.dfy(335,26): Error: function precondition could not be proved +Fuel.dfy(324,21): Related location: this proposition could not be proved +Fuel.dfy(314,93): Related location: this proposition could not be proved +Fuel.dfy(335,49): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple' +Fuel.dfy(335,50): Error: index out of range +Fuel.dfy(336,38): Error: index out of range +Fuel.dfy(336,42): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64' +Fuel.dfy(336,45): Error: function precondition could not be proved +Fuel.dfy(329,21): Related location: this proposition could not be proved +Fuel.dfy(311,43): Related location: this proposition could not be proved +Fuel.dfy(336,45): Error: function precondition could not be proved +Fuel.dfy(329,21): Related location: this proposition could not be proved +Fuel.dfy(312,43): Related location: this proposition could not be proved +Fuel.dfy(336,45): Error: function precondition could not be proved +Fuel.dfy(329,21): Related location: this proposition could not be proved +Fuel.dfy(312,58): Related location: this proposition could not be proved +Fuel.dfy(336,45): Error: function precondition could not be proved +Fuel.dfy(329,21): Related location: this proposition could not be proved +Fuel.dfy(313,41): Related location: this proposition could not be proved +Fuel.dfy(336,45): Error: function precondition could not be proved +Fuel.dfy(329,21): Related location: this proposition could not be proved +Fuel.dfy(314,72): Related location: this proposition could not be proved +Fuel.dfy(336,45): Error: function precondition could not be proved +Fuel.dfy(329,21): Related location: this proposition could not be proved +Fuel.dfy(314,93): Related location: this proposition could not be proved +Fuel.dfy(336,71): Error: index out of range +Fuel.dfy(407,8): Error: Fuel can only increase within a given scope. +Fuel.dfy(397,22): Error: assertion might not hold +Fuel.dfy(398,22): Error: assertion might not hold +Fuel.dfy(399,23): Error: assertion might not hold +Fuel.dfy(435,22): Error: assertion might not hold +Fuel.dfy(436,22): Error: assertion might not hold +Fuel.dfy(437,23): Error: assertion might not hold + +Dafny program verifier finished with 31 verified, 39 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect deleted file mode 100755 index c5a06552f28..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect +++ /dev/null @@ -1,67 +0,0 @@ -Fuel.legacy.dfy(129,8): Error: Fuel can only increase within a given scope. -Fuel.legacy.dfy(407,8): Error: Fuel can only increase within a given scope. -Fuel.legacy.dfy(17,22): Error: assertion might not hold -Fuel.legacy.dfy(66,27): Error: assertion might not hold -Fuel.legacy.dfy(71,27): Error: assertion might not hold -Fuel.legacy.dfy(92,22): Error: assertion might not hold -Fuel.legacy.dfy(93,23): Error: assertion might not hold -Fuel.legacy.dfy(94,22): Error: assertion might not hold -Fuel.legacy.dfy(120,22): Error: assertion might not hold -Fuel.legacy.dfy(121,23): Error: assertion might not hold -Fuel.legacy.dfy(122,22): Error: assertion might not hold -Fuel.legacy.dfy(132,26): Error: assertion might not hold -Fuel.legacy.dfy(133,26): Error: assertion might not hold -Fuel.legacy.dfy(157,22): Error: assertion might not hold -Fuel.legacy.dfy(200,55): Error: assertion might not hold -Fuel.legacy.dfy(245,22): Error: assertion might not hold -Fuel.legacy.dfy(247,22): Error: assertion might not hold -Fuel.legacy.dfy(280,26): Error: assertion might not hold -Fuel.legacy.dfy(335,26): Error: function precondition could not be proved -Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(313,41): Related location -Fuel.legacy.dfy(335,26): Error: function precondition could not be proved -Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,72): Related location -Fuel.legacy.dfy(335,26): Error: function precondition could not be proved -Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,93): Related location -Fuel.legacy.dfy(335,26): Error: function precondition could not be proved -Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(314,46): Related location -Fuel.legacy.dfy(335,26): Error: function precondition could not be proved -Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(312,43): Related location -Fuel.legacy.dfy(335,26): Error: function precondition could not be proved -Fuel.legacy.dfy(324,21): Related location -Fuel.legacy.dfy(312,58): Related location -Fuel.legacy.dfy(335,49): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple' -Fuel.legacy.dfy(335,50): Error: index out of range -Fuel.legacy.dfy(336,38): Error: index out of range -Fuel.legacy.dfy(336,42): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64' -Fuel.legacy.dfy(336,45): Error: function precondition could not be proved -Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(311,43): Related location -Fuel.legacy.dfy(336,45): Error: function precondition could not be proved -Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(314,93): Related location -Fuel.legacy.dfy(336,45): Error: function precondition could not be proved -Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(312,58): Related location -Fuel.legacy.dfy(336,45): Error: function precondition could not be proved -Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(313,41): Related location -Fuel.legacy.dfy(336,45): Error: function precondition could not be proved -Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(314,72): Related location -Fuel.legacy.dfy(336,45): Error: function precondition could not be proved -Fuel.legacy.dfy(329,21): Related location -Fuel.legacy.dfy(312,43): Related location -Fuel.legacy.dfy(336,71): Error: index out of range -Fuel.legacy.dfy(397,22): Error: assertion might not hold -Fuel.legacy.dfy(398,22): Error: assertion might not hold -Fuel.legacy.dfy(399,23): Error: assertion might not hold -Fuel.legacy.dfy(435,22): Error: assertion might not hold -Fuel.legacy.dfy(436,22): Error: assertion might not hold -Fuel.legacy.dfy(437,23): Error: assertion might not hold - -Dafny program verifier finished with 31 verified, 39 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Input/IncludesTuples.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Input/IncludesTuples.dfy index 480f19bf3c7..daf58aae43e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Input/IncludesTuples.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Input/IncludesTuples.dfy @@ -1,6 +1,6 @@ // RUN: echo Input for Stdin.dfy // Note that the current directory for .NET tests is always the output directory // for the IntegrationTests project. -// i.e. something like IntegrationTests/bin/Debug/net6.0 +// i.e. something like IntegrationTests/bin/Debug/net8.0 include "TestFiles/LitTests/LitTest/dafny0/Tuples.dfy" \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/one-message-per-failed-precondition.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/one-message-per-failed-precondition.dfy.expect index 730a9d00e35..5391422767e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/one-message-per-failed-precondition.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/one-message-per-failed-precondition.dfy.expect @@ -1,10 +1,10 @@ one-message-per-failed-precondition.dfy(13,3): Error: a precondition for this call could not be proved -one-message-per-failed-precondition.dfy(9,13): Related location: this is the precondition that could not be proved -one-message-per-failed-precondition.dfy(13,3): Error: a precondition for this call could not be proved one-message-per-failed-precondition.dfy(8,13): Related location: this is the precondition that could not be proved -one-message-per-failed-precondition.dfy(20,33): Error: function precondition could not be proved -one-message-per-failed-precondition.dfy(18,13): Related location: this proposition could not be proved +one-message-per-failed-precondition.dfy(13,3): Error: a precondition for this call could not be proved +one-message-per-failed-precondition.dfy(9,13): Related location: this is the precondition that could not be proved one-message-per-failed-precondition.dfy(20,33): Error: function precondition could not be proved one-message-per-failed-precondition.dfy(17,13): Related location: this proposition could not be proved +one-message-per-failed-precondition.dfy(20,33): Error: function precondition could not be proved +one-message-per-failed-precondition.dfy(18,13): Related location: this proposition could not be proved Dafny program verifier finished with 0 verified, 4 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/Makefile b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/Makefile index 9b695cffd4d..662f746a702 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/Makefile +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/Makefile @@ -21,7 +21,7 @@ $(dafny_csharp_dir)/%.cs: %.dfy | $(dafny_csharp_dir) # Step 3: compile resulting C# project csproj := SimpleCompiler.csproj -csharp_dll := $(csharp_dir)/bin/Debug/net6.0/SimpleCompiler.dll +csharp_dll := $(csharp_dir)/bin/Debug/net8.0/SimpleCompiler.dll csharp_files := $(wildcard $(csharp_dir)/*) csharp_shared_deps := $(patsubst %,$(csharp_dir)/%,$(shared_deps)) csharp_dafny_deps := $(patsubst %.dfy,$(dafny_csharp_dir)/%.cs,$(dafny_files)) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj index c3a9eccf93e..bb542208d5a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj @@ -2,9 +2,9 @@ Exe - net6.0 + net8.0 enable - CS3021; CS0162; CS0164 + CS8981; CS3021; CS0162; CS0164 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect index 101c6a5a397..2bb07b70a75 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2299.dfy.expect @@ -7,13 +7,13 @@ git-issue-2299.dfy(21,4): Related location: this proposition could not be proved git-issue-2299.dfy(67,13): Error: assertion might not hold git-issue-2299.dfy(21,4): Related location: this proposition could not be proved git-issue-2299.dfy(81,11): Error: assertion might not hold +git-issue-2299.dfy(27,4): Related location: this proposition could not be proved +git-issue-2299.dfy(10,11): Related location: this proposition could not be proved +git-issue-2299.dfy(81,11): Error: assertion might not hold git-issue-2299.dfy(27,18): Related location: this proposition could not be proved git-issue-2299.dfy(16,4): Related location: this proposition could not be proved git-issue-2299.dfy(81,11): Error: assertion might not hold git-issue-2299.dfy(27,32): Related location: this proposition could not be proved git-issue-2299.dfy(21,4): Related location: this proposition could not be proved -git-issue-2299.dfy(81,11): Error: assertion might not hold -git-issue-2299.dfy(27,4): Related location: this proposition could not be proved -git-issue-2299.dfy(10,11): Related location: this proposition could not be proved Dafny program verifier finished with 7 verified, 7 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect index 32d93e22db0..3ccac32363e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect @@ -1 +1 @@ -Invalid filename: The path is empty. (Parameter 'path') +Invalid filename: The value cannot be an empty string. (Parameter 'path') diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect index f049bcc234c..4f6393dcb36 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.expect @@ -19,10 +19,10 @@ InductionWithoutTriggers.dfy(100,0): Error: a postcondition could not be proved InductionWithoutTriggers.dfy(99,10): Related location: this is the postcondition that could not be proved InductionWithoutTriggers.dfy(31,27): Related location: this proposition could not be proved InductionWithoutTriggers.dfy(124,0): Error: a postcondition could not be proved on this return path -InductionWithoutTriggers.dfy(123,18): Related location: this is the postcondition that could not be proved -InductionWithoutTriggers.dfy(35,27): Related location: this proposition could not be proved -InductionWithoutTriggers.dfy(124,0): Error: a postcondition could not be proved on this return path InductionWithoutTriggers.dfy(123,10): Related location: this is the postcondition that could not be proved InductionWithoutTriggers.dfy(31,27): Related location: this proposition could not be proved +InductionWithoutTriggers.dfy(124,0): Error: a postcondition could not be proved on this return path +InductionWithoutTriggers.dfy(123,18): Related location: this is the postcondition that could not be proved +InductionWithoutTriggers.dfy(35,27): Related location: this proposition could not be proved Dafny program verifier finished with 17 verified, 8 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.refresh.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.refresh.expect index 963b7041fd6..566c53271f8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.refresh.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/triggers/InductionWithoutTriggers.dfy.refresh.expect @@ -19,10 +19,10 @@ InductionWithoutTriggers.dfy(100,0): Error: a postcondition could not be proved InductionWithoutTriggers.dfy(99,10): Related location: this is the postcondition that could not be proved InductionWithoutTriggers.dfy(31,27): Related location: this proposition could not be proved InductionWithoutTriggers.dfy(124,0): Error: a postcondition could not be proved on this return path -InductionWithoutTriggers.dfy(123,18): Related location: this is the postcondition that could not be proved -InductionWithoutTriggers.dfy(35,27): Related location: this proposition could not be proved -InductionWithoutTriggers.dfy(124,0): Error: a postcondition could not be proved on this return path InductionWithoutTriggers.dfy(123,10): Related location: this is the postcondition that could not be proved InductionWithoutTriggers.dfy(31,27): Related location: this proposition could not be proved +InductionWithoutTriggers.dfy(124,0): Error: a postcondition could not be proved on this return path +InductionWithoutTriggers.dfy(123,18): Related location: this is the postcondition that could not be proved +InductionWithoutTriggers.dfy(35,27): Related location: this proposition could not be proved Dafny program verifier finished with 12 verified, 8 errors diff --git a/Source/TestDafny/TestDafny.csproj b/Source/TestDafny/TestDafny.csproj index 83f292e7923..4865653669c 100644 --- a/Source/TestDafny/TestDafny.csproj +++ b/Source/TestDafny/TestDafny.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 enable enable false diff --git a/Source/XUnitExtensions/Lit/DiffCommand.cs b/Source/XUnitExtensions/Lit/DiffCommand.cs index ad79003bfe3..f4060abbfb0 100644 --- a/Source/XUnitExtensions/Lit/DiffCommand.cs +++ b/Source/XUnitExtensions/Lit/DiffCommand.cs @@ -35,7 +35,7 @@ public static ILitCommand Parse(string[] args) { if (Path.GetExtension(expectedOutputFile) == ".tmp") { return "With DAFNY_INTEGRATION_TESTS_UPDATE_EXPECT_FILE=true, first argument of %diff cannot be a *.tmp file, it should be an *.expect file"; } - var path = Path.GetFullPath(expectedOutputFile).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net6.0" + Path.DirectorySeparatorChar, ""); + var path = Path.GetFullPath(expectedOutputFile).Replace("bin" + Path.DirectorySeparatorChar + "Debug" + Path.DirectorySeparatorChar + "net8.0" + Path.DirectorySeparatorChar, ""); File.WriteAllText(path, actualOutput); return null; } diff --git a/Source/XUnitExtensions/XUnitExtensions.csproj b/Source/XUnitExtensions/XUnitExtensions.csproj index 3ff901352c0..3ee91d23d07 100644 --- a/Source/XUnitExtensions/XUnitExtensions.csproj +++ b/Source/XUnitExtensions/XUnitExtensions.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 false enable diff --git a/customBoogie.patch b/customBoogie.patch index 911dc435a47..9887a911223 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -73,6 +73,6 @@ index 4a8b2f89b..a308be9bf 100644 + + + - + diff --git a/docs/DafnyRef/Plugins.md b/docs/DafnyRef/Plugins.md index 6cb7c29f1df..c044914d6a0 100644 --- a/docs/DafnyRef/Plugins.md +++ b/docs/DafnyRef/Plugins.md @@ -230,6 +230,6 @@ That's it! Now, build your library while inside your folder: > dotnet build ``` -This will create the file `PluginTutorial/bin/Debug/net6.0/PluginTutorial.dll`. +This will create the file `PluginTutorial/bin/Debug/net8.0/PluginTutorial.dll`. Now, open VSCode, open Dafny settings, and enter the absolute path to this DLL in the plugins section. Restart VSCode, and it should work! diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 156cb2b049f..578b63c6924 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -2732,7 +2732,7 @@ If you have Boogie installed locally, you can run the printed Boogie file with t DOTNET=$(which dotnet) BOOGIE_ROOT="path/to/boogie/Source" -BOOGIE="$BOOGIE_ROOT/BoogieDriver/bin/Debug/net6.0/BoogieDriver.dll" +BOOGIE="$BOOGIE_ROOT/BoogieDriver/bin/Debug/net8.0/BoogieDriver.dll" if [[ ! -x "$DOTNET" ]]; then echo "Error: Dafny requires .NET Core to run on non-Windows systems." diff --git a/docs/Installation.md b/docs/Installation.md index edecd0f3928..991e4b06b42 100644 --- a/docs/Installation.md +++ b/docs/Installation.md @@ -15,7 +15,7 @@ are in the [Dafny project wiki](https://github.com/dafny-lang/dafny/wiki/INSTALL System Requirements =================== -The `dafny tool` is a .NET 6.0 artifact, but it compiles to native executables on supported platforms. +The `dafny tool` is a .NET 8.0 artifact, but it compiles to native executables on supported platforms. That and the Z3 tool are all that is needed to use dafny for verification; additional tools are need for compilation, as described below. @@ -41,7 +41,7 @@ In addition, the Dafny toolkit supplies runtime libraries, either in source form ### C# - Dafny targeting C# produces C#10-compatible source code. -- Only the .NET 6.0 set of tools (which includes the C# compiler) is needed to compile and run the generated C# code. +- Only the .NET 8.0 set of tools (which includes the C# compiler) is needed to compile and run the generated C# code. - The Dafny runtime library is included as C# source along with the generated C# code, so the user can compile those sources and any user code in one project. @@ -86,9 +86,9 @@ For most users, we recommend using Dafny with VS Code, which has an easy install ## Visual Studio Code {#Visual-Studio-Code} 0. Install [Visual Studio Code](https://code.visualstudio.com/) -1. If you are on a Mac or Linux, install .NET 6.0, as described under those platforms below. +1. If you are on a Mac or Linux, install .NET 8.0, as described under those platforms below. 2. In Visual Studio Code, press `Ctrl+P` (or `⌘P` on a Mac), and enter `ext install dafny-lang.ide-vscode`. -3. If you open a `.dfy` file, Dafny VSCode will offer to download and install the latest Dafny. You can also browse extensions: +3. If you open a `.dfy` file, Dafny VSCode will offer to download and install the latest Dafny. You can also browse extensions: ![vs-code-dafny-2 0 1-install](https://user-images.githubusercontent.com/3601079/141353551-5cb5e23b-5536-47be-ba17-e5af494b775c.gif) ## Emacs {#Emacs} @@ -118,7 +118,7 @@ install the correct dependencies for the desired language. To install Dafny on your own machine, -* Install (if not already present) .NET Core 6.0: `https://dotnet.microsoft.com/download/dotnet/6.0` +* Install (if not already present) .NET Core 8.0: `https://dotnet.microsoft.com/download/dotnet/8.0` * Download the windows zip file from the [releases page](https://github.com/dafny-lang/dafny/releases/latest) and **save** it to your disk. * Then, **before you open or unzip it**, right-click on it and select Properties; at the bottom of the dialog, click the **Unblock** button and then the OK button. * Now, open the zip file and copy its contents into a directory on your machine. (You can now delete the zip file.) @@ -130,7 +130,7 @@ Then: ## Linux (Binary) {#linux-binary} To install a binary installation of dafny on Linux (e.g., Ubuntu), do the following: -* Install .NET 6.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-6.0` +* Install .NET 8.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-8.0` * Install the Linux binary version of Dafny, from `https://github.com/dafny-lang/dafny/releases/latest` * Unzip the downloaded file in a (empty) location of your choice @@ -165,7 +165,7 @@ After the compiler dependencies are installed, you can run a quick test of the i The .NET [NuGet](https://www.nuget.org/) repository collects .NET libraries and tools for easy installation. Dafny is available on NuGet, and can be installed as follows: -* Install .NET 6.0 as described for your platform in one of the subsections above. +* Install .NET 8.0 as described for your platform in one of the subsections above. * Install a binary version of Z3 4.12.1 for your platform from its [GitHub releases page](https://github.com/Z3Prover/z3/releases/tag/Z3-4.12.1) and put the `z3` executable in your `PATH`. * Install Dafny using `dotnet tool install --global dafny` (or leave out the `--global` to use with `dotnet tool run` from the source directory of a .NET project). @@ -181,10 +181,10 @@ Additional instructions are found in the [Dafny User Guide](DafnyRef/DafnyRef#se ### C# (.Net) -Install .NET 6.0: -* Windows) `https://dotnet.microsoft.com/download/dotnet/6.0` -* Linux) Install .NET 6.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-6.0` -* Mac) Install .NET 6.0: `brew install dotnet-sdk` or from `https://docs.microsoft.com/dotnet/core/install/macos` +Install .NET 8.0: +* Windows) `https://dotnet.microsoft.com/download/dotnet/8.0` +* Linux) Install .NET 8.0. See: `https://docs.microsoft.com/dotnet/core/install/linux` or `sudo apt install dotnet-sdk-8.0` +* Mac) Install .NET 8.0: `brew install dotnet-sdk` or from `https://docs.microsoft.com/dotnet/core/install/macos` To separately compile and run your program for .NET: diff --git a/docs/OnlineTutorial/guide.10.expect b/docs/OnlineTutorial/guide.10.expect index e714f865f0b..6a7d67a8974 100644 --- a/docs/OnlineTutorial/guide.10.expect +++ b/docs/OnlineTutorial/guide.10.expect @@ -1,14 +1,14 @@ text.dfy(7,0): Error: a postcondition could not be proved on this return path +text.dfy(4,12): Related location: this is the postcondition that could not be proved +text.dfy(7,0): Error: a postcondition could not be proved on this return path text.dfy(5,23): Related location: this is the postcondition that could not be proved text.dfy(7,0): Error: a postcondition could not be proved on this return path text.dfy(6,22): Related location: this is the postcondition that could not be proved -text.dfy(7,0): Error: a postcondition could not be proved on this return path -text.dfy(4,12): Related location: this is the postcondition that could not be proved +text.dfy(16,0): Error: a postcondition could not be proved on this return path +text.dfy(13,12): Related location: this is the postcondition that could not be proved text.dfy(16,0): Error: a postcondition could not be proved on this return path text.dfy(14,23): Related location: this is the postcondition that could not be proved text.dfy(16,0): Error: a postcondition could not be proved on this return path text.dfy(15,22): Related location: this is the postcondition that could not be proved -text.dfy(16,0): Error: a postcondition could not be proved on this return path -text.dfy(13,12): Related location: this is the postcondition that could not be proved Dafny program verifier finished with 0 verified, 6 errors From c79cb5e55aa45ce584e12dd308251f799163f5b3 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Thu, 9 Jan 2025 20:24:57 +0100 Subject: [PATCH 2/4] Set a default verification time limit (#6028) Fixes https://github.com/dafny-lang/ide-vscode/issues/514 ### What was changed? Set a default verification time limit ### How has this been tested? Added a CLI test that checks there is a default time-out 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). --- Source/DafnyCore/Options/BoogieOptionBag.cs | 4 +- Source/DafnyCore/Pipeline/Compilation.cs | 96 +++++++++++++++++-- .../LitTests/LitTest/cli/defaultTimeLimit.dfy | 17 ++++ .../LitTest/cli/defaultTimeLimit.dfy.expect | 7 ++ .../git-issues/git-issue-3855.dfy.expect | 2 +- docs/DafnyRef/UserGuide.md | 2 +- docs/news/{fix.6006 => 6006.fix} | 0 docs/news/6028.feat | 1 + 8 files changed, 117 insertions(+), 12 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect rename docs/news/{fix.6006 => 6006.fix} (100%) create mode 100644 docs/news/6028.feat diff --git a/Source/DafnyCore/Options/BoogieOptionBag.cs b/Source/DafnyCore/Options/BoogieOptionBag.cs index 2983c3dbf3b..59ffe8bfcbe 100644 --- a/Source/DafnyCore/Options/BoogieOptionBag.cs +++ b/Source/DafnyCore/Options/BoogieOptionBag.cs @@ -51,8 +51,8 @@ public static class BoogieOptionBag { IsHidden = true }; - public static readonly Option VerificationTimeLimit = new("--verification-time-limit", - "Limit the number of seconds spent trying to verify each procedure") { + public static readonly Option VerificationTimeLimit = new("--verification-time-limit", () => 30, + "Limit the number of seconds spent trying to verify each assertion batch. A value of 0 indicates no limit") { ArgumentHelpName = "seconds", }; diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index d89a6b973fd..0ecaadeae78 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -4,6 +4,7 @@ using System.Collections.Concurrent; using System.Collections.Generic; using System.CommandLine; +using System.CommandLine.Help; using System.IO; using System.Linq; using System.Reactive; @@ -560,17 +561,96 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, string name, errorReporter.ReportBoogieError(errorInformation, dafnyCounterExampleModel); } - // This reports problems that are not captured by counter-examples, like a time-out - // The Boogie API forces us to create a temporary engine here to report the outcome, even though it only uses the options. - var boogieEngine = new ExecutionEngine(options, new EmptyVerificationResultCache(), - CustomStackSizePoolTaskScheduler.Create(0, 0)); - boogieEngine.ReportOutcome(null, outcome, outcomeError => errorReporter.ReportBoogieError(outcomeError, null, false), - name, token, null, TextWriter.Null, - timeLimit, result.CounterExamples); + var outcomeError = ReportOutcome(options, outcome, name, token, timeLimit, result.CounterExamples); + if (outcomeError != null) { + errorReporter.ReportBoogieError(outcomeError, null, false); + } + } + + private static ErrorInformation? ReportOutcome(DafnyOptions options, + VcOutcome vcOutcome, string name, + IToken token, uint timeLimit, List errors) { + ErrorInformation? errorInfo = null; + + switch (vcOutcome) { + case VcOutcome.Correct: + break; + case VcOutcome.Errors: + case VcOutcome.TimedOut: { + if (vcOutcome != VcOutcome.TimedOut && + (!errors.Any(e => e.IsAuxiliaryCexForDiagnosingTimeouts))) { + break; + } + + string msg = string.Format("Verification of '{1}' timed out after {0} seconds. (the limit can be increased using --verification-time-limit)", timeLimit, name); + errorInfo = ErrorInformation.Create(token, msg); + + // Report timed out assertions as auxiliary info. + var comparer = new CounterexampleComparer(); + var timedOutAssertions = errors.Where(e => e.IsAuxiliaryCexForDiagnosingTimeouts).Distinct(comparer) + .OrderBy(x => x, comparer).ToList(); + if (0 < timedOutAssertions.Count) { + errorInfo!.Msg += $" with {timedOutAssertions.Count} check(s) that timed out individually"; + } + + foreach (Counterexample error in timedOutAssertions) { + IToken tok; + string auxMsg = null!; + switch (error) { + case CallCounterexample callCounterexample: + tok = callCounterexample.FailingCall.tok; + auxMsg = callCounterexample.FailingCall.Description.FailureDescription; + break; + case ReturnCounterexample returnCounterexample: + tok = returnCounterexample.FailingReturn.tok; + auxMsg = returnCounterexample.FailingReturn.Description.FailureDescription; + break; + case AssertCounterexample assertError: { + tok = assertError.FailingAssert.tok; + if (!(assertError.FailingAssert.ErrorMessage == null || + ((ExecutionEngineOptions)options).ForceBplErrors)) { + auxMsg = assertError.FailingAssert.ErrorMessage; + } + + auxMsg ??= assertError.FailingAssert.Description.FailureDescription; + break; + } + default: throw new Exception(); + } + + errorInfo.AddAuxInfo(tok, auxMsg, "Unverified check due to timeout"); + } + + break; + } + case VcOutcome.OutOfResource: { + string msg = "Verification out of resource (" + name + ")"; + errorInfo = ErrorInformation.Create(token, msg); + } + break; + case VcOutcome.OutOfMemory: { + string msg = "Verification out of memory (" + name + ")"; + errorInfo = ErrorInformation.Create(token, msg); + } + break; + case VcOutcome.SolverException: { + string msg = "Verification encountered solver exception (" + name + ")"; + errorInfo = ErrorInformation.Create(token, msg); + } + break; + + case VcOutcome.Inconclusive: { + string msg = "Verification inconclusive (" + name + ")"; + errorInfo = ErrorInformation.Create(token, msg); + } + break; + } + + return errorInfo; } private static void AddAssertedExprToCounterExampleErrorInfo( - DafnyOptions options, Counterexample counterExample, ErrorInformation errorInformation) { + DafnyOptions options, Counterexample counterExample, ErrorInformation errorInformation) { Boogie.ProofObligationDescription? boogieProofObligationDesc = null; switch (errorInformation.Kind) { case ErrorKind.Assertion: diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy new file mode 100644 index 00000000000..e91e3331f33 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy @@ -0,0 +1,17 @@ +// RUN: ! %baredafny verify --use-basename-for-filename "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method Foo() { + // Assert something that takes a long time to verify + assert Ack(4, 2) == 1; +} + +function Ack(m: nat, n: nat): nat +{ + if m == 0 then + n + 1 + else if n == 0 then + Ack(m - 1, 1) + else + Ack(m - 1, Ack(m, n - 1)) +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect new file mode 100644 index 00000000000..b7677c39850 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/defaultTimeLimit.dfy.expect @@ -0,0 +1,7 @@ +defaultTimeLimit.dfy(4,7): Error: Verification of 'Foo' timed out after 30 seconds. (the limit can be increased using --verification-time-limit) + | +4 | method Foo() { + | ^^^ + + +Dafny program verifier finished with 1 verified, 0 errors, 1 time out diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect index e7965e56414..2c2bc4bc249 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3855.dfy.expect @@ -1,5 +1,5 @@ git-issue-3855.dfy(799,0): Warning: attribute :ignore is deprecated -git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after seconds +git-issue-3855.dfy(799,11): Error: Verification of 'Memory.dynMove' timed out after seconds. (the limit can be increased using --verification-time-limit) git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved git-issue-3855.dfy(430,29): Related location: this is the precondition that could not be proved git-issue-3855.dfy(942,17): Error: a precondition for this call could not be proved diff --git a/docs/DafnyRef/UserGuide.md b/docs/DafnyRef/UserGuide.md index 578b63c6924..8fd4ce1c5dc 100644 --- a/docs/DafnyRef/UserGuide.md +++ b/docs/DafnyRef/UserGuide.md @@ -2769,7 +2769,7 @@ The following options are also commonly used: but a large positive number reports more errors per run * `--verification-time-limit:` (was `-timeLimit:`) - limits - the number of seconds spent trying to verify each procedure. + the number of seconds spent trying to verify each assertion batch. ### 13.9.11. Controlling test generation {#sec-controlling-test-gen} diff --git a/docs/news/fix.6006 b/docs/news/6006.fix similarity index 100% rename from docs/news/fix.6006 rename to docs/news/6006.fix diff --git a/docs/news/6028.feat b/docs/news/6028.feat new file mode 100644 index 00000000000..2bfb7957467 --- /dev/null +++ b/docs/news/6028.feat @@ -0,0 +1 @@ +Change the default value for --verification-time-limit to 30 seconds instead of 0 (no limit) \ No newline at end of file From 0edf705ee7a5a53cc496d1718aa36351d10fb3d2 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 10 Jan 2025 15:20:59 +0100 Subject: [PATCH 3/4] Attempt at fixing nightly. (#6035) ### What was changed? - Remove the `$(RUNTIME_IDENTIFIER)` property from csproj files that was needed as a workaround but may break things in .NET 8 according to SO - Remove references from DafnyDriver to DafnyServer, that prevented publishing correctly with .NET 8 - Stop publishing DafnyLanguageServer since it's not used directly. ### How has this been tested? Tested by existing tests 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). --- .github/workflows/integration-tests-reusable.yml | 5 +++++ Scripts/package.py | 1 - Source/DafnyDriver/Commands/ServerCommand.cs | 2 -- Source/DafnyDriver/DafnyDriver.csproj | 12 +----------- .../Legacy/LegacyJsonVerificationLogger.cs | 1 - .../DafnyLanguageServer/DafnyLanguageServer.csproj | 1 - Source/DafnyServer/DafnyServer.csproj | 10 ---------- .../DafnyTestGeneration/DafnyTestGeneration.csproj | 1 - 8 files changed, 6 insertions(+), 27 deletions(-) diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index 3109c167ccb..79d72f30dcf 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.github/workflows/integration-tests-reusable.yml @@ -72,6 +72,11 @@ jobs: uses: actions/setup-dotnet@v4 with: dotnet-version: ${{ env.dotnet-version }} + # Setup dotnet 6.0 for running Boogie. Alternatively we could try running Boogie with a roll forward policy, or updating Boogie. + - name: Setup dotnet + uses: actions/setup-dotnet@v4 + with: + dotnet-version: 6.0.x - name: C++ for ubuntu 20.04 if: matrix.os == 'ubuntu-20.04' run: | diff --git a/Scripts/package.py b/Scripts/package.py index f543d37715c..aaffbfe4e20 100755 --- a/Scripts/package.py +++ b/Scripts/package.py @@ -161,7 +161,6 @@ def build(self): if path.exists(self.buildDirectory): shutil.rmtree(self.buildDirectory) run(["make", "--quiet", "clean"]) - self.run_publish("DafnyLanguageServer") self.run_publish("DafnyServer") self.run_publish("DafnyRuntime", "netstandard2.0") self.run_publish("DafnyRuntime", "net452") diff --git a/Source/DafnyDriver/Commands/ServerCommand.cs b/Source/DafnyDriver/Commands/ServerCommand.cs index a4cdf8c92b3..51381672ef5 100644 --- a/Source/DafnyDriver/Commands/ServerCommand.cs +++ b/Source/DafnyDriver/Commands/ServerCommand.cs @@ -1,6 +1,4 @@ -using System.Collections.Generic; using System.CommandLine; -using DafnyCore; using Microsoft.Dafny.LanguageServer.Language; using Microsoft.Dafny.LanguageServer.Language.Symbols; using Microsoft.Dafny.LanguageServer.Workspace; diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index f928e3f5043..0236f2ce5f6 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -13,16 +13,6 @@ true - - - false - false - - - - - $(RUNTIME_IDENTIFIER) - @@ -42,8 +32,8 @@ + - diff --git a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs index 93087fe8e5d..e6e27c8b151 100644 --- a/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs +++ b/Source/DafnyDriver/Legacy/LegacyJsonVerificationLogger.cs @@ -4,7 +4,6 @@ using System.Linq; using System.Text.Json.Nodes; using DafnyCore.Verifier; -using DafnyServer; using Microsoft.Boogie; using VC; diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj index 67513425d4e..92f1fad7dff 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj @@ -6,7 +6,6 @@ enable Microsoft.Dafny.LanguageServer ..\..\Binaries\ - true false MIT README.md diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index d736ee1074e..f9cd46eb532 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -10,16 +10,6 @@ MIT - - false - false - - - - - $(RUNTIME_IDENTIFIER) - - diff --git a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj index 016cf01c491..f4f2f78ffd1 100644 --- a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj +++ b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj @@ -15,7 +15,6 @@ - From 8ede38cda6543763c3d6684f7f01ffbd9df492dc Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 10 Jan 2025 21:14:55 +0100 Subject: [PATCH 4/4] Delete test for legacy CLI that tests broken behavior (#6037) ### What was changed? The Dafny legacy CLI shows part of a .NET error message as part of it UI. This can not be tested well since the specific error message is not defined as part of .NET, and can be different across .NET versions and platforms. On Windows it returns: `Invalid filename: The value cannot be an empty string. (Parameter 'path')` On other platforms it is: `Invalid filename: The path is empty. (Parameter 'path')` Instead of fixing the legacy CLI to remove the ambiguity, I'm removing the test for that ambiguous behavior since the old CLI is deprecated. ### How has this been tested? Removed a test 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). --- .../TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy | 2 -- .../LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect | 1 - 2 files changed, 3 deletions(-) delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy delete mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy deleted file mode 100644 index 9ce07b0f267..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy +++ /dev/null @@ -1,2 +0,0 @@ -// RUN: %exits-with 1 %baredafny "" 2> "%t" -// RUN: %diff "%s.expect" "%t" diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect deleted file mode 100644 index 3ccac32363e..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect +++ /dev/null @@ -1 +0,0 @@ -Invalid filename: The value cannot be an empty string. (Parameter 'path')