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..79d72f30dcf 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. @@ -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/.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/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/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/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/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/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/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..0236f2ce5f6 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -5,8 +5,7 @@ DafnyDriver false TRACE - net6.0 -Major + Major ..\..\Binaries\ false @@ -14,16 +13,6 @@ true - - - false - false - - - - - $(RUNTIME_IDENTIFIER) - @@ -43,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.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..92f1fad7dff 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj @@ -1,19 +1,17 @@  - net6.0 -Major + Major true enable Microsoft.Dafny.LanguageServer ..\..\Binaries\ - true false MIT 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..f9cd46eb532 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -5,22 +5,11 @@ DafnyServer false TRACE - net6.0 -Major + Major ..\..\Binaries\ MIT - - false - false - - - - - $(RUNTIME_IDENTIFIER) - - 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..f4f2f78ffd1 100644 --- a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj +++ b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj @@ -8,15 +8,13 @@ ..\..\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/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/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 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 32d93e22db0..00000000000 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3549a.dfy.expect +++ /dev/null @@ -1 +0,0 @@ -Invalid filename: The path is empty. (Parameter 'path') 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/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..8fd4ce1c5dc 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." @@ -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/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 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