diff --git a/.github/workflows/doc-tests.yml b/.github/workflows/doc-tests.yml index c6a68115327..1c058b850b5 100644 --- a/.github/workflows/doc-tests.yml +++ b/.github/workflows/doc-tests.yml @@ -36,12 +36,11 @@ jobs: submodules: recursive path: dafny - name: Load Z3 + with: + path: dafny run: | sudo apt-get install -qq libarchive-tools - mkdir -p dafny/Binaries/z3/bin - wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf - - mv z3-* dafny/Binaries/z3/bin/ - chmod +x dafny/Binaries/z3/bin/z3-* + make z3-ubuntu - name: Build Dafny run: dotnet build dafny/Source/Dafny.sln - name: Check generated error catalog diff --git a/.github/workflows/release-downloads-nuget.yml b/.github/workflows/release-downloads-nuget.yml index c2307def244..09c25932a11 100644 --- a/.github/workflows/release-downloads-nuget.yml +++ b/.github/workflows/release-downloads-nuget.yml @@ -32,7 +32,7 @@ jobs: fail-fast: false matrix: # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906 - os: [ ubuntu-22.04, ubuntu-20.04, macos-11, windows-2019 ] + os: [ ubuntu-22.04, ubuntu-20.04, macos-13, windows-2019 ] steps: - name: OS diff --git a/.github/workflows/release-downloads.yml b/.github/workflows/release-downloads.yml index 87ddc114722..74c68178672 100644 --- a/.github/workflows/release-downloads.yml +++ b/.github/workflows/release-downloads.yml @@ -25,7 +25,7 @@ jobs: - os: 'ubuntu-20.04' osn: 'ubuntu-20.04' - os: 'macos-13' - osn: 'x64-macos-11' + osn: 'x64-macos-13' - os: 'windows-2019' osn: 'windows-2019' # There is no hosted environment for Ubuntu 14.04 or for debian diff --git a/.github/workflows/standard-libraries.yml b/.github/workflows/standard-libraries.yml index 0c1ffc6ea17..dd966bbc82f 100644 --- a/.github/workflows/standard-libraries.yml +++ b/.github/workflows/standard-libraries.yml @@ -17,7 +17,7 @@ jobs: build: needs: check-deep-tests if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' ))) - runs-on: macos-11 + runs-on: macos-13 steps: - name: Checkout Dafny diff --git a/.github/workflows/xunit-tests-reusable.yml b/.github/workflows/xunit-tests-reusable.yml index bb8c4e4bb33..68576f2315f 100644 --- a/.github/workflows/xunit-tests-reusable.yml +++ b/.github/workflows/xunit-tests-reusable.yml @@ -49,10 +49,10 @@ jobs: strategy: fail-fast: false matrix: - os: [ubuntu-20.04, windows-2019, macos-11] + os: [ubuntu-20.04, windows-2019, macos-13] iteration: ${{ fromJson(needs.populate-matrix-dimensions.outputs.iterations) }} include: - - os: macos-11 + - os: macos-13 suffix: osx chmod: true - os: windows-2019 @@ -63,7 +63,7 @@ jobs: chmod: true env: solutionPath: Source/Dafny.sln - z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02 + z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10 Logging__LogLevel__Microsoft: Debug steps: - uses: actions/checkout@v4 diff --git a/.gitmodules b/.gitmodules index aa94f844181..e5dec47b942 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,6 @@ [submodule "Test/libraries"] path = Source/IntegrationTests/TestFiles/LitTests/LitTest/libraries url = https://github.com/dafny-lang/libraries.git +[submodule "boogie"] + path = boogie + url = git@github.com:keyboardDrummer/boogie.git diff --git a/Binaries/.gitignore b/Binaries/.gitignore deleted file mode 100644 index 1e1e2a09ca6..00000000000 --- a/Binaries/.gitignore +++ /dev/null @@ -1 +0,0 @@ -DafnyRuntime.jar diff --git a/Makefile b/Makefile index d6d9295fa64..7c36a74f97c 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,5 @@ DIR=$(realpath $(dir $(firstword $(MAKEFILE_LIST)))) +BIN=$(DIR)/Binaries/net8.0/ default: exe @@ -39,37 +40,37 @@ refman-release: exe make -C "${DIR}"/docs/DafnyRef release z3-mac: - mkdir -p "${DIR}"/Binaries/z3/bin - wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-macos-11-bin.zip - unzip z3-4.12.1-x64-macos-11-bin.zip - rm z3-4.12.1-x64-macos-11-bin.zip - wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip - unzip z3-4.8.5-x64-macos-11-bin.zip - rm z3-4.8.5-x64-macos-11-bin.zip - mv z3-* "${DIR}"/Binaries/z3/bin/ - chmod +x "${DIR}"/Binaries/z3/bin/z3-* + mkdir -p "${BIN}"/z3/bin + wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10/z3-4.12.1-x64-macos-13-bin.zip + unzip z3-4.12.1-x64-macos-13-bin.zip + rm z3-4.12.1-x64-macos-13-bin.zip + wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10/z3-4.12.6-x64-macos-13-bin.zip + unzip z3-4.12.6-x64-macos-13-bin.zip + rm z3-4.12.6-x64-macos-13-bin.zip + mv z3-* "${BIN}"/z3/bin/ + chmod +x "${BIN}"/z3/bin/z3-* z3-mac-arm: - mkdir -p "${DIR}"/Binaries/z3/bin - wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-arm64-macos-11-bin.zip - unzip z3-4.12.1-arm64-macos-11-bin.zip - rm z3-4.12.1-arm64-macos-11-bin.zip - wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip - unzip z3-4.8.5-x64-macos-11-bin.zip - rm z3-4.8.5-x64-macos-11-bin.zip - mv z3-* "${DIR}"/Binaries/z3/bin/ - chmod +x "${DIR}"/Binaries/z3/bin/z3-* + mkdir -p "${BIN}"/z3/bin + wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10/z3-4.12.1-arm64-macos-13-bin.zip + unzip z3-4.12.1-arm64-macos-13-bin.zip + rm z3-4.12.1-arm64-macos-13-bin.zip + wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10/z3-4.12.6-x64-macos-13-bin.zip + unzip z3-4.12.6-x64-macos-13-bin.zip + rm z3-4.12.6-x64-macos-13-bin.zip + mv z3-* "${BIN}"/z3/bin/ + chmod +x "${BIN}"/z3/bin/z3-* z3-ubuntu: - mkdir -p "${DIR}"/Binaries/z3/bin - wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip + mkdir -p "${BIN}"/z3/bin + wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10/z3-4.12.1-x64-ubuntu-20.04-bin.zip unzip z3-4.12.1-x64-ubuntu-20.04-bin.zip rm z3-4.12.1-x64-ubuntu-20.04-bin.zip - wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-ubuntu-20.04-bin.zip - unzip z3-4.8.5-x64-ubuntu-20.04-bin.zip - rm z3-4.8.5-x64-ubuntu-20.04-bin.zip - mv z3-* "${DIR}"/Binaries/z3/bin/ - chmod +x "${DIR}"/Binaries/z3/bin/z3-* + wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10/z3-4.12.6-x64-ubuntu-20.04-bin.zip + unzip z3-4.12.6-x64-ubuntu-20.04-bin.zip + rm z3-4.12.6-x64-ubuntu-20.04-bin.zip + mv z3-* "${BIN}"/z3/bin/ + chmod +x "${BIN}"/z3/bin/z3-* format: dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs diff --git a/Scripts/dafny b/Scripts/dafny index ab813e0ca37..2b84c32dc1b 100755 --- a/Scripts/dafny +++ b/Scripts/dafny @@ -17,7 +17,7 @@ if [ "${MY_OS:0:5}" == "MINGW" ] || [ "${MY_OS:0:6}" == "CYGWIN" ]; then else DAFNY_EXE_NAME="Dafny.dll" fi -DAFNY="$DAFNY_ROOT/Binaries/$DAFNY_EXE_NAME" +DAFNY="$DAFNY_ROOT/Binaries/net8.0/$DAFNY_EXE_NAME" if [[ ! -e "$DAFNY" ]]; then echo "Error: $DAFNY_EXE_NAME not found at $DAFNY." exit 1 diff --git a/Source/AutoExtern.Test/AutoExtern.Test.csproj b/Source/AutoExtern.Test/AutoExtern.Test.csproj index 0c4e1dc0b51..4947cc7ecaf 100644 --- a/Source/AutoExtern.Test/AutoExtern.Test.csproj +++ b/Source/AutoExtern.Test/AutoExtern.Test.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.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..16692440fb3 100644 --- a/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj +++ b/Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 enable 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.sln b/Source/Dafny.sln index 23297b185ed..fc8e8b1fa49 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln @@ -43,6 +43,32 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}" EndProject +Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Boogie", "Boogie", "{60332269-9C5D-465E-8582-01F9B738BD90}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BaseTypes", "..\boogie\Source\BaseTypes\BaseTypes.csproj", "{68721962-0D91-4355-BC94-BE1CCBD30E47}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbstractInterpretation", "..\boogie\Source\AbstractInterpretation\AbstractInterpretation.csproj", "{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj", "{09662044-5640-4785-92E3-2F7CDBA4DDB2}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "..\boogie\Source\Concurrency\Concurrency.csproj", "{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "..\boogie\Source\Core\Core.csproj", "{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj", "{0145DC89-7243-41F8-AB3E-F716F04E9BFF}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "..\boogie\Source\Graph\Graph.csproj", "{05DE24BB-D639-40C4-894F-701652F51559}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "..\boogie\Source\Houdini\Houdini.csproj", "{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\boogie\Source\Model\Model.csproj", "{D97C23B6-FB4A-4450-930E-58EC83D308A0}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "..\boogie\Source\Provers\SMTLib\SMTLib.csproj", "{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}" +EndProject EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution @@ -138,5 +164,17 @@ Global SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187} EndGlobalSection GlobalSection(NestedProjects) = preSolution + {68721962-0D91-4355-BC94-BE1CCBD30E47} = {60332269-9C5D-465E-8582-01F9B738BD90} + {2A6B36F4-9F15-459A-8EDB-5BAEED98FE17} = {60332269-9C5D-465E-8582-01F9B738BD90} + {09662044-5640-4785-92E3-2F7CDBA4DDB2} = {60332269-9C5D-465E-8582-01F9B738BD90} + {DA8A9BA8-9BBA-4C64-9736-FD967517DCA9} = {60332269-9C5D-465E-8582-01F9B738BD90} + {2BF5ECCA-24B2-4A4B-86B6-D0DB17331109} = {60332269-9C5D-465E-8582-01F9B738BD90} + {0145DC89-7243-41F8-AB3E-F716F04E9BFF} = {60332269-9C5D-465E-8582-01F9B738BD90} + {05DE24BB-D639-40C4-894F-701652F51559} = {60332269-9C5D-465E-8582-01F9B738BD90} + {51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6} = {60332269-9C5D-465E-8582-01F9B738BD90} + {D97C23B6-FB4A-4450-930E-58EC83D308A0} = {60332269-9C5D-465E-8582-01F9B738BD90} + {0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F} = {60332269-9C5D-465E-8582-01F9B738BD90} + {E760E37E-0257-4C96-89C4-722F85BABDBB} = {60332269-9C5D-465E-8582-01F9B738BD90} + {1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90} EndGlobalSection EndGlobal diff --git a/Source/Dafny/Dafny.csproj b/Source/Dafny/Dafny.csproj index 0ac53285657..9a3d324b173 100644 --- a/Source/Dafny/Dafny.csproj +++ b/Source/Dafny/Dafny.csproj @@ -5,7 +5,7 @@ Dafny true TRACE - net6.0 + net8.0 ..\..\Binaries\ false diff --git a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj index d10cb4ca84e..8af0441bac0 100644 --- a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj +++ b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable enable ..\..\Binaries\ diff --git a/Source/DafnyCore.Test/DafnyCore.Test.csproj b/Source/DafnyCore.Test/DafnyCore.Test.csproj index 8e9d3e8aeba..635725c74cf 100644 --- a/Source/DafnyCore.Test/DafnyCore.Test.csproj +++ b/Source/DafnyCore.Test/DafnyCore.Test.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable enable diff --git a/Source/DafnyCore/AST/AstVisitor.cs b/Source/DafnyCore/AST/AstVisitor.cs index cf1388b50d9..95316147bd5 100644 --- a/Source/DafnyCore/AST/AstVisitor.cs +++ b/Source/DafnyCore/AST/AstVisitor.cs @@ -115,7 +115,7 @@ public void VisitMember(MemberDecl member) { } else { Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected member type + throw new Cce.UnreachableException(); // unexpected member type } } diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index e3f44389b65..9f161433b15 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -19,7 +19,7 @@ public class Attributes : TokenNode { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Name != null); - Contract.Invariant(cce.NonNullElements(Args)); + Contract.Invariant(Cce.NonNullElements(Args)); } public static string AxiomAttributeName = "axiom"; @@ -36,7 +36,7 @@ void ObjectInvariant() { public readonly Attributes Prev; public Attributes(string name, [Captured] List args, Attributes prev) { Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(args)); + Contract.Requires(Cce.NonNullElements(args)); Name = name; Args = args; Prev = prev; diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index 0726f4831a9..39e27441e41 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -98,7 +98,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne } else if (d is TupleTypeDecl) { // Tuple type declarations only exist in the system module. Therefore, they are never cloned. Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } else if (d is IndDatatypeDecl) { var dd = (IndDatatypeDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); @@ -441,7 +441,7 @@ public virtual Statement CloneStmt(Statement stmt, bool isReference) { } Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected statement TODO, make all statements inherit from ICloneable. + throw new Cce.UnreachableException(); // unexpected statement TODO, make all statements inherit from ICloneable. } public MatchCaseStmt CloneMatchCaseStmt(MatchCaseStmt c) { @@ -481,7 +481,7 @@ public CalcStmt.CalcOp CloneCalcOp(CalcStmt.CalcOp op) { return new CalcStmt.TernaryCalcOp(CloneExpr(((CalcStmt.TernaryCalcOp)op).Index)); } else { Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } diff --git a/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs b/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs index 15a703bec34..98dc8b5f96c 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs @@ -39,7 +39,7 @@ public ApplySuffix(IToken tok, IToken/*?*/ atLabel, Expression lhs, List { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Array != null); - Contract.Invariant(cce.NonNullElements(Indices)); + Contract.Invariant(Cce.NonNullElements(Indices)); Contract.Invariant(1 <= Indices.Count); } @@ -23,7 +23,7 @@ public MultiSelectExpr(IToken tok, Expression array, List indices) : base(tok) { Contract.Requires(tok != null); Contract.Requires(array != null); - Contract.Requires(cce.NonNullElements(indices) && 1 <= indices.Count); + Contract.Requires(Cce.NonNullElements(indices) && 1 <= indices.Count); Array = array; Indices = indices; diff --git a/Source/DafnyCore/AST/Expressions/Collections/DisplayExpression.cs b/Source/DafnyCore/AST/Expressions/Collections/DisplayExpression.cs index 677dfe896cf..d543cec8c30 100644 --- a/Source/DafnyCore/AST/Expressions/Collections/DisplayExpression.cs +++ b/Source/DafnyCore/AST/Expressions/Collections/DisplayExpression.cs @@ -7,7 +7,7 @@ public abstract class DisplayExpression : Expression { public readonly List Elements; [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(Elements)); + Contract.Invariant(Cce.NonNullElements(Elements)); } protected DisplayExpression(Cloner cloner, DisplayExpression original) : base(cloner, original) { @@ -16,7 +16,7 @@ protected DisplayExpression(Cloner cloner, DisplayExpression original) : base(cl public DisplayExpression(IToken tok, List elements) : base(tok) { - Contract.Requires(cce.NonNullElements(elements)); + Contract.Requires(Cce.NonNullElements(elements)); Elements = elements; } diff --git a/Source/DafnyCore/AST/Expressions/Collections/MapDisplayExpr.cs b/Source/DafnyCore/AST/Expressions/Collections/MapDisplayExpr.cs index b4994544422..f6792891c3b 100644 --- a/Source/DafnyCore/AST/Expressions/Collections/MapDisplayExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Collections/MapDisplayExpr.cs @@ -16,7 +16,7 @@ public MapDisplayExpr(Cloner cloner, MapDisplayExpr original) : base(cloner, ori public MapDisplayExpr(IToken tok, bool finite, List elements) : base(tok) { Contract.Requires(tok != null); - Contract.Requires(cce.NonNullElements(elements)); + Contract.Requires(Cce.NonNullElements(elements)); Finite = finite; Elements = elements; } diff --git a/Source/DafnyCore/AST/Expressions/Collections/MultiSetDisplayExpr.cs b/Source/DafnyCore/AST/Expressions/Collections/MultiSetDisplayExpr.cs index 1447da33c6c..e009a03716f 100644 --- a/Source/DafnyCore/AST/Expressions/Collections/MultiSetDisplayExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Collections/MultiSetDisplayExpr.cs @@ -9,7 +9,7 @@ public MultiSetDisplayExpr(Cloner cloner, MultiSetDisplayExpr original) : base(c public MultiSetDisplayExpr(IToken tok, List elements) : base(tok, elements) { Contract.Requires(tok != null); - Contract.Requires(cce.NonNullElements(elements)); + Contract.Requires(Cce.NonNullElements(elements)); } public MultiSetDisplayExpr Clone(Cloner cloner) { diff --git a/Source/DafnyCore/AST/Expressions/Collections/MultiSetFormingExpr.cs b/Source/DafnyCore/AST/Expressions/Collections/MultiSetFormingExpr.cs index f7fdab16273..955b68ab191 100644 --- a/Source/DafnyCore/AST/Expressions/Collections/MultiSetFormingExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Collections/MultiSetFormingExpr.cs @@ -20,7 +20,7 @@ public MultiSetFormingExpr(IToken tok, Expression expr) : base(tok) { Contract.Requires(tok != null); Contract.Requires(expr != null); - cce.Owner.AssignSame(this, expr); + Cce.Owner.AssignSame(this, expr); E = expr; } diff --git a/Source/DafnyCore/AST/Expressions/Collections/SeqDisplayExpr.cs b/Source/DafnyCore/AST/Expressions/Collections/SeqDisplayExpr.cs index f739f72f5e1..2c1488cb50e 100644 --- a/Source/DafnyCore/AST/Expressions/Collections/SeqDisplayExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Collections/SeqDisplayExpr.cs @@ -6,7 +6,7 @@ namespace Microsoft.Dafny; public class SeqDisplayExpr : DisplayExpression, ICanFormat, ICloneable { public SeqDisplayExpr(IToken tok, List elements) : base(tok, elements) { - Contract.Requires(cce.NonNullElements(elements)); + Contract.Requires(Cce.NonNullElements(elements)); Contract.Requires(tok != null); } diff --git a/Source/DafnyCore/AST/Expressions/Collections/SetDisplayExpr.cs b/Source/DafnyCore/AST/Expressions/Collections/SetDisplayExpr.cs index b413a85348f..6677dd16a50 100644 --- a/Source/DafnyCore/AST/Expressions/Collections/SetDisplayExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Collections/SetDisplayExpr.cs @@ -8,7 +8,7 @@ public class SetDisplayExpr : DisplayExpression, ICanFormat, ICloneable elements) : base(tok, elements) { Contract.Requires(tok != null); - Contract.Requires(cce.NonNullElements(elements)); + Contract.Requires(Cce.NonNullElements(elements)); Finite = finite; } diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs index 0abfc1614cd..ec96d0adaeb 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs @@ -54,7 +54,7 @@ public List UncompilableBoundVars() { public ComprehensionExpr(IToken tok, RangeToken rangeToken, List bvars, Expression range, Expression term, Attributes attrs) : base(tok) { Contract.Requires(tok != null); - Contract.Requires(cce.NonNullElements(bvars)); + Contract.Requires(Cce.NonNullElements(bvars)); Contract.Requires(term != null); BoundVars = bvars; diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ExistsExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ExistsExpr.cs index b16b10017b2..686482a6fd7 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/ExistsExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ExistsExpr.cs @@ -9,7 +9,7 @@ public class ExistsExpr : QuantifierExpr, ICloneable { public ExistsExpr(IToken tok, RangeToken rangeToken, List bvars, Expression range, Expression term, Attributes attrs) : base(tok, rangeToken, bvars, range, term, attrs) { - Contract.Requires(cce.NonNullElements(bvars)); + Contract.Requires(Cce.NonNullElements(bvars)); Contract.Requires(tok != null); Contract.Requires(term != null); } diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs index 64e3fd1e846..f7dec188ed2 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs @@ -9,7 +9,7 @@ public class ForallExpr : QuantifierExpr, ICloneable { public ForallExpr(IToken tok, RangeToken rangeToken, List bvars, Expression range, Expression term, Attributes attrs) : base(tok, rangeToken, bvars, range, term, attrs) { - Contract.Requires(cce.NonNullElements(bvars)); + Contract.Requires(Cce.NonNullElements(bvars)); Contract.Requires(tok != null); Contract.Requires(term != null); } diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/MapComprehension.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/MapComprehension.cs index 38022ff60fb..c4d9639976e 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/MapComprehension.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/MapComprehension.cs @@ -23,7 +23,7 @@ public MapComprehension(Cloner cloner, MapComprehension original) : base(cloner, public MapComprehension(IToken tok, RangeToken rangeToken, bool finite, List bvars, Expression range, Expression/*?*/ termLeft, Expression termRight, Attributes attrs) : base(tok, rangeToken, bvars, range, termRight, attrs) { Contract.Requires(tok != null); - Contract.Requires(cce.NonNullElements(bvars)); + Contract.Requires(Cce.NonNullElements(bvars)); Contract.Requires(1 <= bvars.Count); Contract.Requires(range != null); Contract.Requires(termRight != null); diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs index c829236b45b..89da49e4994 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs @@ -53,7 +53,7 @@ public String Refresh(string prefix, FreshIdGenerator idGen) { public QuantifierExpr(IToken tok, RangeToken rangeToken, List bvars, Expression range, Expression term, Attributes attrs) : base(tok, rangeToken, bvars, range, term, attrs) { Contract.Requires(tok != null); - Contract.Requires(cce.NonNullElements(bvars)); + Contract.Requires(Cce.NonNullElements(bvars)); Contract.Requires(term != null); this.UniqueId = FreshQuantId(); } @@ -70,7 +70,7 @@ protected QuantifierExpr(Cloner cloner, QuantifierExpr original) : base(cloner, public virtual Expression LogicalBody(bool bypassSplitQuantifier = false) { // Don't call this on a quantifier with a Split clause: it's not a real quantifier. The only exception is the Compiler. Contract.Requires(bypassSplitQuantifier || SplitQuantifier == null); - throw new cce.UnreachableException(); // This body is just here for the "Requires" clause + throw new Cce.UnreachableException(); // This body is just here for the "Requires" clause } public override IEnumerable PreResolveChildren => base.SubExpressions; diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/SetComprehension.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/SetComprehension.cs index 0dc1a998664..a2b53a44f1f 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/SetComprehension.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/SetComprehension.cs @@ -30,7 +30,7 @@ public SetComprehension(Cloner cloner, SetComprehension original) : base(cloner, public SetComprehension(IToken tok, RangeToken rangeToken, bool finite, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) : base(tok, rangeToken, bvars, range, term ?? new IdentifierExpr(tok, bvars[0].Name), attrs) { Contract.Requires(tok != null); - Contract.Requires(cce.NonNullElements(bvars)); + Contract.Requires(Cce.NonNullElements(bvars)); Contract.Requires(1 <= bvars.Count); Contract.Requires(range != null); Contract.Requires(term != null || bvars.Count == 1); diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs index d5e5e2e4c23..4778d540839 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs @@ -35,7 +35,7 @@ public NestedMatchExpr(Cloner cloner, NestedMatchExpr original) : base(cloner, o public NestedMatchExpr(IToken tok, Expression source, [Captured] List cases, bool usesOptionalBraces, Attributes attrs = null) : base(tok) { Contract.Requires(source != null); - Contract.Requires(cce.NonNullElements(cases)); + Contract.Requires(Cce.NonNullElements(cases)); this.Source = source; this.Cases = cases; this.UsesOptionalBraces = usesOptionalBraces; diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs index 68a6cf14c09..48944132602 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs @@ -68,7 +68,7 @@ public override IEnumerable NonSpecificationSubExpressions { public NestedMatchStmt(RangeToken rangeToken, Expression source, [Captured] List cases, bool usesOptionalBraces, Attributes attrs = null) : base(rangeToken, attrs) { Contract.Requires(source != null); - Contract.Requires(cce.NonNullElements(cases)); + Contract.Requires(Cce.NonNullElements(cases)); this.Source = source; this.Cases = cases; this.UsesOptionalBraces = usesOptionalBraces; diff --git a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs index 553d85e5100..590e381ad38 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/ExtendedPattern.cs @@ -77,7 +77,7 @@ public void CheckLinearExtendedPattern(Type type, ResolutionContext resolutionCo /* =[2]= */ return; } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } } else if (type.AsDatatype is TupleTypeDecl tupleTypeDecl) { var udt = type.NormalizeExpand() as UserDefinedType; @@ -125,7 +125,7 @@ public void CheckLinearExtendedPattern(Type type, ResolutionContext resolutionCo var dtd = type.AsDatatype; Dictionary ctors = dtd.ConstructorsByName; if (ctors == null) { - Contract.Assert(false); throw new cce.UnreachableException(); // Datatype not found + Contract.Assert(false); throw new Cce.UnreachableException(); // Datatype not found } DatatypeCtor ctor = null; // Check if the head of the pattern is a constructor or a variable diff --git a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs index ef817d6efc3..999565b4382 100644 --- a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs +++ b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs @@ -20,8 +20,8 @@ public class DatatypeValue : Expression, IHasReferences, ICloneable arguments) : base(tok) { - Contract.Requires(cce.NonNullElements(arguments)); + Contract.Requires(Cce.NonNullElements(arguments)); Contract.Requires(tok != null); Contract.Requires(datatypeName != null); Contract.Requires(memberName != null); diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs index ab1825a99db..3ec354a212a 100644 --- a/Source/DafnyCore/AST/Expressions/Expression.cs +++ b/Source/DafnyCore/AST/Expressions/Expression.cs @@ -142,7 +142,7 @@ public virtual bool IsImplicit { public static IEnumerable Conjuncts(Expression expr) { Contract.Requires(expr != null); Contract.Requires(expr.Type.IsBoolType); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Ensures(Cce.NonNullElements(Contract.Result>())); expr = StripParens(expr); if (expr is UnaryOpExpr unary && unary.Op == UnaryOpExpr.Opcode.Not) { @@ -169,7 +169,7 @@ public static IEnumerable Conjuncts(Expression expr) { public static IEnumerable Disjuncts(Expression expr) { Contract.Requires(expr != null); Contract.Requires(expr.Type.IsBoolType); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Ensures(Cce.NonNullElements(Contract.Result>())); expr = StripParens(expr); if (expr is UnaryOpExpr unary && unary.Op == UnaryOpExpr.Opcode.Not) { diff --git a/Source/DafnyCore/AST/Expressions/Heap/OldExpr.cs b/Source/DafnyCore/AST/Expressions/Heap/OldExpr.cs index 3c0c51c84e5..16204e88c2c 100644 --- a/Source/DafnyCore/AST/Expressions/Heap/OldExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Heap/OldExpr.cs @@ -32,7 +32,7 @@ public OldExpr(IToken tok, Expression expr, string at = null) : base(tok) { Contract.Requires(tok != null); Contract.Requires(expr != null); - cce.Owner.AssignSame(this, expr); + Cce.Owner.AssignSame(this, expr); E = expr; At = at; } diff --git a/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs b/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs index b81c90e4840..4cd12ec405d 100644 --- a/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs @@ -296,7 +296,7 @@ public static string OpcodeString(Opcode op) { return "^"; default: Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected operator + throw new Cce.UnreachableException(); // unexpected operator } } public Expression E0; diff --git a/Source/DafnyCore/AST/Expressions/Specification.cs b/Source/DafnyCore/AST/Expressions/Specification.cs index fc0a5ef3710..179bd0ca6c8 100644 --- a/Source/DafnyCore/AST/Expressions/Specification.cs +++ b/Source/DafnyCore/AST/Expressions/Specification.cs @@ -9,7 +9,7 @@ public class Specification : TokenNode, IAttributeBearingDeclaration [ContractInvariantMethod] private void ObjectInvariant() { - Contract.Invariant(Expressions == null || cce.NonNullElements(Expressions)); + Contract.Invariant(Expressions == null || Cce.NonNullElements(Expressions)); } public Specification() { @@ -18,7 +18,7 @@ public Specification() { } public Specification(List exprs, Attributes attrs) { - Contract.Requires(exprs == null || cce.NonNullElements(exprs)); + Contract.Requires(exprs == null || Cce.NonNullElements(exprs)); Expressions = exprs; Attributes = attrs; } diff --git a/Source/DafnyCore/AST/Expressions/StmtExpr.cs b/Source/DafnyCore/AST/Expressions/StmtExpr.cs index 8af66ea9d28..06432a3a8d8 100644 --- a/Source/DafnyCore/AST/Expressions/StmtExpr.cs +++ b/Source/DafnyCore/AST/Expressions/StmtExpr.cs @@ -66,7 +66,7 @@ public Expression GetSConclusion() { } else if (S is UpdateStmt) { return CreateBoolLiteral(tok, true); // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :) } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected statement } } diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs index a95048f8f31..cb57bd43b16 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Expression.cs @@ -781,7 +781,7 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, case UnaryOpExpr.Opcode.Not: op = "!"; opBindingStrength = 0x80; break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary opcode + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected unary opcode } bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext); @@ -857,7 +857,7 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, case BinaryExpr.Opcode.Iff: opBindingStrength = 0x08; break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected binary operator + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected binary operator } int opBS = opBindingStrength & 0xF8; int ctxtBS = contextBindingStrength & 0xF8; @@ -1220,7 +1220,7 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, comma = true; } } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected expression } } diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs index 7188e4da1f7..bcf9dd0b743 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs @@ -435,7 +435,7 @@ public void PrintStatement(Statement stmt, int indent) { PrintModifyStmt(indent, (ModifyStmt)s.S, true); } else { Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected skeleton statement + throw new Cce.UnreachableException(); // unexpected skeleton statement } } else if (stmt is TryRecoverStatement haltRecoveryStatement) { @@ -453,7 +453,7 @@ public void PrintStatement(Statement stmt, int indent) { PrintStatement(haltRecoveryStatement.RecoverBody, ind); wr.Write("[[ } ]]"); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected statement } } @@ -712,7 +712,7 @@ void PrintRhs(AssignmentRhs rhs) { wr.Write(")"); } } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected RHS + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected RHS } if (rhs.HasAttributes()) { diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs index 8ed0acedbe7..3f1ac595ba2 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs @@ -731,7 +731,7 @@ public void PrintMembers(List members, int indent, string fileBeingP } state = 2; } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected member } } } @@ -793,7 +793,7 @@ public string TypeParamString(TypeParameter tp) { break; default: Contract.Assert(false); // unexpected VarianceSyntax - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } return variance + tp.Name + TPCharacteristicsSuffix(tp.Characteristics); } diff --git a/Source/DafnyCore/AST/Grammar/ProgramParser.cs b/Source/DafnyCore/AST/Grammar/ProgramParser.cs index 8c6ea9f3a4e..3a183452bc0 100644 --- a/Source/DafnyCore/AST/Grammar/ProgramParser.cs +++ b/Source/DafnyCore/AST/Grammar/ProgramParser.cs @@ -295,7 +295,7 @@ private static Parser SetupParser(string s /*!*/, Uri uri /*!*/, Contract.Requires(uri != null); System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ParseErrors).TypeHandle); System.Runtime.CompilerServices.RuntimeHelpers.RunClassConstructor(typeof(ResolutionErrors).TypeHandle); - byte[] /*!*/ buffer = cce.NonNull(Encoding.Default.GetBytes(s)); + byte[] /*!*/ buffer = Cce.NonNull(Encoding.Default.GetBytes(s)); var ms = new MemoryStream(buffer, false); var firstToken = new Token { Uri = uri diff --git a/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs b/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs index 00c0eb8ee4d..167e5b3ce0d 100644 --- a/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs +++ b/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs @@ -46,7 +46,7 @@ public IfDirectiveState(bool hasSeenElse, bool mayStillIncludeAnotherAlternative // "arg" is assumed to be trimmed private static bool IfdefConditionSaysToInclude(string arg, List /*!*/ defines) { Contract.Requires(arg != null); - Contract.Requires(cce.NonNullElements(defines)); + Contract.Requires(Cce.NonNullElements(defines)); bool sense = true; while (arg.StartsWith("!")) { sense = !sense; @@ -58,7 +58,7 @@ private static bool IfdefConditionSaysToInclude(string arg, List /*!*/ d public static string ProcessDirectives(TextReader reader, List /*!*/ defines) { Contract.Requires(reader != null); - Contract.Requires(cce.NonNullElements(defines)); + Contract.Requires(Cce.NonNullElements(defines)); Contract.Ensures(Contract.Result() != null); string newline = null; StringBuilder sb = new StringBuilder(); diff --git a/Source/DafnyCore/AST/Members/ConstantField.cs b/Source/DafnyCore/AST/Members/ConstantField.cs index 490443f42f2..446c34bc99d 100644 --- a/Source/DafnyCore/AST/Members/ConstantField.cs +++ b/Source/DafnyCore/AST/Members/ConstantField.cs @@ -29,7 +29,7 @@ public override bool CanBeRevealed() { public List Ins { get { return new List(); } } public ModuleDefinition EnclosingModule { get { return this.EnclosingClass.EnclosingModuleDefinition; } } public bool MustReverify { get { return false; } } - public bool AllowsNontermination { get { throw new cce.UnreachableException(); } } + public bool AllowsNontermination { get { throw new Cce.UnreachableException(); } } public string NameRelativeToModule { get { if (EnclosingClass is DefaultClassDecl) { @@ -39,10 +39,10 @@ public string NameRelativeToModule { } } } - public Specification Decreases { get { throw new cce.UnreachableException(); } } + public Specification Decreases { get { throw new Cce.UnreachableException(); } } public bool InferredDecreases { - get { throw new cce.UnreachableException(); } - set { throw new cce.UnreachableException(); } + get { throw new Cce.UnreachableException(); } + set { throw new Cce.UnreachableException(); } } public bool AllowsAllocation => true; diff --git a/Source/DafnyCore/AST/Members/Constructor.cs b/Source/DafnyCore/AST/Members/Constructor.cs index b40feeaf963..2cd2dbbbed3 100644 --- a/Source/DafnyCore/AST/Members/Constructor.cs +++ b/Source/DafnyCore/AST/Members/Constructor.cs @@ -48,11 +48,11 @@ public Constructor(RangeToken rangeToken, Name name, : base(rangeToken, name, false, isGhost, typeArgs, ins, new List(), req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(ins)); - Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(Cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(ins)); + Contract.Requires(Cce.NonNullElements(req)); Contract.Requires(mod != null); - Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(Cce.NonNullElements(ens)); Contract.Requires(decreases != null); } diff --git a/Source/DafnyCore/AST/Members/ExtremeLemma.cs b/Source/DafnyCore/AST/Members/ExtremeLemma.cs index fab1ff5cb71..4a61bc3707b 100644 --- a/Source/DafnyCore/AST/Members/ExtremeLemma.cs +++ b/Source/DafnyCore/AST/Members/ExtremeLemma.cs @@ -32,12 +32,12 @@ public ExtremeLemma(RangeToken rangeToken, Name name, : base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(ins)); - Contract.Requires(cce.NonNullElements(outs)); - Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(Cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(ins)); + Contract.Requires(Cce.NonNullElements(outs)); + Contract.Requires(Cce.NonNullElements(req)); Contract.Requires(mod != null); - Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(Cce.NonNullElements(ens)); Contract.Requires(decreases != null); TypeOfK = typeOfK; } @@ -62,12 +62,12 @@ public LeastLemma(RangeToken rangeToken, Name name, : base(rangeToken, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(ins)); - Contract.Requires(cce.NonNullElements(outs)); - Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(Cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(ins)); + Contract.Requires(Cce.NonNullElements(outs)); + Contract.Requires(Cce.NonNullElements(req)); Contract.Requires(mod != null); - Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(Cce.NonNullElements(ens)); Contract.Requires(decreases != null); } @@ -92,12 +92,12 @@ public GreatestLemma(RangeToken rangeToken, Name name, : base(rangeToken, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(ins)); - Contract.Requires(cce.NonNullElements(outs)); - Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(Cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(ins)); + Contract.Requires(Cce.NonNullElements(outs)); + Contract.Requires(Cce.NonNullElements(req)); Contract.Requires(mod != null); - Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(Cce.NonNullElements(ens)); Contract.Requires(decreases != null); } diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs index 7a901fe1917..4029582dad0 100644 --- a/Source/DafnyCore/AST/Members/Function.cs +++ b/Source/DafnyCore/AST/Members/Function.cs @@ -203,12 +203,12 @@ public enum CoCallClusterInvolvement { [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(TypeArgs)); - Contract.Invariant(cce.NonNullElements(Ins)); + Contract.Invariant(Cce.NonNullElements(TypeArgs)); + Contract.Invariant(Cce.NonNullElements(Ins)); Contract.Invariant(ResultType != null); - Contract.Invariant(cce.NonNullElements(Req)); + Contract.Invariant(Cce.NonNullElements(Req)); Contract.Invariant(Reads != null); - Contract.Invariant(cce.NonNullElements(Ens)); + Contract.Invariant(Cce.NonNullElements(Ens)); Contract.Invariant(Decreases != null); } @@ -221,12 +221,12 @@ public Function(RangeToken range, Name name, bool hasStaticKeyword, bool isGhost Contract.Requires(tok != null); Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(ins)); + Contract.Requires(Cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(ins)); Contract.Requires(resultType != null); - Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(Cce.NonNullElements(req)); Contract.Requires(reads != null); - Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(Cce.NonNullElements(ens)); Contract.Requires(decreases != null); Contract.Requires(byMethodBody == null || (!isGhost && body != null)); // function-by-method has a ghost expr and non-ghost stmt, but to callers appears like a functiion-method this.IsFueled = false; // Defaults to false. Only set to true if someone mentions this function in a fuel annotation diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs index bcf14888f6c..363ba42692b 100644 --- a/Source/DafnyCore/AST/Members/ICodeContext.cs +++ b/Source/DafnyCore/AST/Members/ICodeContext.cs @@ -104,35 +104,35 @@ public string GetDescription(DafnyOptions options) { public class DontUseICallable : ICallable { - public string WhatKind { get { throw new cce.UnreachableException(); } } - public bool IsGhost { get { throw new cce.UnreachableException(); } } - public List TypeArgs { get { throw new cce.UnreachableException(); } } - public List Ins { get { throw new cce.UnreachableException(); } } - public ModuleDefinition EnclosingModule { get { throw new cce.UnreachableException(); } } - public bool MustReverify { get { throw new cce.UnreachableException(); } } - public string FullSanitizedName { get { throw new cce.UnreachableException(); } } - public bool AllowsNontermination { get { throw new cce.UnreachableException(); } } - public IToken Tok { get { throw new cce.UnreachableException(); } } - public IEnumerable Children => throw new cce.UnreachableException(); - public IEnumerable PreResolveChildren => throw new cce.UnreachableException(); - - public string NameRelativeToModule { get { throw new cce.UnreachableException(); } } - public Specification Decreases { get { throw new cce.UnreachableException(); } } + public string WhatKind { get { throw new Cce.UnreachableException(); } } + public bool IsGhost { get { throw new Cce.UnreachableException(); } } + public List TypeArgs { get { throw new Cce.UnreachableException(); } } + public List Ins { get { throw new Cce.UnreachableException(); } } + public ModuleDefinition EnclosingModule { get { throw new Cce.UnreachableException(); } } + public bool MustReverify { get { throw new Cce.UnreachableException(); } } + public string FullSanitizedName { get { throw new Cce.UnreachableException(); } } + public bool AllowsNontermination { get { throw new Cce.UnreachableException(); } } + public IToken Tok { get { throw new Cce.UnreachableException(); } } + public IEnumerable Children => throw new Cce.UnreachableException(); + public IEnumerable PreResolveChildren => throw new Cce.UnreachableException(); + + public string NameRelativeToModule { get { throw new Cce.UnreachableException(); } } + public Specification Decreases { get { throw new Cce.UnreachableException(); } } public bool InferredDecreases { - get { throw new cce.UnreachableException(); } - set { throw new cce.UnreachableException(); } + get { throw new Cce.UnreachableException(); } + set { throw new Cce.UnreachableException(); } } - public bool AllowsAllocation => throw new cce.UnreachableException(); + public bool AllowsAllocation => throw new Cce.UnreachableException(); public IEnumerable GetConcreteChildren() { - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } - public IEnumerable OwnedTokens => throw new cce.UnreachableException(); - public RangeToken RangeToken => throw new cce.UnreachableException(); - public IToken NavigationToken => throw new cce.UnreachableException(); - public SymbolKind? Kind => throw new cce.UnreachableException(); + public IEnumerable OwnedTokens => throw new Cce.UnreachableException(); + public RangeToken RangeToken => throw new Cce.UnreachableException(); + public IToken NavigationToken => throw new Cce.UnreachableException(); + public SymbolKind? Kind => throw new Cce.UnreachableException(); public string GetDescription(DafnyOptions options) { - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } public string Designator => WhatKind; } @@ -157,9 +157,9 @@ public NoContext(ModuleDefinition module) { List ICodeContext.TypeArgs { get { return new List(); } } List ICodeContext.Ins { get { return new List(); } } ModuleDefinition IASTVisitorContext.EnclosingModule { get { return Module; } } - bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } - public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } - public bool AllowsNontermination { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } + bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new Cce.UnreachableException(); } } + public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new Cce.UnreachableException(); } } + public bool AllowsNontermination { get { Contract.Assume(false, "should not be called on NoContext"); throw new Cce.UnreachableException(); } } public bool AllowsAllocation => true; } diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs index ff275773731..0452b2ad0e7 100644 --- a/Source/DafnyCore/AST/Members/Method.cs +++ b/Source/DafnyCore/AST/Members/Method.cs @@ -110,13 +110,13 @@ public override IEnumerable SubExpressions { [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(TypeArgs)); - Contract.Invariant(cce.NonNullElements(Ins)); - Contract.Invariant(cce.NonNullElements(Outs)); - Contract.Invariant(cce.NonNullElements(Req)); + Contract.Invariant(Cce.NonNullElements(TypeArgs)); + Contract.Invariant(Cce.NonNullElements(Ins)); + Contract.Invariant(Cce.NonNullElements(Outs)); + Contract.Invariant(Cce.NonNullElements(Req)); Contract.Invariant(Reads != null); Contract.Invariant(Mod != null); - Contract.Invariant(cce.NonNullElements(Ens)); + Contract.Invariant(Cce.NonNullElements(Ens)); Contract.Invariant(Decreases != null); } @@ -147,13 +147,13 @@ public Method(RangeToken rangeToken, Name name, typeArgs, ins, req, ens, decreases) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(ins)); - Contract.Requires(cce.NonNullElements(outs)); - Contract.Requires(cce.NonNullElements(req)); + Contract.Requires(Cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(ins)); + Contract.Requires(Cce.NonNullElements(outs)); + Contract.Requires(Cce.NonNullElements(req)); Contract.Requires(reads != null); Contract.Requires(mod != null); - Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(Cce.NonNullElements(ens)); Contract.Requires(decreases != null); this.Outs = outs; this.Reads = reads; diff --git a/Source/DafnyCore/AST/Modules/DefaultClassDecl.cs b/Source/DafnyCore/AST/Modules/DefaultClassDecl.cs index 1ba074ffe70..cc86eb382d4 100644 --- a/Source/DafnyCore/AST/Modules/DefaultClassDecl.cs +++ b/Source/DafnyCore/AST/Modules/DefaultClassDecl.cs @@ -14,7 +14,7 @@ public class DefaultClassDecl : TopLevelDeclWithMembers, RevealableTypeDecl { public DefaultClassDecl(ModuleDefinition module, [Captured] List members) : base(RangeToken.NoToken, new Name("_default"), module, new List(), members, null, false, null) { Contract.Requires(module != null); - Contract.Requires(cce.NonNullElements(members)); + Contract.Requires(Cce.NonNullElements(members)); this.NewSelfSynonym(); } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index 1e251e7744b..742ad5e2048 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -100,7 +100,7 @@ public IEnumerable DefaultClasses { [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(TopLevelDecls)); + Contract.Invariant(Cce.NonNullElements(TopLevelDecls)); Contract.Invariant(CallGraph != null); } diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs index 09f93ed194a..28eaf039b5d 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignStmt.cs @@ -102,7 +102,7 @@ public static string NonGhostKind_To_String(NonGhostKind gk) { case NonGhostKind.ArrayElement: return "array element"; default: Contract.Assume(false); // unexpected NonGhostKind - throw new cce.UnreachableException(); // please compiler + throw new Cce.UnreachableException(); // please compiler } } /// diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs index 1d1db731578..adec2340d17 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs @@ -58,7 +58,7 @@ public AssignSuchThatStmt(Cloner cloner, AssignSuchThatStmt original) : base(clo public AssignSuchThatStmt(RangeToken rangeToken, List lhss, Expression expr, AttributedToken assumeToken, Attributes attrs) : base(rangeToken, lhss, attrs) { Contract.Requires(rangeToken != null); - Contract.Requires(cce.NonNullElements(lhss)); + Contract.Requires(Cce.NonNullElements(lhss)); Contract.Requires(lhss.Count != 0); Contract.Requires(expr != null); Expr = expr; diff --git a/Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs b/Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs index 159ddb223fa..51bdcf54f0d 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/ConcreteUpdateStatement.cs @@ -16,7 +16,7 @@ protected ConcreteUpdateStatement(Cloner cloner, ConcreteUpdateStatement origina public ConcreteUpdateStatement(RangeToken rangeToken, List lhss, Attributes attrs = null) : base(rangeToken, attrs) { - Contract.Requires(cce.NonNullElements(lhss)); + Contract.Requires(Cce.NonNullElements(lhss)); Lhss = lhss; } diff --git a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs index cc3fe0507f1..f611205309c 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/UpdateStmt.cs @@ -34,8 +34,8 @@ public override IToken Tok { [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(Lhss)); - Contract.Invariant(cce.NonNullElements(Rhss)); + Contract.Invariant(Cce.NonNullElements(Lhss)); + Contract.Invariant(Cce.NonNullElements(Rhss)); } public UpdateStmt Clone(Cloner cloner) { @@ -52,16 +52,16 @@ public UpdateStmt(Cloner cloner, UpdateStmt original) : base(cloner, original) { public UpdateStmt(RangeToken rangeToken, List lhss, List rhss) : base(rangeToken, lhss) { - Contract.Requires(cce.NonNullElements(lhss)); - Contract.Requires(cce.NonNullElements(rhss)); + Contract.Requires(Cce.NonNullElements(lhss)); + Contract.Requires(Cce.NonNullElements(rhss)); Contract.Requires(lhss.Count != 0 || rhss.Count == 1); Rhss = rhss; CanMutateKnownState = false; } public UpdateStmt(RangeToken rangeToken, List lhss, List rhss, bool mutate) : base(rangeToken, lhss) { - Contract.Requires(cce.NonNullElements(lhss)); - Contract.Requires(cce.NonNullElements(rhss)); + Contract.Requires(Cce.NonNullElements(lhss)); + Contract.Requires(Cce.NonNullElements(rhss)); Contract.Requires(lhss.Count != 0 || rhss.Count == 1); Rhss = rhss; CanMutateKnownState = mutate; diff --git a/Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs index 72bbed6ffc0..b5075cecff9 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs @@ -9,7 +9,7 @@ public class VarDeclStmt : Statement, ICloneable, ICanFormat { public readonly ConcreteUpdateStatement Update; [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(Locals)); + Contract.Invariant(Cce.NonNullElements(Locals)); Contract.Invariant(Locals.Count != 0); } diff --git a/Source/DafnyCore/AST/Statements/BlockStmt.cs b/Source/DafnyCore/AST/Statements/BlockStmt.cs index 7cac730b458..dc2a5e12bba 100644 --- a/Source/DafnyCore/AST/Statements/BlockStmt.cs +++ b/Source/DafnyCore/AST/Statements/BlockStmt.cs @@ -18,7 +18,7 @@ protected BlockStmt(Cloner cloner, BlockStmt original) : base(cloner, original) public BlockStmt(RangeToken rangeToken, [Captured] List body) : base(rangeToken) { Contract.Requires(rangeToken != null); - Contract.Requires(cce.NonNullElements(body)); + Contract.Requires(Cce.NonNullElements(body)); this.Body = body; } diff --git a/Source/DafnyCore/AST/Statements/CalcStmt.cs b/Source/DafnyCore/AST/Statements/CalcStmt.cs index a4d5d14af45..bb23b5f1036 100644 --- a/Source/DafnyCore/AST/Statements/CalcStmt.cs +++ b/Source/DafnyCore/AST/Statements/CalcStmt.cs @@ -95,7 +95,7 @@ public override CalcOp ResultOp(CalcOp other) { return other.ResultOp(this); } else { Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } @@ -140,7 +140,7 @@ public override CalcOp ResultOp(CalcOp other) { return new TernaryCalcOp(minIndex); // ToDo: if we could compare expressions for syntactic equality, we could use this here to optimize } else { Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } @@ -213,12 +213,12 @@ public CalcOp GetInferredDefaultOp() { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Lines != null); - Contract.Invariant(cce.NonNullElements(Lines)); + Contract.Invariant(Cce.NonNullElements(Lines)); Contract.Invariant(Hints != null); - Contract.Invariant(cce.NonNullElements(Hints)); + Contract.Invariant(Cce.NonNullElements(Hints)); Contract.Invariant(StepOps != null); Contract.Invariant(Steps != null); - Contract.Invariant(cce.NonNullElements(Steps)); + Contract.Invariant(Cce.NonNullElements(Steps)); Contract.Invariant(Hints.Count == Math.Max(Lines.Count - 1, 0)); Contract.Invariant(StepOps.Count == Hints.Count); } @@ -229,8 +229,8 @@ public CalcStmt(RangeToken rangeToken, CalcOp userSuppliedOp, List l Contract.Requires(lines != null); Contract.Requires(hints != null); Contract.Requires(stepOps != null); - Contract.Requires(cce.NonNullElements(lines)); - Contract.Requires(cce.NonNullElements(hints)); + Contract.Requires(Cce.NonNullElements(lines)); + Contract.Requires(Cce.NonNullElements(hints)); Contract.Requires(hints.Count == Math.Max(lines.Count - 1, 0)); Contract.Requires(stepOps.Count == hints.Count); UserSuppliedOp = userSuppliedOp; diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/ForallStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/ForallStmt.cs index 6a71378ac49..51f87b136a5 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/ForallStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/ForallStmt.cs @@ -66,10 +66,10 @@ public ForallStmt(Cloner cloner, ForallStmt original) : base(cloner, original) { public ForallStmt(RangeToken rangeToken, List boundVars, Attributes attrs, Expression range, List ens, Statement body) : base(rangeToken, attrs) { Contract.Requires(rangeToken != null); - Contract.Requires(cce.NonNullElements(boundVars)); + Contract.Requires(Cce.NonNullElements(boundVars)); Contract.Requires(range != null); Contract.Requires(boundVars.Count != 0 || LiteralExpr.IsTrue(range)); - Contract.Requires(cce.NonNullElements(ens)); + Contract.Requires(Cce.NonNullElements(ens)); this.BoundVars = boundVars; this.Range = range; this.Ens = ens; diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs index d28972d3a6b..18c24ee8e4b 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs @@ -10,7 +10,7 @@ public abstract class LoopStmt : Statement, IHasNavigationToken { public readonly Specification Mod; [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(Invariants)); + Contract.Invariant(Cce.NonNullElements(Invariants)); Contract.Invariant(Decreases != null); Contract.Invariant(Mod != null); } @@ -28,7 +28,7 @@ protected LoopStmt(Cloner cloner, LoopStmt original) : base(cloner, original) { public LoopStmt(RangeToken rangeToken, List invariants, Specification decreases, Specification mod) : base(rangeToken) { Contract.Requires(rangeToken != null); - Contract.Requires(cce.NonNullElements(invariants)); + Contract.Requires(Cce.NonNullElements(invariants)); Contract.Requires(decreases != null); Contract.Requires(mod != null); @@ -39,7 +39,7 @@ public LoopStmt(RangeToken rangeToken, List invariants, Sp public LoopStmt(RangeToken rangeToken, List invariants, Specification decreases, Specification mod, Attributes attrs) : base(rangeToken, attrs) { Contract.Requires(rangeToken != null); - Contract.Requires(cce.NonNullElements(invariants)); + Contract.Requires(Cce.NonNullElements(invariants)); Contract.Requires(decreases != null); Contract.Requires(mod != null); diff --git a/Source/DafnyCore/AST/Statements/DividedBlockStmt.cs b/Source/DafnyCore/AST/Statements/DividedBlockStmt.cs index 076fbae4025..ff39a268311 100644 --- a/Source/DafnyCore/AST/Statements/DividedBlockStmt.cs +++ b/Source/DafnyCore/AST/Statements/DividedBlockStmt.cs @@ -25,8 +25,8 @@ public DividedBlockStmt(Cloner cloner, DividedBlockStmt original) : base(cloner, public DividedBlockStmt(RangeToken rangeToken, List bodyInit, IToken/*?*/ separatorTok, List bodyProper) : base(rangeToken, Util.Concat(bodyInit, bodyProper)) { Contract.Requires(rangeToken != null); - Contract.Requires(cce.NonNullElements(bodyInit)); - Contract.Requires(cce.NonNullElements(bodyProper)); + Contract.Requires(Cce.NonNullElements(bodyInit)); + Contract.Requires(Cce.NonNullElements(bodyProper)); this.BodyInit = bodyInit; this.SeparatorTok = separatorTok; this.BodyProper = bodyProper; diff --git a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs index fc52debc2a6..6107a1dc7ed 100644 --- a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs +++ b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs @@ -14,8 +14,8 @@ public class CallStmt : Statement, ICloneable { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(MethodSelect.Member is Method); - Contract.Invariant(cce.NonNullElements(Lhs)); - Contract.Invariant(cce.NonNullElements(Args)); + Contract.Invariant(Cce.NonNullElements(Lhs)); + Contract.Invariant(Cce.NonNullElements(Args)); } public override IEnumerable Children => Lhs.Concat(new Node[] { MethodSelect, Bindings }); @@ -32,10 +32,10 @@ void ObjectInvariant() { public CallStmt(RangeToken rangeToken, List lhs, MemberSelectExpr memSel, List args, IToken overrideToken = null) : base(rangeToken) { Contract.Requires(rangeToken != null); - Contract.Requires(cce.NonNullElements(lhs)); + Contract.Requires(Cce.NonNullElements(lhs)); Contract.Requires(memSel != null); Contract.Requires(memSel.Member is Method); - Contract.Requires(cce.NonNullElements(args)); + Contract.Requires(Cce.NonNullElements(args)); this.Lhs = lhs; this.MethodSelect = memSel; diff --git a/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs b/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs index cf08c54bfa6..12e64a4b7f5 100644 --- a/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs +++ b/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs @@ -25,7 +25,7 @@ static PrintStmt() { [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(Args)); + Contract.Invariant(Cce.NonNullElements(Args)); } public PrintStmt Clone(Cloner cloner) { @@ -39,7 +39,7 @@ public PrintStmt(Cloner cloner, PrintStmt original) : base(cloner, original) { public PrintStmt(RangeToken rangeToken, List args) : base(rangeToken) { Contract.Requires(rangeToken != null); - Contract.Requires(cce.NonNullElements(args)); + Contract.Requires(Cce.NonNullElements(args)); Args = args; } diff --git a/Source/DafnyCore/AST/Substituter.cs b/Source/DafnyCore/AST/Substituter.cs index 1ce3fb1f55a..3f508306c92 100644 --- a/Source/DafnyCore/AST/Substituter.cs +++ b/Source/DafnyCore/AST/Substituter.cs @@ -85,7 +85,7 @@ public virtual Expression Substitute(Expression expr) { } } - return cce.NonNull(substExprFinal); + return Cce.NonNull(substExprFinal); } } else if (expr is DisplayExpression) { DisplayExpression e = (DisplayExpression)expr; @@ -565,7 +565,7 @@ public BoundedPool SubstituteBoundedPool(BoundedPool bound) { return bound; // nothing to substitute } else { Contract.Assume(false); // unexpected BoundedPool - throw new cce.UnreachableException(); // to please compiler + throw new Cce.UnreachableException(); // to please compiler } } @@ -676,12 +676,12 @@ Func, Type, VT, VT> cloneVt } protected List/*!*/ SubstituteExprList(List/*!*/ elist) { - Contract.Requires(cce.NonNullElements(elist)); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Requires(Cce.NonNullElements(elist)); + Contract.Ensures(Cce.NonNullElements(Contract.Result>())); List newElist = null; // initialized lazily for (int i = 0; i < elist.Count; i++) { - cce.LoopInvariant(newElist == null || newElist.Count == i); + Cce.LoopInvariant(newElist == null || newElist.Count == i); Expression substE = Substitute(elist[i]); if (substE != elist[i] && newElist == null) { @@ -880,7 +880,7 @@ protected virtual Statement SubstStmt(Statement stmt) { rr.ResolvedStatements.AddRange(s.ResolvedStatements.ConvertAll(SubstStmt)); r = rr; } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected statement } // add labels to the cloned statement @@ -967,7 +967,7 @@ protected AssignmentRhs SubstRHS(AssignmentRhs rhs) { c = new HavocRhs(rhs.Tok); } else { // since the Substituter is assumed to operate on statements only if they are part of a StatementExpression, then the TypeRhs case cannot occur - Contract.Assume(false); throw new cce.UnreachableException(); + Contract.Assume(false); throw new Cce.UnreachableException(); } c.Attributes = SubstAttributes(rhs.Attributes); return c; @@ -994,12 +994,12 @@ protected CalcStmt.CalcOp SubstCalcOp(CalcStmt.CalcOp op) { return new CalcStmt.TernaryCalcOp(Substitute(((CalcStmt.TernaryCalcOp)op).Index)); } else { Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } public Attributes SubstAttributes(Attributes attrs) { - Contract.Requires(cce.NonNullDictionaryAndValues(substMap)); + Contract.Requires(Cce.NonNullDictionaryAndValues(substMap)); if (attrs != null) { var newArgs = new List(); // allocate it eagerly, what the heck, it doesn't seem worth the extra complexity in the code to do it lazily for the infrequently occurring attributes bool anyArgSubst = false; diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs index d7d946b7b2d..45d5d89f0f9 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/AST/TypeDeclarations/ClassDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs index e4d9677aa12..16bbd1f6617 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs @@ -11,7 +11,7 @@ public class ClassDecl : ClassLikeDecl { [FilledInDuringResolution] public bool HasConstructor; // filled in (early) during resolution; true iff there exists a member that is a Constructor [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(Members)); + Contract.Invariant(Cce.NonNullElements(Members)); Contract.Invariant(ParentTraits != null); } @@ -21,8 +21,8 @@ public ClassDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Contract.Requires(rangeToken != null); Contract.Requires(name != null); Contract.Requires(module != null); - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(members)); + Contract.Requires(Cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(members)); NonNullTypeDecl = new NonNullTypeDecl(this); this.NewSelfSynonym(); } diff --git a/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs index eca519a627e..bc32940779c 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs @@ -30,8 +30,8 @@ public ClassLikeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Contract.Requires(rangeToken != null); Contract.Requires(name != null); Contract.Requires(module != null); - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(members)); + Contract.Requires(Cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(members)); } public virtual bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { diff --git a/Source/DafnyCore/AST/TypeDeclarations/CoDatatypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/CoDatatypeDecl.cs index 319e2520fa7..3f5d055f0c9 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/CoDatatypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/CoDatatypeDecl.cs @@ -14,9 +14,9 @@ public CoDatatypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Contract.Requires(rangeToken != null); Contract.Requires(name != null); Contract.Requires(module != null); - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(ctors)); - Contract.Requires(cce.NonNullElements(members)); + Contract.Requires(Cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(ctors)); + Contract.Requires(Cce.NonNullElements(members)); Contract.Requires((isRefining && ctors.Count == 0) || (!isRefining && 1 <= ctors.Count)); } diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs index 854e6dc79f3..6caf88d6869 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs @@ -10,7 +10,7 @@ public class DatatypeCtor : Declaration, TypeParameter.ParentType, IHasDocstring public readonly List Formals; [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(Formals)); + Contract.Invariant(Cce.NonNullElements(Formals)); Contract.Invariant(Destructors != null); Contract.Invariant( Destructors.Count == 0 || // this is until resolution @@ -28,7 +28,7 @@ public DatatypeCtor(RangeToken rangeToken, Name name, bool isGhost, [Captured] L : base(rangeToken, name, attributes, false) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(formals)); + Contract.Requires(Cce.NonNullElements(formals)); this.Formals = formals; this.IsGhost = isGhost; } diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs index a8b82c29e9a..f7f8ae7165f 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs @@ -12,7 +12,7 @@ public abstract class DatatypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl [FilledInDuringResolution] public Dictionary ConstructorsByName { get; set; } [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(Ctors)); + Contract.Invariant(Cce.NonNullElements(Ctors)); Contract.Invariant(1 <= Ctors.Count); } @@ -26,9 +26,9 @@ public DatatypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, L Contract.Requires(rangeToken != null); Contract.Requires(name != null); Contract.Requires(module != null); - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(ctors)); - Contract.Requires(cce.NonNullElements(members)); + Contract.Requires(Cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(ctors)); + Contract.Requires(Cce.NonNullElements(members)); Contract.Requires((isRefining && ctors.Count == 0) || (!isRefining && 1 <= ctors.Count)); Ctors = ctors; this.NewSelfSynonym(); @@ -60,12 +60,12 @@ Specification ICallable.Decreases { get { // The resolver checks that a NewtypeDecl sits in its own SSC in the call graph. Therefore, // the question of what its Decreases clause is should never arise. - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } bool ICallable.InferredDecreases { - get { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases - set { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases + get { throw new Cce.UnreachableException(); } // see comment above about ICallable.Decreases + set { throw new Cce.UnreachableException(); } // see comment above about ICallable.Decreases } /// diff --git a/Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs index 6af1191fe99..72319bf83c1 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs @@ -38,9 +38,9 @@ public IndDatatypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module Contract.Requires(rangeToken != null); Contract.Requires(name != null); Contract.Requires(module != null); - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(ctors)); - Contract.Requires(cce.NonNullElements(members)); + Contract.Requires(Cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(ctors)); + Contract.Requires(Cce.NonNullElements(members)); Contract.Requires((isRefining && ctors.Count == 0) || (!isRefining && 1 <= ctors.Count)); } diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs index efd594d52f4..841ca74d93e 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs @@ -131,12 +131,12 @@ Specification ICallable.Decreases { get { // The resolver checks that a NewtypeDecl sits in its own SSC in the call graph. Therefore, // the question of what its Decreases clause is should never arise. - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } bool ICallable.InferredDecreases { - get { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases - set { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases + get { throw new Cce.UnreachableException(); } // see comment above about ICallable.Decreases + set { throw new Cce.UnreachableException(); } // see comment above about ICallable.Decreases } public override bool AcceptThis => true; diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs index 79b485c04eb..660b0690677 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs @@ -12,7 +12,7 @@ public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType, ISym public readonly List TypeArgs; [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(TypeArgs)); + Contract.Invariant(Cce.NonNullElements(TypeArgs)); } protected TopLevelDecl(Cloner cloner, TopLevelDecl original, ModuleDefinition parent) : base(cloner, original) { @@ -24,7 +24,7 @@ protected TopLevelDecl(RangeToken rangeToken, Name name, ModuleDefinition enclos : base(rangeToken, name, attributes, isRefining) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(typeArgs)); EnclosingModuleDefinition = enclosingModule; TypeArgs = typeArgs; } diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs index e83436c2dbe..3717c9db667 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs @@ -93,8 +93,8 @@ protected TopLevelDeclWithMembers(RangeToken rangeToken, Name name, ModuleDefini : base(rangeToken, name, module, typeArgs, attributes, isRefining) { Contract.Requires(rangeToken != null); Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(members)); + Contract.Requires(Cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(members)); Members = members; ParentTraits = traits ?? new List(); SetMembersBeforeResolution(); diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs index a6daacab0d6..199a5851858 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs @@ -88,12 +88,12 @@ Specification ICallable.Decreases { get { // The resolver checks that a NewtypeDecl sits in its own SSC in the call graph. Therefore, // the question of what its Decreases clause is should never arise. - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } bool ICallable.InferredDecreases { - get { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases - set { throw new cce.UnreachableException(); } // see comment above about ICallable.Decreases + get { throw new Cce.UnreachableException(); } // see comment above about ICallable.Decreases + set { throw new Cce.UnreachableException(); } // see comment above about ICallable.Decreases } public override bool CanBeRevealed() { return true; diff --git a/Source/DafnyCore/AST/Types/TypeParameter.cs b/Source/DafnyCore/AST/Types/TypeParameter.cs index 1e5548ffc2e..e67c437584a 100644 --- a/Source/DafnyCore/AST/Types/TypeParameter.cs +++ b/Source/DafnyCore/AST/Types/TypeParameter.cs @@ -92,7 +92,7 @@ public TPVariance Variance { return TPVariance.Contra; default: Contract.Assert(false); // unexpected VarianceSyntax - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } } @@ -108,7 +108,7 @@ public bool StrictVariance { return false; default: Contract.Assert(false); // unexpected VarianceSyntax - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } } diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index 22317360fdd..3776ac904c2 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -431,7 +431,7 @@ AutoInitInfo CharacteristicToAutoInitInfo(TypeParameter.TypeParameterCharacteris case SubsetTypeDecl.WKind.Special: default: Contract.Assert(false); // unexpected case - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } else if (cl is SubsetTypeDecl) { var td = (SubsetTypeDecl)cl; @@ -461,7 +461,7 @@ AutoInitInfo CharacteristicToAutoInitInfo(TypeParameter.TypeParameterCharacteris } default: Contract.Assert(false); // unexpected case - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } else if (cl is TraitDecl traitDecl) { return traitDecl.IsReferenceTypeDecl ? AutoInitInfo.CompilableValue : AutoInitInfo.MaybeEmpty; @@ -503,7 +503,7 @@ AutoInitInfo CharacteristicToAutoInitInfo(TypeParameter.TypeParameterCharacteris return r; } else { Contract.Assert(false); // unexpected type - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } @@ -1906,7 +1906,7 @@ public override Type Subst(IDictionary subst) { // SelfType's are used only in certain restricted situations. In those situations, we need to be able // to substitute for the the SelfType's TypeArg. That's the only case in which we expect to see a // SelfType being part of a substitution operation at all. - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } } diff --git a/Source/DafnyCore/AST/Types/UserDefinedType.cs b/Source/DafnyCore/AST/Types/UserDefinedType.cs index cc97c154dc9..05ac46e928e 100644 --- a/Source/DafnyCore/AST/Types/UserDefinedType.cs +++ b/Source/DafnyCore/AST/Types/UserDefinedType.cs @@ -11,7 +11,7 @@ public class UserDefinedType : NonProxyType, IHasReferences { void ObjectInvariant() { Contract.Invariant(tok != null); Contract.Invariant(Name != null); - Contract.Invariant(cce.NonNullElements(TypeArgs)); + Contract.Invariant(Cce.NonNullElements(TypeArgs)); Contract.Invariant(NamePath is NameSegment or ExprDotName); Contract.Invariant(!ArrowType.IsArrowTypeName(Name) || this is ArrowType); } @@ -151,7 +151,7 @@ public UserDefinedType(IToken tok, string name, TopLevelDecl cd, [Captured] List Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cd != null); - Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(Cce.NonNullElements(typeArgs)); Contract.Requires(cd.TypeArgs.Count == typeArgs.Count); Contract.Requires(namePath == null || namePath is NameSegment || namePath is ExprDotName); // The following is almost a precondition. In a few places, the source program names a class, not a type, diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 99f4c54c6f5..dbc622e5a73 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -281,7 +281,7 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef const string DafnyTypeDescriptor = "Dafny.TypeDescriptor"; internal string TypeParameters(List/*?*/ targs, bool addVariance = false, bool uniqueNames = false) { - Contract.Requires(targs == null || cce.NonNullElements(targs)); + Contract.Requires(targs == null || Cce.NonNullElements(targs)); Contract.Ensures(Contract.Result() != null); if (targs == null || targs.Count == 0) { @@ -1371,7 +1371,7 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name, break; default: Contract.Assert(false); // unexpected native type - throw new cce.UnreachableException(); // to please the compiler + throw new Cce.UnreachableException(); // to please the compiler } } @@ -1429,7 +1429,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, } public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) { - throw new cce.UnreachableException(); // InitializeField should be called only for those compilers that set ClassesRedeclareInheritedFields to false. + throw new Cce.UnreachableException(); // InitializeField should be called only for those compilers that set ClassesRedeclareInheritedFields to false. } public ConcreteSyntaxTree /*?*/ ErrorWriter() => InstanceMemberWriter; @@ -1618,7 +1618,7 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, Type ranType = ((MapType)xType).Range; return DafnyIMap + "<" + TypeName(domType, wr, tok) + "," + TypeName(ranType, wr, tok) + ">"; } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -1759,7 +1759,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } return string.Format($"{s}.Default({wDefaultTypeArguments}{sep}{arguments})"); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -1854,7 +1854,7 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IToke return AddTypeDescriptorArgs(FullTypeName(udt, ignoreInterface: true), udt, relevantTypeArgs, wr, tok); } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } } @@ -1879,7 +1879,7 @@ private string GetNativeTypeDescriptor(NativeType nt) { return $"Dafny.Helpers.UINT64"; default: Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } @@ -2262,7 +2262,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { wr.Write("\"))"); } } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected literal } } @@ -2861,7 +2861,7 @@ protected override void EmitMultiSetFormingExpr(MultiSetFormingExpr expr, bool i } else if (eeType is SetType) { TrParenExpr(".FromSet", expr.E, wr, inLetExprBody, wStmts); } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } } @@ -3032,7 +3032,7 @@ protected override void EmitUnaryExpr(ResolvedUnaryOp op, Expression expr, bool } break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected unary expression } } @@ -3435,7 +3435,7 @@ protected override void GetCollectionBuilder_Build(CollectionType ct, IToken tok wr.Write($"{DafnyMapClass}<{domtypeName},{rantypeName}>.FromCollection({collName})"); } else { Contract.Assume(false); // unexpected collection type - throw new cce.UnreachableException(); // please compiler + throw new Cce.UnreachableException(); // please compiler } } diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index be83d5f912b..cdd2dc15831 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -173,7 +173,7 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef } private string TypeParameters(List targs) { - Contract.Requires(cce.NonNullElements(targs)); + Contract.Requires(Cce.NonNullElements(targs)); Contract.Ensures(Contract.Result() != null); if (targs != null) { return Util.Comma(targs, tp => "typename " + IdName(tp)); @@ -700,7 +700,7 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name, break; default: Contract.Assert(false); // unexpected native type - throw new cce.UnreachableException(); // to please the compiler + throw new Cce.UnreachableException(); // to please the compiler } } @@ -749,7 +749,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, CodeGenerator.DeclareField(ClassName, enclosingDecl.TypeArgs, name, isStatic, isConst, type, tok, rhs, FieldWriter, Finisher); } public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) { - throw new cce.UnreachableException(); // InitializeField should be called only for those compilers that set ClassesRedeclareInheritedFields to false. + throw new Cce.UnreachableException(); // InitializeField should be called only for those compilers that set ClassesRedeclareInheritedFields to false. } public ConcreteSyntaxTree/*?*/ ErrorWriter() => MethodWriter; public void Finish() { } @@ -984,7 +984,7 @@ protected string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDe } return DafnyMapClass + "<" + TypeName(domType, wr, tok) + "," + TypeName(ranType, wr, tok) + ">"; } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -1098,7 +1098,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree w.Write("{0}{1}()", s, InstantiateTemplate(udt.TypeArgs)); return w.ToString(); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -1462,7 +1462,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { } else if (e.Value is BaseTypes.BigDec) { throw new UnsupportedFeatureException(e.tok, Feature.RealNumbers); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected literal } } void EmitIntegerLiteral(BigInteger i, ConcreteSyntaxTree wr) { @@ -2033,7 +2033,7 @@ protected override void EmitUnaryExpr(ResolvedUnaryOp op, Expression expr, bool wr.Write(".size()"); break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected unary expression } } @@ -2274,7 +2274,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op, preOpString = "!"; callString = "contains"; reverseArguments = true; break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected binary expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected binary expression } } @@ -2444,7 +2444,7 @@ protected override void EmitSetBuilder_Add(CollectionType ct, string collName, E Contract.Assume(ct is SetType || ct is MultiSetType); // follows from precondition if (ct is MultiSetType) { // This should never occur since there is no syntax for multiset comprehensions yet - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } var wStmts = wr.Fork(); wr.Write("{0}.set.emplace(", collName); diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index 0bb731ae39f..4e60aa98d9d 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -618,7 +618,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, } public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) { - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } public ConcreteSyntaxTree ErrorWriter() => null; @@ -1381,7 +1381,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { break; default: // TODO: This may not be exhaustive - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } break; } diff --git a/Source/DafnyCore/Backends/DatatypeWrapperEraser.cs b/Source/DafnyCore/Backends/DatatypeWrapperEraser.cs index efe344eeab8..7c1f256b056 100644 --- a/Source/DafnyCore/Backends/DatatypeWrapperEraser.cs +++ b/Source/DafnyCore/Backends/DatatypeWrapperEraser.cs @@ -58,7 +58,7 @@ Type ExpandType(Type typ) { case SimplifyTypeExpandMode.ExpandSynonymsAndSubsetTypesAndNewtypesExceptNativeTypes: return typ.GetRuntimeType(); default: Contract.Assert(false); // unexpected case - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index a8007611a29..f2bd5a046d0 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -1187,7 +1187,7 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name, break; default: Contract.Assert(false); // unexpected native type - throw new cce.UnreachableException(); // to please the compiler + throw new Cce.UnreachableException(); // to please the compiler } } protected class ClassWriter : IClassWriter { @@ -1513,7 +1513,7 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IToke return w.ToString(); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -1637,7 +1637,7 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, } else if (xType is MapType) { return "_dafny.Map"; } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -1746,7 +1746,7 @@ string nil() { var arguments = relevantTypeArgs.Comma(ta => DefaultValue(ta.Actual, wr, tok, constructTypeParameterDefaultsFromTypeDescriptors)); return $"{n}({wTypeDescriptorArguments}{sep}{arguments})"; } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -2282,7 +2282,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { } wr.Write("_dafny.RealOfString(\"{0}\")", str); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected literal } } void EmitIntegerLiteral(BigInteger i, ConcreteSyntaxTree wr) { @@ -3203,7 +3203,7 @@ void TrExprToBigInt(Expression e, ConcreteSyntaxTree wr, bool inLetExprBody) { wr.Write($"IntOfInt64("); break; default: - throw new cce.UnreachableException(); // unexpected nativeType.Selection value + throw new Cce.UnreachableException(); // unexpected nativeType.Selection value } } @@ -3240,7 +3240,7 @@ protected override void EmitMultiSetFormingExpr(MultiSetFormingExpr expr, bool i } else if (eeType is SetType) { TrParenExpr("_dafny.MultiSetFromSet", expr.E, wr, inLetExprBody, wStmts); } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } } @@ -3354,7 +3354,7 @@ protected override void EmitUnaryExpr(ResolvedUnaryOp op, Expression expr, bool break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected unary expression } } diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index 8fd4afa98c2..9137c1e5f13 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -107,7 +107,7 @@ private static JavaNativeType AsJavaNativeType(NativeType.Selection sel) { return JavaNativeType.Long; default: Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } @@ -479,7 +479,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, CodeGenerator.DeclareField(name, isStatic, isConst, type, tok, rhs, this); } public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) { - throw new cce.UnreachableException(); // InitializeField should be called only for those compilers that set ClassesRedeclareInheritedFields to false. + throw new Cce.UnreachableException(); // InitializeField should be called only for those compilers that set ClassesRedeclareInheritedFields to false. } public ConcreteSyntaxTree/*?*/ ErrorWriter() => InstanceMemberWriter; @@ -645,7 +645,7 @@ private void EmitSuppression(ConcreteSyntaxTree wr) { } string TypeParameters(List/*?*/ targs, string suffix = "") { - Contract.Requires(targs == null || cce.NonNullElements(targs)); + Contract.Requires(targs == null || Cce.NonNullElements(targs)); Contract.Ensures(Contract.Result() != null); if (targs == null || targs.Count == 0) { @@ -772,7 +772,7 @@ private string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, bool boxed } return $"{DafnyMapClass}<{ActualTypeArgument(domType, TypeParameter.TPVariance.Co, wr, tok)}, {ActualTypeArgument(ranType, TypeParameter.TPVariance.Co, wr, tok)}>"; } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -802,7 +802,7 @@ protected string CollectionTypeUnparameterizedName(CollectionType ct) { return DafnyMapClass; } else { Contract.Assert(false); // unexpected collection type - throw new cce.UnreachableException(); // to please the compiler + throw new Cce.UnreachableException(); // to please the compiler } } @@ -1072,7 +1072,7 @@ private void EmitTypeDescriptorMethod([CanBeNull] TopLevelDecl enclosingTypeDecl break; default: Contract.Assert(false); // unexpected case - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } @@ -1170,7 +1170,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { wr.Write("\"))"); } } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected literal } } @@ -1224,7 +1224,7 @@ protected string GetNativeDefault(NativeType nt) { case JavaNativeType.Long: return "0L"; default: Contract.Assert(false); // unexpected native type - throw new cce.UnreachableException(); // to please the compiler + throw new Cce.UnreachableException(); // to please the compiler } } @@ -1239,7 +1239,7 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name, case JavaNativeType.Long: name = "long"; literalSuffix = "L"; break; default: Contract.Assert(false); // unexpected native type - throw new cce.UnreachableException(); // to please the compiler + throw new Cce.UnreachableException(); // to please the compiler } } @@ -1255,7 +1255,7 @@ private string GetBoxedNativeTypeName(NativeType nt) { case JavaNativeType.Long: return "java.lang.Long"; default: Contract.Assert(false); // unexpected native type - throw new cce.UnreachableException(); // to please the compiler + throw new Cce.UnreachableException(); // to please the compiler } } @@ -2359,7 +2359,7 @@ private ConcreteSyntaxTree EmitToString(ConcreteSyntaxTree wr, Type type) { default: // Should be an unsigned type by assumption Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } else { bool isGeneric = type.NormalizeToAncestorType().AsSeqType is { Arg: { IsTypeParameter: true } }; @@ -2579,7 +2579,7 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IToke case JavaNativeType.Long: return $"{DafnyTypeDescriptor}.LONG_ARRAY"; default: Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } else { return $"(({DafnyTypeDescriptor}<{BoxedTypeName(type, wr, tok)}>)({TypeDescriptor(elType, wr, tok)}).arrayType())"; @@ -2632,7 +2632,7 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IToke return AddTypeDescriptorArgs(s, udt.TypeArgs, relevantTypeArgs, wr, udt.tok); } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } } @@ -2642,7 +2642,7 @@ private string GetNativeTypeDescriptor(NativeType nt) { case JavaNativeType.Short: return $"{DafnyTypeDescriptor}.SHORT"; case JavaNativeType.Int: return $"{DafnyTypeDescriptor}.INT"; case JavaNativeType.Long: return $"{DafnyTypeDescriptor}.LONG"; - default: Contract.Assert(false); throw new cce.UnreachableException(); + default: Contract.Assert(false); throw new Cce.UnreachableException(); } } @@ -2779,7 +2779,7 @@ protected override void EmitUnaryExpr(ResolvedUnaryOp op, Expression expr, bool break; } default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected unary expression } } @@ -2899,7 +2899,7 @@ void doPossiblyNativeBinOp(string o, string name, out string preOpS, out string break; default: Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } else { switch (op) { @@ -2917,7 +2917,7 @@ void doPossiblyNativeBinOp(string o, string name, out string preOpS, out string break; default: Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } break; @@ -3297,7 +3297,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree return $"{s}.{typeargs}Default({wDefaultTypeArguments}{sep}{arguments})"; } else { Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected type + throw new Cce.UnreachableException(); // unexpected type } } @@ -3575,7 +3575,7 @@ protected override void GetCollectionBuilder_Build(CollectionType ct, IToken tok wr.Write($"new {DafnyMapClass}<{domtypeName},{rantypeName}>({collName})"); } else { Contract.Assume(false); // unexpected collection type - throw new cce.UnreachableException(); // please compiler + throw new Cce.UnreachableException(); // please compiler } } @@ -4093,7 +4093,7 @@ private static int NativeTypeSize(NativeType nt) { case JavaNativeType.Short: return 16; case JavaNativeType.Int: return 32; case JavaNativeType.Long: return 64; - default: Contract.Assert(false); throw new cce.UnreachableException(); + default: Contract.Assert(false); throw new Cce.UnreachableException(); } } diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs index e2e71971cf2..1371ae1b840 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs +++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs @@ -664,7 +664,7 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name, break; default: Contract.Assert(false); // unexpected native type - throw new cce.UnreachableException(); // to please the compiler + throw new Cce.UnreachableException(); // to please the compiler } } @@ -703,7 +703,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, CodeGenerator.DeclareField(name, isStatic, isConst, type, tok, rhs, FieldWriter); } public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) { - throw new cce.UnreachableException(); // InitializeField should be called only for those compilers that set ClassesRedeclareInheritedFields to false. + throw new Cce.UnreachableException(); // InitializeField should be called only for those compilers that set ClassesRedeclareInheritedFields to false. } public ConcreteSyntaxTree/*?*/ ErrorWriter() => MethodWriter; public void Finish() { } @@ -852,7 +852,7 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IToke return TypeName_UDT(FullTypeName(udt), udt, wr, udt.tok); } } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -946,7 +946,7 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, } else if (xType is MapType) { return DafnyMapClass; } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -1050,7 +1050,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree var arguments = relevantTypeArgs.Comma(arg => DefaultValue(arg, wr, tok, constructTypeParameterDefaultsFromTypeDescriptors)); return string.Format($"{s}.Default({typeDescriptors}{sep}{arguments})"); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -1434,7 +1434,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { wr.Write("\"))"); } } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected literal } } string IntegerLiteral(BigInteger i) { @@ -2044,7 +2044,7 @@ protected override void EmitUnaryExpr(ResolvedUnaryOp op, Expression expr, bool } break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected unary expression } } @@ -2162,7 +2162,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op, } else if (IsRepresentedAsBigNumber(e0Type) || e0Type.IsNumericBased(Type.NumericPersuasion.Real)) { callString = "isLessThan"; } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } break; case BinaryExpr.ResolvedOpcode.Le: @@ -2173,7 +2173,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op, } else if (e0Type.IsNumericBased(Type.NumericPersuasion.Real)) { callString = "isAtMost"; } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } break; case BinaryExpr.ResolvedOpcode.Ge: @@ -2186,7 +2186,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op, callString = "isAtMost"; reverseArguments = true; } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } break; case BinaryExpr.ResolvedOpcode.Gt: @@ -2196,7 +2196,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op, callString = "isLessThan"; reverseArguments = true; } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } break; case BinaryExpr.ResolvedOpcode.LtChar when UnicodeCharEnabled: diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs index 81e3a5b7212..436ac23ec95 100644 --- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs @@ -519,7 +519,7 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name, name = "int"; break; default: Contract.Assert(false); // unexpected native type - throw new cce.UnreachableException(); // to please the compiler + throw new Cce.UnreachableException(); // to please the compiler } } @@ -569,7 +569,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, } public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) { - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } public ConcreteSyntaxTree ErrorWriter() => MethodWriter; @@ -690,9 +690,9 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IToke ClassLikeDecl or NonNullTypeDecl => $"{DafnyDefaults}.pointer", DatatypeDecl => DatatypeDescriptor(udt, udt.TypeArgs, udt.tok), NewtypeDecl or SubsetTypeDecl => CustomDescriptor(udt), - _ => throw new cce.UnreachableException() + _ => throw new Cce.UnreachableException() }, - _ => throw new cce.UnreachableException() + _ => throw new Cce.UnreachableException() }; string TypeParameterDescriptor(TypeParameter typeParameter) { @@ -781,7 +781,7 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, // TODO: I'm not 100% sure this is exhaustive yet Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } private string FullName(TopLevelDecl decl) { @@ -882,7 +882,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree } Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected type + throw new Cce.UnreachableException(); // unexpected type } protected override string TypeName_UDT(string fullCompileName, List variance, @@ -1156,7 +1156,7 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { break; default: // TODO: This may not be exhaustive - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } break; } @@ -1618,7 +1618,7 @@ protected override void EmitUnaryExpr(ResolvedUnaryOp op, Expression expr, bool TrParenExpr("not", expr, wr, inLetExprBody, wStmts); break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected unary expression } } @@ -1773,7 +1773,7 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op, } protected override void TrStmtList(List stmts, ConcreteSyntaxTree writer) { - Contract.Requires(cce.NonNullElements(stmts)); + Contract.Requires(Cce.NonNullElements(stmts)); Contract.Requires(writer != null); var listWriter = new ConcreteSyntaxTree(); base.TrStmtList(stmts, listWriter); diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs index 654a5af6623..c128fd28df7 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs @@ -274,7 +274,7 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn } case OldExpr: Contract.Assert(false); - throw new cce.UnreachableException(); // 'old' is always a ghost + throw new Cce.UnreachableException(); // 'old' is always a ghost case UnaryOpExpr opExpr: { var e = opExpr; if (e.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BVNot) { @@ -579,7 +579,7 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn } default: Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected expression + throw new Cce.UnreachableException(); // unexpected expression } ConcreteSyntaxTree EmitGuardFragment(List<(Expression conj, ISet frees)> unusedConjuncts, diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs index d4feaecdeac..f4502c36cbc 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs @@ -481,7 +481,7 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree EmitHaltRecoveryStmt(h.TryBody, IdName(h.HaltMessageVar), h.RecoverBody, wr); break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected statement } } @@ -503,7 +503,7 @@ private void EmitMatchStmt(ConcreteSyntaxTree wr, MatchStmt s) { int i = 0; var sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand(); foreach (MatchCaseStmt mc in s.Cases) { - var w = MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, wr); + var w = MatchCasePrelude(source, sourceType, Cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, wr); TrStmtList(mc.Body, w); i++; } diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index 7ad99fe4a9d..2158bbb836d 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -812,7 +812,7 @@ protected virtual bool CompareZeroUsingSign(Type type) { protected virtual ConcreteSyntaxTree EmitSign(Type type, ConcreteSyntaxTree wr) { // Currently, this should only be called when CompareZeroUsingSign is true Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } protected abstract void EmitEmptyTupleList(string tupleTypeArgs, ConcreteSyntaxTree wr); protected abstract ConcreteSyntaxTree EmitAddTupleToList(string ingredients, string tupleTypeArgs, ConcreteSyntaxTree wr); @@ -1396,7 +1396,7 @@ protected virtual void CompileBinOp(BinaryExpr.ResolvedOpcode op, default: // The operator is one that needs to be handled in the specific compilers. - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected binary expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected binary expression } if (dualOp != BinaryExpr.ResolvedOpcode.Add) { // remember from above that Add stands for "there is no dual" @@ -2346,7 +2346,7 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite } v.Visit(m); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected member } thisContext = null; @@ -2737,7 +2737,7 @@ private void CompileFunction(Function f, IClassWriter cw, bool lookasideBody) { unit.Type = f.ResultType; } else { Contract.Assert(false); // unexpected type - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } DeclareLocalVar(IdName(accVar), accVar.Type, f.tok, unit, false, w); } @@ -3125,7 +3125,7 @@ protected void TrExprOpt(Expression expr, Type resultType, ConcreteSyntaxTree wr break; default: Contract.Assert(false); // unexpected TailStatus - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } else { Contract.Assert(accumulatorVar == null); @@ -3196,7 +3196,7 @@ protected bool ComplicatedTypeParameterForCompilation(TypeParameter.TPVariance v } protected string/*!*/ TypeNames(List/*!*/ types, ConcreteSyntaxTree wr, IToken tok) { - Contract.Requires(cce.NonNullElements(types)); + Contract.Requires(Cce.NonNullElements(types)); Contract.Ensures(Contract.Result() != null); return Util.Comma(types, ty => TypeName(ty, wr, tok)); } @@ -3494,7 +3494,7 @@ Type CompileCollection(BoundedPool bound, IVariable bv, bool inLetExprBody, bool ResolvedClass = b.Decl }; } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected BoundedPool type } } @@ -4634,7 +4634,7 @@ protected virtual void TrDividedBlockStmt(Constructor m, DividedBlockStmt divide } protected virtual void TrStmtList(List stmts, ConcreteSyntaxTree writer) { - Contract.Requires(cce.NonNullElements(stmts)); + Contract.Requires(Cce.NonNullElements(stmts)); Contract.Requires(writer != null); foreach (Statement ss in stmts) { // label: // if any @@ -4674,7 +4674,7 @@ ConcreteSyntaxTree MatchCasePrelude(string source, UserDefinedType sourceType, D Contract.Requires(source != null); Contract.Requires(sourceType != null); Contract.Requires(ctor != null); - Contract.Requires(cce.NonNullElements(arguments)); + Contract.Requires(Cce.NonNullElements(arguments)); Contract.Requires(0 <= caseIndex && caseIndex < caseCount); // if (source.is_Ctor0) { // FormalType f0 = ((Dt_Ctor0)source._D).a0; @@ -4738,7 +4738,7 @@ protected void TrParenExpr(Expression expr, ConcreteSyntaxTree wr, bool inLetExp /// protected void TrExprList(List exprs, ConcreteSyntaxTree wr, bool inLetExprBody, ConcreteSyntaxTree wStmts, Func typeAt = null, bool parens = true) { - Contract.Requires(cce.NonNullElements(exprs)); + Contract.Requires(Cce.NonNullElements(exprs)); if (parens) { wr = wr.ForkInParens(); } wr.Comma(exprs, (e, index) => { diff --git a/Source/DafnyCore/CompileNestedMatch/MatchAst.cs b/Source/DafnyCore/CompileNestedMatch/MatchAst.cs index a3dcffd4d2e..6fb6a383729 100644 --- a/Source/DafnyCore/CompileNestedMatch/MatchAst.cs +++ b/Source/DafnyCore/CompileNestedMatch/MatchAst.cs @@ -15,15 +15,15 @@ public class MatchExpr : Expression, IMatch, ICloneable { // a Match [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Source != null); - Contract.Invariant(cce.NonNullElements(Cases)); - Contract.Invariant(cce.NonNullElements(MissingCases)); + Contract.Invariant(Cce.NonNullElements(Cases)); + Contract.Invariant(Cce.NonNullElements(MissingCases)); } public MatchExpr(IToken tok, Expression source, [Captured] List cases, bool usesOptionalBraces, MatchingContext context = null) : base(tok) { Contract.Requires(tok != null); Contract.Requires(source != null); - Contract.Requires(cce.NonNullElements(cases)); + Contract.Requires(Cce.NonNullElements(cases)); this.source = source; this.cases = cases; this.UsesOptionalBraces = usesOptionalBraces; @@ -89,13 +89,13 @@ public abstract class MatchCase : TokenNode, IHasReferences { void ObjectInvariant() { Contract.Invariant(tok != null); Contract.Invariant(Ctor != null); - Contract.Invariant(cce.NonNullElements(Arguments)); + Contract.Invariant(Cce.NonNullElements(Arguments)); } public MatchCase(IToken tok, DatatypeCtor ctor, [Captured] List arguments) { Contract.Requires(tok != null); Contract.Requires(ctor != null); - Contract.Requires(cce.NonNullElements(arguments)); + Contract.Requires(Cce.NonNullElements(arguments)); this.tok = tok; this.Ctor = ctor; this.Arguments = arguments; @@ -117,8 +117,8 @@ public class MatchStmt : Statement, IMatch, ICloneable { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Source != null); - Contract.Invariant(cce.NonNullElements(Cases)); - Contract.Invariant(cce.NonNullElements(MissingCases)); + Contract.Invariant(Cce.NonNullElements(Cases)); + Contract.Invariant(Cce.NonNullElements(MissingCases)); } private Expression source; @@ -147,7 +147,7 @@ public MatchStmt(RangeToken rangeToken, Expression source, [Captured] List Children => body; @@ -237,8 +237,8 @@ public MatchCaseStmt(RangeToken rangeToken, DatatypeCtor ctor, bool fromBoundVar RangeToken = rangeToken; Contract.Requires(tok != null); Contract.Requires(ctor != null); - Contract.Requires(cce.NonNullElements(arguments)); - Contract.Requires(cce.NonNullElements(body)); + Contract.Requires(Cce.NonNullElements(arguments)); + Contract.Requires(Cce.NonNullElements(body)); this.body = body; this.Attributes = attrs; this.FromBoundVar = fromBoundVar; @@ -270,7 +270,7 @@ public MatchCaseExpr(IToken tok, DatatypeCtor ctor, bool FromBoundVar, [Captured : base(tok, ctor, arguments) { Contract.Requires(tok != null); Contract.Requires(ctor != null); - Contract.Requires(cce.NonNullElements(arguments)); + Contract.Requires(Cce.NonNullElements(arguments)); Contract.Requires(body != null); this.body = body; this.Attributes = attrs; diff --git a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs index 33837e33690..2c8ad787a46 100644 --- a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs +++ b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs @@ -110,7 +110,7 @@ private Expression CompileNestedMatchExpr(NestedMatchExpr nestedMatchExpr) { } return expression; } - Contract.Assert(false); throw new cce.UnreachableException(); // Returned container should be a CExpr + Contract.Assert(false); throw new Cce.UnreachableException(); // Returned container should be a CExpr } private Statement CompileNestedMatchStmt(NestedMatchStmt nestedMatchStmt) { @@ -144,7 +144,7 @@ private Statement CompileNestedMatchStmt(NestedMatchStmt nestedMatchStmt) { Visit(result, nestedMatchStmt.IsGhost, null); return result; } - Contract.Assert(false); throw new cce.UnreachableException(); // Returned container should be a StmtContainer + Contract.Assert(false); throw new Cce.UnreachableException(); // Returned container should be a StmtContainer } private IEnumerable FlattenNestedMatchCaseStmt(NestedMatchCaseStmt c) { @@ -271,7 +271,7 @@ private CaseBody CompilePatternPathsForMatchee(MatchCompilationState state, Matc var (head, tail) = SplitPath(path); if (!(head is IdPattern)) { Contract.Assert(false); - throw new cce.UnreachableException(); // in Variable case with a constant pattern + throw new Cce.UnreachableException(); // in Variable case with a constant pattern } var currPattern = (IdPattern)head; @@ -279,7 +279,7 @@ private CaseBody CompilePatternPathsForMatchee(MatchCompilationState state, Matc if (currPattern.Arguments != null) { if (dtd == null) { Contract.Assert(false); - throw new cce.UnreachableException(); // non-nullary constructors of a non-datatype; + throw new Cce.UnreachableException(); // non-nullary constructors of a non-datatype; } else { Reporter.Error(MessageSource.Resolver, currPattern.Tok, "Type mismatch: expected constructor of type {0}. Got {1}.", dtd.Name, currPattern.Id); @@ -367,7 +367,7 @@ private CaseBody CompileHeadsContainingConstructor(MatchCompilationState mti, Ma ctorToFromBoundVar.Add(ctor.Name); } } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } } // Add variables corresponding to the arguments of the current constructor (ctor) to the matchees @@ -482,7 +482,7 @@ private CaseBody CompileHeadsContainingLiteralPattern(MatchCompilationState mti, mti.UpdateCaseCopyCount(tail.CaseId, 1); pathsForLiteral.Add(newPath); } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } } var blockContext = context.FillHole(new LitCtx(ifBlockLiteral)); @@ -578,7 +578,7 @@ private CaseBody CreateIfElseIfChain(MatchCompilationState mti, MatchingContext } } - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } record CaseBody(IToken Tok, Node Node, Attributes Attributes = null); @@ -592,7 +592,7 @@ private CaseBody PackBody(IToken tok, PatternPath path) { return new CaseBody(tok, ((ExprPatternPath)path).Body, ((ExprPatternPath)path).Attributes); } - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } private List UnboxStmt(Statement statement) { diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index c8fe3ccaa02..26fc1aefd41 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -595,7 +595,7 @@ TraitDecl mm, bool allowConstructors, bool moduleLevelDecl.> -= (. Contract.Requires(cce.NonNullElements(mm)); += (. Contract.Requires(Cce.NonNullElements(mm)); Method/*!*/ m; Function/*!*/ f; .) @@ -671,7 +671,7 @@ DatatypeDecl = NoUSIdentOrDigits . DatatypeMemberDecl<.List/*!*/ ctors.> -= (. Contract.Requires(cce.NonNullElements(ctors)); += (. Contract.Requires(Cce.NonNullElements(ctors)); Attributes attrs = null; IToken/*!*/ id; List formals = new List(); @@ -702,7 +702,7 @@ TypeMembers<. ModuleDefinition/*!*/ module, List members .> /*------------------------------------------------------------------------*/ FieldDecl<.DeclModifierData dmod, List mm.> -= (. Contract.Requires(cce.NonNullElements(mm)); += (. Contract.Requires(Cce.NonNullElements(mm)); Attributes attrs = null; Type/*!*/ ty; Name name; @@ -725,7 +725,7 @@ FieldDecl<.DeclModifierData dmod, List mm.> /*------------------------------------------------------------------------*/ ConstantFieldDecl<.DeclModifierData dmod, List/*!*/ mm, bool moduleLevelDecl.> -= (. Contract.Requires(cce.NonNullElements(mm)); += (. Contract.Requires(Cce.NonNullElements(mm)); Attributes attrs = null; Type/*!*/ ty; Expression e = null; @@ -1067,7 +1067,7 @@ IteratorDecl = Name . GenericParameters<.List/*!*/ typeArgs, bool allowVariance.> -= (. Contract.Requires(cce.NonNullElements(typeArgs)); += (. Contract.Requires(Cce.NonNullElements(typeArgs)); TypeParameter.TypeParameterCharacteristics characteristics; TypeParameter.TPVarianceSyntax variance = TypeParameter.TPVarianceSyntax.NonVariant_Strict; // assignment is to please compiler characteristics = new TypeParameter.TypeParameterCharacteristics(false); @@ -1361,11 +1361,11 @@ InvariantClause<. List invariants.> = /*------------------------------------------------------------------------*/ MethodSpec<.bool isGhost, List req, List reads, List mod, List ens, List decreases, ref Attributes decAttrs, ref Attributes modAttrs, ref Attributes readsAttrs, string caption, bool performThisDeprecatedCheck.> -= (. Contract.Requires(cce.NonNullElements(req)); - Contract.Requires(cce.NonNullElements(reads)); - Contract.Requires(cce.NonNullElements(mod)); - Contract.Requires(cce.NonNullElements(ens)); - Contract.Requires(cce.NonNullElements(decreases)); += (. Contract.Requires(Cce.NonNullElements(req)); + Contract.Requires(Cce.NonNullElements(reads)); + Contract.Requires(Cce.NonNullElements(mod)); + Contract.Requires(Cce.NonNullElements(ens)); + Contract.Requires(Cce.NonNullElements(decreases)); .) SYNC { ReadsClause @@ -1397,7 +1397,7 @@ IteratorSpec<.List/*!*/ reads, List/ /*------------------------------------------------------------------------*/ Formals<.bool incoming, bool allowGhostKeyword, bool allowNewKeyword, bool allowOlderKeyword, List formals.> -= (. Contract.Requires(cce.NonNullElements(formals)); += (. Contract.Requires(Cce.NonNullElements(formals)); Type ty; bool isGhost; bool isOld; @@ -1443,7 +1443,7 @@ ParameterDefaultValue /*------------------------------------------------------------------------*/ FormalsOptionalIds<.List/*!*/ formals.> -= (. Contract.Requires(cce.NonNullElements(formals)); += (. Contract.Requires(Cce.NonNullElements(formals)); RangeToken/*!*/ range; Type/*!*/ ty; Name/*!*/ name; bool isGhost; Expression/*?*/ defaultValue; bool isNameOnly; Attributes attributes; @@ -1655,7 +1655,7 @@ OptGenericInstantiation<.out List gt, bool inExpressionContext.> /* NOTE: /*------------------------------------------------------------------------*/ GenericInstantiation<.List gt.> -= (. Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; .) += (. Contract.Requires(Cce.NonNullElements(gt)); Type/*!*/ ty; .) "<" ( ">" (. SemErr(ErrorId.p_no_empty_type_parameter_list, t, "empty type parameter lists are not permitted"); .) @@ -2014,9 +2014,9 @@ FunctionDecl /*------------------------------------------------------------------------*/ FunctionSpec<.List reqs, List reads, List ens, List decreases, ref Attributes decAttrs, ref Attributes readsAttrs.> -= (. Contract.Requires(cce.NonNullElements(reqs)); - Contract.Requires(cce.NonNullElements(reads)); - Contract.Requires(decreases == null || cce.NonNullElements(decreases)); += (. Contract.Requires(Cce.NonNullElements(reqs)); + Contract.Requires(Cce.NonNullElements(reads)); + Contract.Requires(decreases == null || Cce.NonNullElements(decreases)); .) SYNC { RequiresClause @@ -2662,7 +2662,7 @@ WhileStmt (. stmt = new AlternativeLoopStmt(new RangeToken(startToken, t), invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), alternatives, usesOptionalBraces, attrs); .) | - ( Guard (. Contract.Assume(guard == null || cce.Owner.None(guard)); .) + ( Guard (. Contract.Assume(guard == null || Cce.Owner.None(guard)); .) | ellipsis (. guardEllipsis = t; errors.Deprecated(ErrorId.p_deprecated_statement_refinement, t, "the ... refinement feature in statements is deprecated"); .) diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index ebf85839d83..b01bce194c3 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -17,7 +17,7 @@ true ..\..\Binaries\ TRACE - net6.0 + net8.0 MIT $(NoWarn);NU5104 @@ -34,7 +34,17 @@ - + + + + + + + + + + + diff --git a/Source/DafnyCore/DafnyMain.cs b/Source/DafnyCore/DafnyMain.cs index 4074baaf226..17f70aa3541 100644 --- a/Source/DafnyCore/DafnyMain.cs +++ b/Source/DafnyCore/DafnyMain.cs @@ -117,8 +117,8 @@ public static string Resolve(Program program) { if (options.PrintFile != null) { bplFilename = options.PrintFile; } else { - string baseName = cce.NonNull(Path.GetFileName(baseFile)); - baseName = cce.NonNull(Path.ChangeExtension(baseName, "bpl")); + string baseName = Cce.NonNull(Path.GetFileName(baseFile)); + baseName = Cce.NonNull(Path.ChangeExtension(baseName, "bpl")); bplFilename = Path.Combine(Path.GetTempPath(), baseName); } @@ -193,7 +193,7 @@ await options.OutputWriter.WriteLineAsync( default: Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected outcome + throw new Cce.UnreachableException(); // unexpected outcome } } } diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 6ef92d58f0c..f396a03c134 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -224,10 +224,10 @@ public override void Error(string message, params string[] args) { /// public bool BaseParse(string[] args, bool allowFile) { Environment = Environment + "Command Line Options: " + string.Join(" ", args); - args = cce.NonNull((string[])args.Clone()); + args = Cce.NonNull((string[])args.Clone()); Bpl.CommandLineParseState state; for (state = InitializeCommandLineParseState(args); state.i < args.Length; state.i = state.nextIndex) { - cce.LoopInvariant(state.args == args); + Cce.LoopInvariant(state.args == args); string file = args[state.i]; state.s = file.Trim(); bool flag = state.s.StartsWith("-") || state.s.StartsWith("/"); diff --git a/Source/DafnyCore/Generic/ConsoleErrorReporter.cs b/Source/DafnyCore/Generic/ConsoleErrorReporter.cs index 8bdd061acc1..128ae45a023 100644 --- a/Source/DafnyCore/Generic/ConsoleErrorReporter.cs +++ b/Source/DafnyCore/Generic/ConsoleErrorReporter.cs @@ -14,7 +14,7 @@ private ConsoleColor ColorForLevel(ErrorLevel level) { case ErrorLevel.Info: return ConsoleColor.Green; default: - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } diff --git a/Source/DafnyCore/Generic/SccGraph.cs b/Source/DafnyCore/Generic/SccGraph.cs index aed140270df..f39e4083893 100644 --- a/Source/DafnyCore/Generic/SccGraph.cs +++ b/Source/DafnyCore/Generic/SccGraph.cs @@ -16,8 +16,8 @@ public class Vertex { public List SccMembers; // non-null only for the representative of the SCC [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(Successors)); - Contract.Invariant(SccMembers == null || cce.NonNullElements(SccMembers)); + Contract.Invariant(Cce.NonNullElements(Successors)); + Contract.Invariant(SccMembers == null || Cce.NonNullElements(SccMembers)); } public Vertex SccRepresentative; // null if not computed @@ -60,8 +60,8 @@ private void ComputeSccPredecessorCounts() { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(vertices != null); - Contract.Invariant(cce.NonNullElements(vertices.Values)); - Contract.Invariant(topologicallySortedRepresentatives == null || cce.NonNullElements(topologicallySortedRepresentatives)); + Contract.Invariant(Cce.NonNullElements(vertices.Values)); + Contract.Invariant(topologicallySortedRepresentatives == null || Cce.NonNullElements(topologicallySortedRepresentatives)); Contract.Invariant(!sccComputed || topologicallySortedRepresentatives != null); } @@ -175,7 +175,7 @@ Vertex GetSCCRepr(Node n) { /// Returns a list of the topologically sorted SCCs, each represented in the list by its representative node. /// public List TopologicallySortedComponents() { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Ensures(Cce.NonNullElements(Contract.Result>())); ComputeSCCs(); Contract.Assert(topologicallySortedRepresentatives != null); // follows from object invariant return topologicallySortedRepresentatives.ConvertAll(v => v.N); @@ -186,7 +186,7 @@ public List TopologicallySortedComponents() { /// that contains 'n'. /// public List GetSCC(Node n) { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Ensures(Cce.NonNullElements(Contract.Result>())); Vertex v = GetVertex(n); ComputeSCCs(); Vertex repr = v.SccRepresentative; @@ -249,7 +249,7 @@ void ComputeSCCs() { /// void SearchC(Vertex/*!*/ v, Stack/*!*/ stack, ref int cnt) { Contract.Requires(v != null); - Contract.Requires(cce.NonNullElements(stack)); + Contract.Requires(Cce.NonNullElements(stack)); Contract.Requires(v.Visited == VisitedStatus.Unvisited); Contract.Requires(topologicallySortedRepresentatives != null); Contract.Ensures(v.Visited != VisitedStatus.Unvisited); diff --git a/Source/DafnyCore/Resolver/BoundsDiscovery/BoundsDiscovery.cs b/Source/DafnyCore/Resolver/BoundsDiscovery/BoundsDiscovery.cs index 137a9f10e91..75b67139b77 100644 --- a/Source/DafnyCore/Resolver/BoundsDiscovery/BoundsDiscovery.cs +++ b/Source/DafnyCore/Resolver/BoundsDiscovery/BoundsDiscovery.cs @@ -448,7 +448,7 @@ private static List DiscoverAllBounds_Aux_SingleVar(List bv case BinaryExpr.ResolvedOpcode.Gt: case BinaryExpr.ResolvedOpcode.Ge: Contract.Assert(false); - throw new cce.UnreachableException(); // promised by postconditions of NormalizedConjunct + throw new Cce.UnreachableException(); // promised by postconditions of NormalizedConjunct case BinaryExpr.ResolvedOpcode.Lt: if (e0.Type.IsNumericBased(Type.NumericPersuasion.Int)) { conjunctsQualifyingAsRangeConstraints++; diff --git a/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs b/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs index b183a06771d..2f926b296f5 100644 --- a/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs +++ b/Source/DafnyCore/Resolver/CheckTypeCharacteristics_Visitor.cs @@ -320,7 +320,7 @@ public void VisitType(IToken tok, Type type, bool inGhostContext) { } else if (type is TypeProxy) { // the type was underconstrained; this is checked elsewhere, but it is not in violation of the equality-type test } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } diff --git a/Source/DafnyCore/Resolver/ExpressionTester.cs b/Source/DafnyCore/Resolver/ExpressionTester.cs index feffd1b2b7c..c3ef48e7041 100644 --- a/Source/DafnyCore/Resolver/ExpressionTester.cs +++ b/Source/DafnyCore/Resolver/ExpressionTester.cs @@ -479,7 +479,7 @@ public static bool UsesSpecFeatures(Expression expr) { return false; } else if (expr is IdentifierExpr) { IdentifierExpr e = (IdentifierExpr)expr; - return cce.NonNull(e.Var).IsGhost; + return Cce.NonNull(e.Var).IsGhost; } else if (expr is DatatypeValue) { var e = (DatatypeValue)expr; if (e.Ctor.IsGhost) { @@ -644,7 +644,7 @@ public static bool UsesSpecFeatures(Expression expr) { var e = (MultiSetFormingExpr)expr; return UsesSpecFeatures(e.E); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected expression } } static void MakeGhostAsNeeded(List> lhss) { diff --git a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs index 386f3b85c47..8522e687a28 100644 --- a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs +++ b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs @@ -485,7 +485,7 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC } } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } } diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 221695c558c..3dedc314f6c 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -1048,8 +1048,8 @@ public void ResolveTopLevelDecls_Core(List declarations, string moduleDescription, bool isAnExport) { Contract.Requires(declarations != null); - Contract.Requires(cce.NonNullElements(datatypeDependencies.GetVertices())); - Contract.Requires(cce.NonNullElements(codatatypeDependencies.GetVertices())); + Contract.Requires(Cce.NonNullElements(datatypeDependencies.GetVertices())); + Contract.Requires(Cce.NonNullElements(codatatypeDependencies.GetVertices())); Contract.Requires(AllTypeConstraints.Count == 0); Contract.Ensures(AllTypeConstraints.Count == 0); @@ -2306,7 +2306,7 @@ void ResolveClassMemberTypes(TopLevelDeclWithMembers cl) { } } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected member type } } @@ -2586,7 +2586,7 @@ private bool AreThereAnyObviousSignsOfEmptiness(Type type, ISet /// void SccStratosphereCheck(IndDatatypeDecl startingPoint, Graph/*!*/ dependencies) { Contract.Requires(startingPoint != null); - Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies)); + Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(Cce.NonNullElements(dependencies)); var scc = dependencies.GetSCC(startingPoint); int totalCleared = 0; @@ -2734,7 +2734,7 @@ bool CheckCanBeConstructed(Type type, ISet typeParametersUsed) { void DetermineEqualitySupport(IndDatatypeDecl startingPoint, Graph/*!*/ dependencies) { Contract.Requires(startingPoint != null); - Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies)); + Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(Cce.NonNullElements(dependencies)); var scc = dependencies.GetSCC(startingPoint); @@ -3776,7 +3776,7 @@ public static BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, Type lef case BinaryExpr.Opcode.BitwiseOr: return BinaryExpr.ResolvedOpcode.BitwiseOr; case BinaryExpr.Opcode.BitwiseXor: return BinaryExpr.ResolvedOpcode.BitwiseXor; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected operator + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected operator } } diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 84d7f2337dc..34e9f012a4e 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -463,7 +463,7 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont e.Type = Type.String(); ResolveType(e.tok, e.Type, resolutionContext, ResolveTypeOptionEnum.DontInfer, null); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected literal type } } } else if (expr is ThisExpr) { @@ -763,7 +763,7 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont expr.Type = Type.Bool; break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary operator + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected unary operator } // We do not have enough information to compute `e.ResolvedOp` yet. @@ -965,7 +965,7 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected operator + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected operator } // We should also fill in e.ResolvedOp, but we may not have enough information for that yet. So, instead, delay // setting e.ResolvedOp until inside CheckTypeInference. @@ -1176,7 +1176,7 @@ public void ResolveExpressionX(Expression expr, ResolutionContext resolutionCont decreasesToExpr.Type = Type.Bool; } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected expression } if (expr.Type == null) { @@ -2817,7 +2817,7 @@ void ResolveClassMemberBodies(TopLevelDeclWithMembers cl) { } } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected member type } Contract.Assert(AllTypeConstraints.Count == 0); } @@ -2872,7 +2872,7 @@ void ResolveCtorSignature(DatatypeCtor ctor, List dtTypeArguments void AddDatatypeDependencyEdge(IndDatatypeDecl dt, Type tp, Graph dependencies) { Contract.Requires(dt != null); Contract.Requires(tp != null); - Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(dependencies)); + Contract.Requires(dependencies != null); // more expensive check: Contract.Requires(Cce.NonNullElements(dependencies)); tp = tp.NormalizeExpand(); var dependee = tp.AsIndDatatype; @@ -3780,7 +3780,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext } else if (s.Rhs is HavocRhs) { // nothing else to do } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected RHS + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected RHS } } else if (stmt is CallStmt) { @@ -4045,7 +4045,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext ResolveStatement(s.S, resolutionContext); } } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } } @@ -4322,7 +4322,7 @@ public ResolveTypeReturn ResolveTypeLenient(IToken tok, Type type, ResolutionCon } else if (type is SelfType) { // do nothing. } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } return null; } @@ -5091,7 +5091,7 @@ public void CheckVariance(Type type, TopLevelDecl enclosingTypeDefinition, TypeP } } } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -6091,9 +6091,9 @@ public void ResolveFunctionCallExpr(FunctionCallExpr e, ResolutionContext resolu if (member == null) { // error has already been reported by ResolveMember } else if (member is Method) { - reporter.Error(MessageSource.Resolver, e, "member {0} in type {1} refers to a method, but only functions can be used in this context", e.Name, cce.NonNull(ctype).Name); + reporter.Error(MessageSource.Resolver, e, "member {0} in type {1} refers to a method, but only functions can be used in this context", e.Name, Cce.NonNull(ctype).Name); } else if (!(member is Function)) { - reporter.Error(MessageSource.Resolver, e, "member {0} in type {1} does not refer to a function", e.Name, cce.NonNull(ctype).Name); + reporter.Error(MessageSource.Resolver, e, "member {0} in type {1} does not refer to a function", e.Name, Cce.NonNull(ctype).Name); } else { Function function = (Function)member; e.Function = function; diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs b/Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs index 7ee90aa0907..6b8eb9c75e9 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs @@ -117,7 +117,7 @@ Type StringDecl() { Target.Real => preTypeResolver.Type2PreType(Type.Real), Target.String => preTypeResolver.Type2PreType(StringDecl()), Target.Object => preTypeResolver.Type2PreType(preTypeResolver.resolver.SystemModuleManager.ObjectQ()), - _ => throw new cce.UnreachableException() // unexpected case + _ => throw new Cce.UnreachableException() // unexpected case }; return target; } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs index 900b0b6fcfd..7dae7fbe9fe 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs @@ -731,7 +731,7 @@ private bool ConfirmConstraint(CommonConfirmationBag check, PreType preType, DPr return true; default: Contract.Assert(false); // unexpected case - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs index 98ec7e26652..8631bf3ca3e 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs @@ -84,7 +84,7 @@ public void ResolveExpression(Expression expr, ResolutionContext resolutionConte Constraints.AddDefaultAdvice(e.PreType, CommonAdvice.Target.String); AddConfirmation(PreTypeConstraints.CommonConfirmationBag.InSeqFamily, e.PreType, e.tok, "string literal used as if it had type {0}"); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected literal type } } @@ -456,7 +456,7 @@ resolutionContext.CodeContext is ConstantField || expr.PreType = ConstrainResultToBoolFamily(expr.tok, "assigned", "boolean literal used as if it had type {0}"); break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary operator + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected unary operator } break; @@ -739,7 +739,7 @@ resolutionContext.CodeContext is ConstantField || Contract.Assert(false); // this case is always handled via NestedMatchExpr break; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected expression } if (expr.PreType == null) { @@ -1010,7 +1010,7 @@ private PreType ResolveBinaryExpr(IToken tok, BinaryExpr.Opcode opcode, Expressi default: Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected operator + throw new Cce.UnreachableException(); // unexpected operator } // We should also fill in e.ResolvedOp, but we may not have enough information for that yet. So, instead, delay // setting e.ResolvedOp until inside CheckTypeInference. diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs index b3e4551a0e0..906e0e97544 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs @@ -255,7 +255,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext } else if (s.Rhs is HavocRhs) { // nothing else to do } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected RHS + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected RHS } } else if (stmt is CallStmt callStmt) { @@ -416,7 +416,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext } } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } } diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs index c160ef4dcdb..f28cbf17050 100644 --- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs +++ b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs @@ -246,7 +246,7 @@ public TopLevelDecl Type2Decl(Type type) { } else if (type is UserDefinedType udt) { decl = udt.ResolvedClass; } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } return decl; } @@ -1137,7 +1137,7 @@ void ResolveMember(MemberDecl member) { } } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected member type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected member type } } diff --git a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs index 085ee36db8a..625792f9a46 100644 --- a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs +++ b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs @@ -518,7 +518,7 @@ static BinaryExpr.ResolvedOpcode ResolveOp(BinaryExpr.Opcode op, PreType leftOpe return BinaryExpr.ResolvedOpcode.BitwiseXor; default: Contract.Assert(false); - throw new cce.UnreachableException(); // unexpected operator + throw new Cce.UnreachableException(); // unexpected operator } } diff --git a/Source/DafnyCore/Resolver/TailRecursion.cs b/Source/DafnyCore/Resolver/TailRecursion.cs index 148e1377e26..47fc3172f87 100644 --- a/Source/DafnyCore/Resolver/TailRecursion.cs +++ b/Source/DafnyCore/Resolver/TailRecursion.cs @@ -581,7 +581,7 @@ Function.TailStatus CheckTailRecursiveExpr(Expression expr, Function enclosingFu } default: Contract.Assert(false); // unexpected case - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } // not an operator that allows accumulation, so drop down below diff --git a/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs b/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs index 1b0c06aa84f..83317370292 100644 --- a/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs +++ b/Source/DafnyCore/Resolver/TypeCharacteristicChecker.cs @@ -182,7 +182,7 @@ private static bool InferRequiredEqualitySupport(TypeParameter tp, Type type) { } } } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } return false; } diff --git a/Source/DafnyCore/Rewriters/AutoReqFunctionRewriter.cs b/Source/DafnyCore/Rewriters/AutoReqFunctionRewriter.cs index 311d89d3825..8e300d09bf8 100644 --- a/Source/DafnyCore/Rewriters/AutoReqFunctionRewriter.cs +++ b/Source/DafnyCore/Rewriters/AutoReqFunctionRewriter.cs @@ -381,7 +381,7 @@ List GenerateAutoReqs(Expression expr) { var e = (ConcreteSyntaxExpression)expr; reqs.AddRange(GenerateAutoReqs(e.ResolvedExpression)); } else { - //Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression + //Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected expression } return reqs; diff --git a/Source/DafnyCore/Rewriters/InductionHeuristic.cs b/Source/DafnyCore/Rewriters/InductionHeuristic.cs index 3787ab4303b..49ad78ef5b8 100644 --- a/Source/DafnyCore/Rewriters/InductionHeuristic.cs +++ b/Source/DafnyCore/Rewriters/InductionHeuristic.cs @@ -104,7 +104,7 @@ static bool VarOccursInArgumentToRecursiveFunction(DafnyOptions options, Express VarOccursInArgumentToRecursiveFunction(options, e.E1, n, subExprIsProminent) || VarOccursInArgumentToRecursiveFunction(options, e.E2, n, subExprIsProminent); default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected ternary expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected ternary expression } } else if (expr is DatatypeValue) { var e = (DatatypeValue)expr; diff --git a/Source/DafnyCore/Rewriters/RefinementTransformer.cs b/Source/DafnyCore/Rewriters/RefinementTransformer.cs index 235ce682616..262f1007b3b 100644 --- a/Source/DafnyCore/Rewriters/RefinementTransformer.cs +++ b/Source/DafnyCore/Rewriters/RefinementTransformer.cs @@ -1259,7 +1259,7 @@ List MergeStmtList(List skeleton, List oldStmt, } if (doMerge) { // Go ahead with the merge: - Contract.Assert(cce.NonNullElements(stmtGenerated)); + Contract.Assert(Cce.NonNullElements(stmtGenerated)); body.AddRange(stmtGenerated); i++; j++; } else { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs index f707a486cd8..9d49e958626 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs @@ -575,7 +575,7 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan return FunctionCall(tok, "AtLayer", typeInstantiation, args); default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected built-in function + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected built-in function } } @@ -593,7 +593,7 @@ static Bpl.NAryExpr FunctionCall(Bpl.IToken tok, string function, Bpl.Type retur Contract.Requires(tok != null); Contract.Requires(function != null); Contract.Requires(returnType != null); - Contract.Requires(cce.NonNullElements(args)); + Contract.Requires(Cce.NonNullElements(args)); Contract.Ensures(Contract.Result() != null); List aa = new List(); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs index 6a52c81f018..16778ce28cb 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs @@ -39,9 +39,9 @@ void CheckCallTermination(IToken tok, List contextDecreases, List typeMap, ExpressionTranslator etranCurrent, bool oldCaller, BoogieStmtListBuilder builder, bool inferredDecreases, string hint) { Contract.Requires(tok != null); - Contract.Requires(cce.NonNullElements(contextDecreases)); - Contract.Requires(cce.NonNullElements(calleeDecreases)); - Contract.Requires(cce.NonNullDictionaryAndValues(substMap)); + Contract.Requires(Cce.NonNullElements(contextDecreases)); + Contract.Requires(Cce.NonNullElements(calleeDecreases)); + Contract.Requires(Cce.NonNullDictionaryAndValues(substMap)); Contract.Requires(etranCurrent != null); Contract.Requires(builder != null); @@ -105,11 +105,11 @@ void CheckCallTermination(IToken tok, List contextDecreases, List toks, List prevGhostLocals, List dafny0, List dafny1, List ee0, List ee1, BoogieStmtListBuilder builder, string suffixMsg, bool allowNoChange, bool includeLowerBound) { - Contract.Requires(cce.NonNullElements(toks)); - Contract.Requires(cce.NonNullElements(dafny0)); - Contract.Requires(cce.NonNullElements(dafny1)); - Contract.Requires(cce.NonNullElements(ee0)); - Contract.Requires(cce.NonNullElements(ee1)); + Contract.Requires(Cce.NonNullElements(toks)); + Contract.Requires(Cce.NonNullElements(dafny0)); + Contract.Requires(Cce.NonNullElements(dafny1)); + Contract.Requires(Cce.NonNullElements(ee0)); + Contract.Requires(Cce.NonNullElements(ee1)); Contract.Requires(predef != null); Contract.Requires(dafny0.Count == dafny1.Count && dafny0.Count == ee0.Count && ee0.Count == ee1.Count); Contract.Requires(builder == null || suffixMsg != null); @@ -283,7 +283,7 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out b0 = FunctionCall(tok, BuiltinFunction.DtRank, null, e0); b1 = FunctionCall(tok, BuiltinFunction.DtRank, null, e1); } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } eq = Bpl.Expr.Eq(b0, b1); less = Bpl.Expr.Lt(b0, b1); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index d8bfd2eef87..e1c317ade76 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -362,7 +362,7 @@ public Boogie.Expr TrExpr(Expression expr) { } else if (e.Value is BaseTypes.BigDec) { return MaybeLit(Boogie.Expr.Literal((BaseTypes.BigDec)e.Value)); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected literal + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected literal } } case ThisExpr: @@ -405,7 +405,7 @@ public Boogie.Expr TrExpr(Expression expr) { foreach (Expression ee in e.Elements) { var rawElement = TrExpr(ee); isLit = isLit && BoogieGenerator.IsLit(rawElement); - Boogie.Expr ss = BoxIfNecessary(GetToken(displayExpr), rawElement, cce.NonNull(ee.Type)); + Boogie.Expr ss = BoxIfNecessary(GetToken(displayExpr), rawElement, Cce.NonNull(ee.Type)); s = BoogieGenerator.FunctionCall(GetToken(displayExpr), e.Finite ? BuiltinFunction.SetUnionOne : BuiltinFunction.ISetUnionOne, predef.BoxType, s, ss); } if (isLit) { @@ -421,7 +421,7 @@ public Boogie.Expr TrExpr(Expression expr) { foreach (Expression ee in e.Elements) { var rawElement = TrExpr(ee); isLit = isLit && BoogieGenerator.IsLit(rawElement); - Boogie.Expr ss = BoxIfNecessary(GetToken(displayExpr), rawElement, cce.NonNull(ee.Type)); + Boogie.Expr ss = BoxIfNecessary(GetToken(displayExpr), rawElement, Cce.NonNull(ee.Type)); s = BoogieGenerator.FunctionCall(GetToken(displayExpr), BuiltinFunction.MultiSetUnionOne, predef.BoxType, s, ss); } if (isLit) { @@ -456,8 +456,8 @@ public Boogie.Expr TrExpr(Expression expr) { var rawA = TrExpr(p.A); var rawB = TrExpr(p.B); isLit = isLit && BoogieGenerator.IsLit(rawA) && BoogieGenerator.IsLit(rawB); - Boogie.Expr elt = BoxIfNecessary(GetToken(displayExpr), rawA, cce.NonNull(p.A.Type)); - Boogie.Expr elt2 = BoxIfNecessary(GetToken(displayExpr), rawB, cce.NonNull(p.B.Type)); + Boogie.Expr elt = BoxIfNecessary(GetToken(displayExpr), rawA, Cce.NonNull(p.A.Type)); + Boogie.Expr elt2 = BoxIfNecessary(GetToken(displayExpr), rawB, Cce.NonNull(p.B.Type)); s = FunctionCall(GetToken(displayExpr), e.Finite ? "Map#Build" : "IMap#Build", maptype, s, elt, elt2); } if (isLit) { @@ -611,13 +611,13 @@ public Boogie.Expr TrExpr(Expression expr) { Boogie.Expr val = BoxIfNecessary(GetToken(updateExpr), TrExpr(e.Value), mt.Range); return FunctionCall(GetToken(updateExpr), mt.Finite ? "Map#Build" : "IMap#Build", maptype, seq, index, val); } else if (seqType is MultiSetType) { - Type elmtType = cce.NonNull((MultiSetType)seqType).Arg; + Type elmtType = Cce.NonNull((MultiSetType)seqType).Arg; Boogie.Expr index = BoxIfNecessary(GetToken(updateExpr), TrExpr(e.Index), elmtType); Boogie.Expr val = TrExpr(e.Value); return Boogie.Expr.StoreTok(GetToken(updateExpr), seq, index, val); } else { Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } case MultiSelectExpr selectExpr: { @@ -724,7 +724,7 @@ public Boogie.Expr TrExpr(Expression expr) { Type t = dtv.Ctor.Formals[i].Type; var bArg = TrExpr(arg); argsAreLit = argsAreLit && BoogieGenerator.IsLit(bArg); - args.Add(BoogieGenerator.CondApplyBox(GetToken(value), bArg, cce.NonNull(arg.Type), t)); + args.Add(BoogieGenerator.CondApplyBox(GetToken(value), bArg, Cce.NonNull(arg.Type), t)); } Boogie.IdentifierExpr id = new Boogie.IdentifierExpr(GetToken(dtv), dtv.Ctor.FullName, predef.DatatypeType); Boogie.Expr ret = new Boogie.NAryExpr(GetToken(dtv), new Boogie.FunctionCall(id), args); @@ -747,7 +747,7 @@ public Boogie.Expr TrExpr(Expression expr) { } else if (eType is SeqType seqType) { return BoogieGenerator.FunctionCall(GetToken(formingExpr), BuiltinFunction.MultiSetFromSeq, BoogieGenerator.TrType(seqType.Arg), TrExpr(e.E)); } else { - Contract.Assert(false); throw new cce.UnreachableException(); + Contract.Assert(false); throw new Cce.UnreachableException(); } } case OldExpr oldExpr: { @@ -853,7 +853,7 @@ public Boogie.Expr TrExpr(Expression expr) { BoogieGenerator.definiteAssignmentTrackers.TryGetValue(name, out var defass); return defass; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected unary expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected unary expression } } case ConversionExpr conversionExpr: { @@ -1121,7 +1121,7 @@ public Boogie.Expr TrExpr(Expression expr) { case BinaryExpr.ResolvedOpcode.GtChar: bOp = BinaryOperator.Opcode.Gt; break; default: Contract.Assert(false); // unexpected case - throw new cce.UnreachableException(); // to please compiler + throw new Cce.UnreachableException(); // to please compiler } return Boogie.Expr.Binary(GetToken(binaryExpr), bOp, operand0, operand1); } @@ -1158,9 +1158,9 @@ public Boogie.Expr TrExpr(Expression expr) { return BoogieGenerator.FunctionCall(GetToken(binaryExpr), f, null, e0, e1); } case BinaryExpr.ResolvedOpcode.InSet: - Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above + Contract.Assert(false); throw new Cce.UnreachableException(); // this case handled above case BinaryExpr.ResolvedOpcode.NotInSet: - Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above + Contract.Assert(false); throw new Cce.UnreachableException(); // this case handled above case BinaryExpr.ResolvedOpcode.Union: { var setType = binaryExpr.Type.NormalizeToAncestorType().AsSetType; bool finite = setType.Finite; @@ -1190,9 +1190,9 @@ public Boogie.Expr TrExpr(Expression expr) { case BinaryExpr.ResolvedOpcode.MultiSetDisjoint: return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetDisjoint, null, e0, e1); case BinaryExpr.ResolvedOpcode.InMultiSet: - Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above + Contract.Assert(false); throw new Cce.UnreachableException(); // this case handled above case BinaryExpr.ResolvedOpcode.NotInMultiSet: - Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above + Contract.Assert(false); throw new Cce.UnreachableException(); // this case handled above case BinaryExpr.ResolvedOpcode.MultiSetUnion: return BoogieGenerator.FunctionCall(GetToken(binaryExpr), BuiltinFunction.MultiSetUnion, BoogieGenerator.TrType(binaryExpr.Type.NormalizeToAncestorType().AsMultiSetType.Arg), e0, e1); @@ -1256,7 +1256,7 @@ public Boogie.Expr TrExpr(Expression expr) { BoogieGenerator.FunctionCall(GetToken(binaryExpr), e.E1.Type.IsDatatype ? BuiltinFunction.DtRank : BuiltinFunction.BoxRank, null, e1)); default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected binary expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected binary expression } liftLit = liftLit && !keepLits; var ae0 = keepLits ? oe0 : e0; @@ -1289,7 +1289,7 @@ public Boogie.Expr TrExpr(Expression expr) { return Boogie.Expr.Unary(GetToken(ternaryExpr), UnaryOperator.Opcode.Not, r); } default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected ternary expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected ternary expression } } case LetExpr letExpr: @@ -1509,7 +1509,7 @@ public Boogie.Expr TrExpr(Expression expr) { null, allowNoChange, false); return decreasesExpr; default: - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected expression } } @@ -1746,7 +1746,7 @@ public Boogie.Expr TrBoundVariablesRename(List boundVars, List splits Expression ee = e.Args[i]; Type t = e.Function.Ins[i].Type; Expr tr_ee = etran.TrExpr(ee); - Bpl.Expr wh = GetWhereClause(e.tok, tr_ee, cce.NonNull(ee.Type), etran, NOALLOC); + Bpl.Expr wh = GetWhereClause(e.tok, tr_ee, Cce.NonNull(ee.Type), etran, NOALLOC); if (wh != null) { fargs = BplAnd(fargs, wh); } @@ -622,7 +622,7 @@ private Expression GetSubstitutedBody(FunctionCallExpr fexp, Function f) { Formal p = f.Ins[i]; var formalType = p.Type.Subst(fexp.GetTypeArgumentSubstitutions()); Expression arg = fexp.Args[i]; - arg = new BoxingCastExpr(arg, cce.NonNull(arg.Type), formalType); + arg = new BoxingCastExpr(arg, Cce.NonNull(arg.Type), formalType); arg.Type = formalType; // resolve here substMap.Add(p, arg); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index 3e03c893181..3e9c1be89d6 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -525,7 +525,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List (e.Obj, e.Member as Field), SeqSelectExpr e => (e.Seq, null), MultiSelectExpr e => (e.Array, null), - _ => throw new cce.UnreachableException() + _ => throw new Cce.UnreachableException() }; var desc = new PODesc.Modifiable(description, GetContextModifiesFrames(), lhsObj, lhsField); definedness.Add(Assert(lhs.tok, Bpl.Expr.SelectTok(lhs.tok, etran.ModifiesFrame(lhs.tok), obj, F), @@ -2180,10 +2180,10 @@ void ProcessRhss(List lhsBuilder, List locals, ExpressionTranslator etran, Statement stmt) { Contract.Requires(lhsBuilder != null); Contract.Requires(bLhss != null); - Contract.Requires(cce.NonNullElements(lhss)); - Contract.Requires(cce.NonNullElements(rhss)); + Contract.Requires(Cce.NonNullElements(lhss)); + Contract.Requires(Cce.NonNullElements(rhss)); Contract.Requires(builder != null); - Contract.Requires(cce.NonNullElements(locals)); + Contract.Requires(Cce.NonNullElements(locals)); Contract.Requires(etran != null); Contract.Requires(predef != null); @@ -2232,10 +2232,10 @@ void ProcessRhss(List lhsBuilder, List ProcessUpdateAssignRhss(List lhss, List rhss, BoogieStmtListBuilder builder, List locals, ExpressionTranslator etran, Statement stmt) { - Contract.Requires(cce.NonNullElements(lhss)); - Contract.Requires(cce.NonNullElements(rhss)); + Contract.Requires(Cce.NonNullElements(lhss)); + Contract.Requires(Cce.NonNullElements(rhss)); Contract.Requires(builder != null); - Contract.Requires(cce.NonNullElements(locals)); + Contract.Requires(Cce.NonNullElements(locals)); Contract.Requires(etran != null); Contract.Requires(predef != null); Contract.Ensures(Contract.ForAll(Contract.Result>(), i => i != null)); @@ -2336,9 +2336,9 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi out List lhsBuilders, out List bLhss, out Bpl.Expr[] prevObj, out Bpl.Expr[] prevIndex, out string[] prevNames, Expression originalInitialLhs = null) { - Contract.Requires(cce.NonNullElements(lhss)); + Contract.Requires(Cce.NonNullElements(lhss)); Contract.Requires(builder != null); - Contract.Requires(cce.NonNullElements(locals)); + Contract.Requires(Cce.NonNullElements(locals)); Contract.Requires(etran != null); Contract.Requires(predef != null); Contract.Ensures(Contract.ValueAtReturn(out lhsBuilders).Count == lhss.Count); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 7821bad63d2..201caf306cd 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -138,9 +138,9 @@ public void AddReferencedMember(MemberDecl m) { [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullDictionaryAndValues(classes)); - Contract.Invariant(cce.NonNullDictionaryAndValues(fields)); - Contract.Invariant(cce.NonNullDictionaryAndValues(fieldFunctions)); + Contract.Invariant(Cce.NonNullDictionaryAndValues(classes)); + Contract.Invariant(Cce.NonNullDictionaryAndValues(fields)); + Contract.Invariant(Cce.NonNullDictionaryAndValues(fieldFunctions)); Contract.Invariant(codeContext == null || codeContext.EnclosingModule == currentModule); } @@ -652,8 +652,8 @@ PredefinedDecls FindPredefinedDecls(Bpl.Program prog) { Bpl.Program ReadPrelude() { string preludePath = options.DafnyPrelude; if (preludePath == null) { - //using (System.IO.Stream stream = cce.NonNull( System.Reflection.Assembly.GetExecutingAssembly().GetManifestResourceStream("DafnyPrelude.bpl")) // Use this once Spec#/VSIP supports designating a non-.resx project item as an embedded resource - string codebase = cce.NonNull(System.IO.Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location))); + //using (System.IO.Stream stream = Cce.NonNull( System.Reflection.Assembly.GetExecutingAssembly().GetManifestResourceStream("DafnyPrelude.bpl")) // Use this once Spec#/VSIP supports designating a non-.resx project item as an embedded resource + string codebase = Cce.NonNull(System.IO.Path.GetDirectoryName(Cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location))); preludePath = System.IO.Path.Combine(codebase, "DafnyPrelude.bpl"); } @@ -1273,7 +1273,7 @@ void CreateBoundVariables(List formals, out List bvs, out List Contract.Requires(formals != null); Contract.Ensures(Contract.ValueAtReturn(out bvs).Count == Contract.ValueAtReturn(out args).Count); Contract.Ensures(Contract.ValueAtReturn(out bvs) != null); - Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out args))); + Contract.Ensures(Cce.NonNullElements(Contract.ValueAtReturn(out args))); var varNameGen = CurrentIdGenerator.NestedFreshIdGenerator("a#"); bvs = new List(); @@ -1437,10 +1437,10 @@ class Specialization { readonly BoogieGenerator boogieGenerator; [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(Formals)); - Contract.Invariant(cce.NonNullElements(ReplacementExprs)); + Contract.Invariant(Cce.NonNullElements(Formals)); + Contract.Invariant(Cce.NonNullElements(ReplacementExprs)); Contract.Invariant(Formals.Count == ReplacementExprs.Count); - Contract.Invariant(cce.NonNullElements(ReplacementFormals)); + Contract.Invariant(Cce.NonNullElements(ReplacementFormals)); Contract.Invariant(SubstMap != null); } @@ -2042,9 +2042,9 @@ void DefineFrame(IToken/*!*/ tok, Boogie.IdentifierExpr frameIdentifier, List rw Contract.Requires(o != null); // Contract.Requires(f != null); // f == null means approximate Contract.Requires(etran != null); - Contract.Requires(cce.NonNullElements(rw)); - Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap)); + Contract.Requires(Cce.NonNullElements(rw)); + Contract.Requires(substMap == null || Cce.NonNullDictionaryAndValues(substMap)); Contract.Requires(predef != null); Contract.Requires(receiverReplacement == null || substMap != null); Contract.Ensures(Contract.Result() != null); @@ -2202,8 +2202,8 @@ Bpl.Expr InRWClause(IToken tok, Bpl.Expr o, Bpl.Expr f, List rw Contract.Requires(o != null); // Contract.Requires(f != null); // f == null means approximate Contract.Requires(etran != null); - Contract.Requires(cce.NonNullElements(rw)); - Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap)); + Contract.Requires(Cce.NonNullElements(rw)); + Contract.Requires(substMap == null || Cce.NonNullDictionaryAndValues(substMap)); Contract.Requires(predef != null); Contract.Requires(receiverReplacement == null || substMap != null); Contract.Ensures(Contract.Result() != null); @@ -2223,8 +2223,8 @@ Bpl.Expr InRWClause_Aux(IToken tok, Bpl.Expr o, Bpl.Expr boxO, Bpl.Expr f, List< Contract.Requires(boxO != null); // Contract.Requires(f != null); // f == null means approximate Contract.Requires(etran != null); - Contract.Requires(cce.NonNullElements(rw)); - Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap)); + Contract.Requires(Cce.NonNullElements(rw)); + Contract.Requires(substMap == null || Cce.NonNullDictionaryAndValues(substMap)); Contract.Requires(predef != null); Contract.Requires((substMap == null && receiverReplacement == null) || substMap != null); Contract.Ensures(Contract.Result() != null); @@ -2396,7 +2396,7 @@ Bpl.Expr CtorInvocation(MatchCase mc, Type sourceType, ExpressionTranslator etra localTypeAssumptions.Add(TrAssumeCmd(p.tok, wh)); } CheckSubrange(p.tok, new Bpl.IdentifierExpr(p.tok, local), pFormalType, p.Type, new IdentifierExpr(p.Tok, p), localTypeAssumptions); - args.Add(CondApplyBox(mc.tok, new Bpl.IdentifierExpr(p.tok, local), cce.NonNull(p.Type), mc.Ctor.Formals[i].Type)); + args.Add(CondApplyBox(mc.tok, new Bpl.IdentifierExpr(p.tok, local), Cce.NonNull(p.Type), mc.Ctor.Formals[i].Type)); } Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(mc.tok, mc.Ctor.FullName, predef.DatatypeType); return new Bpl.NAryExpr(mc.tok, new Bpl.FunctionCall(id), args); @@ -2559,13 +2559,13 @@ void CloneVariableAsBoundVar(IToken tok, IVariable iv, string prefix, out BoundV // Use trType to translate types in the args list Bpl.Expr ClassTyCon(UserDefinedType cl, List args) { Contract.Requires(cl != null); - Contract.Requires(cce.NonNullElements(args)); + Contract.Requires(Cce.NonNullElements(args)); return ClassTyCon(cl.ResolvedClass, args); } Bpl.Expr ClassTyCon(TopLevelDecl cl, List args) { Contract.Requires(cl != null); - Contract.Requires(cce.NonNullElements(args)); + Contract.Requires(Cce.NonNullElements(args)); return FunctionCall(cl.tok, GetClassTyCon(cl), predef.Ty, args); } @@ -3022,7 +3022,7 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes Contract.Requires(modifiesClause != null); Contract.Requires(etranPre != null); Contract.Requires(etran != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Contract.Ensures(Cce.NonNullElements(Contract.Result>())); var boilerplate = new List(); if (!canAllocate && modifiesClause.Count == 0) { @@ -3062,7 +3062,7 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes Contract.Requires(tok != null); Contract.Requires(etran != null); Contract.Requires(etranPre != null); - Contract.Requires(cce.NonNullElements(frame)); + Contract.Requires(Cce.NonNullElements(frame)); Contract.Requires(predef != null); Contract.Ensures(Contract.Result() != null); @@ -3227,7 +3227,7 @@ Bpl.Type TrType(Type type) { } else if (type is SeqType) { return predef.SeqType; } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -3647,7 +3647,7 @@ Bpl.Expr SetupVariableAsLocal(IVariable v, Dictionary sub var idGen = new FreshIdGenerator(); foreach (Expression e in decreases) { Contract.Assert(e != null); - Bpl.LocalVariable bfVar = new Bpl.LocalVariable(e.tok, new Bpl.TypedIdent(e.tok, idGen.FreshId(varPrefix), TrType(cce.NonNull(e.Type)))); + Bpl.LocalVariable bfVar = new Bpl.LocalVariable(e.tok, new Bpl.TypedIdent(e.tok, idGen.FreshId(varPrefix), TrType(Cce.NonNull(e.Type)))); locals.Add(bfVar); Bpl.IdentifierExpr bf = new Bpl.IdentifierExpr(e.tok, bfVar); oldBfs.Add(bf); @@ -3736,7 +3736,7 @@ Bpl.Expr TypeToTy(Type type) { } else if (type is ParamTypeProxy) { return TrTypeParameter(((ParamTypeProxy)type).orig); } else { - Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type + Contract.Assert(false); throw new Cce.UnreachableException(); // unexpected type } } @@ -4755,7 +4755,7 @@ public static Expression Substitute(Expression expr, IVariable v, Expression e) public static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary/*!*/ substMap, Dictionary typeMap = null, Label oldLabel = null) { Contract.Requires(expr != null); - Contract.Requires(cce.NonNullDictionaryAndValues(substMap)); + Contract.Requires(Cce.NonNullDictionaryAndValues(substMap)); Contract.Ensures(Contract.Result() != null); var s = new Substituter(receiverReplacement, substMap, typeMap ?? new Dictionary(), oldLabel); return s.Substitute(expr); diff --git a/Source/DafnyDriver.Test/DafnyDriver.Test.csproj b/Source/DafnyDriver.Test/DafnyDriver.Test.csproj index 8ff46c1febc..eee74f37037 100644 --- a/Source/DafnyDriver.Test/DafnyDriver.Test.csproj +++ b/Source/DafnyDriver.Test/DafnyDriver.Test.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable enable diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index 11f8d8273ba..5199b242203 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -5,7 +5,7 @@ DafnyDriver false TRACE - net6.0 + net8.0 ..\..\Binaries\ false diff --git a/Source/DafnyDriver/JsonVerificationLogger.cs b/Source/DafnyDriver/JsonVerificationLogger.cs index a2681ca28de..1013e9a5fb8 100644 --- a/Source/DafnyDriver/JsonVerificationLogger.cs +++ b/Source/DafnyDriver/JsonVerificationLogger.cs @@ -133,7 +133,7 @@ public static VcOutcome MergeOutcomes(VcOutcome currentVcOutcome, SolverOutcome return currentVcOutcome; default: Contract.Assert(false); - throw new cce.UnreachableException(); + throw new Cce.UnreachableException(); } } diff --git a/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs b/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs index 260b8a981ce..1394586155b 100644 --- a/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs +++ b/Source/DafnyDriver/Legacy/DafnyBackwardsCompatibleCli.cs @@ -40,7 +40,7 @@ public static Task MainWithWriters(TextWriter outputWriter, TextWriter erro } private static Task ThreadMain(TextWriter outputWriter, TextWriter errorWriter, TextReader inputReader, string[] args) { - Contract.Requires(cce.NonNullElements(args)); + Contract.Requires(Cce.NonNullElements(args)); var legacyResult = TryLegacyArgumentParser(inputReader, outputWriter, errorWriter, args); if (legacyResult == null) { var console = new WritersConsole(inputReader, outputWriter, errorWriter); diff --git a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs index 150a7434a00..d8e45ce4a09 100644 --- a/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs +++ b/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs @@ -240,7 +240,7 @@ public async Task ProcessFilesAsync(IReadOnlyList/*!* ReadOnlyCollection otherFileNames, DafnyOptions options, ProofDependencyManager depManager, bool lookForSnapshots = true, string programId = null) { - Contract.Requires(cce.NonNullElements(dafnyFiles)); + Contract.Requires(Cce.NonNullElements(dafnyFiles)); var dafnyFileNames = DafnyFile.FileNames(dafnyFiles); ExitValue exitValue = ExitValue.SUCCESS; @@ -286,7 +286,7 @@ public async Task ProcessFilesAsync(IReadOnlyList/*!* var boogiePrograms = await DafnyMain.LargeStackFactory.StartNew(() => Translate(engine.Options, dafnyProgram).ToList()); - string baseName = cce.NonNull(Path.GetFileName(dafnyFileNames[^1])); + string baseName = Cce.NonNull(Path.GetFileName(dafnyFileNames[^1])); var (verified, outcome, moduleStats) = await BoogieAsync(dafnyProgram.Reporter, options, baseName, boogiePrograms, programId); diff --git a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj index e25f0c91a99..4005d15710e 100644 --- a/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj +++ b/Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj @@ -1,7 +1,7 @@  - net6.0 + net8.0 false Microsoft.Dafny.LanguageServer.IntegrationTest diff --git a/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs b/Source/DafnyLanguageServer.Test/Performance/LargeFilesTest.cs index 359ab1ee16a..8bf52a75fd5 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; diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj index dc0109c8446..a2128752e35 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.csproj +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.csproj @@ -1,7 +1,7 @@  - net6.0 + net8.0 true enable Microsoft.Dafny.LanguageServer diff --git a/Source/DafnyLanguageServer/Language/CachingParser.cs b/Source/DafnyLanguageServer/Language/CachingParser.cs index 2c161a075f0..1c9987438ab 100644 --- a/Source/DafnyLanguageServer/Language/CachingParser.cs +++ b/Source/DafnyLanguageServer/Language/CachingParser.cs @@ -36,7 +36,7 @@ protected override DfyParseResult ParseFile(DafnyOptions options, Func newReader, uri, cancellationToken); diff --git a/Source/DafnyLanguageServer/Language/CachingResolver.cs b/Source/DafnyLanguageServer/Language/CachingResolver.cs index 1bfc9021266..28a1c3ca7b6 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); diff --git a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj index 8dc6a8806e1..2be0a7b42eb 100644 --- a/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj +++ b/Source/DafnyPipeline.Test/DafnyPipeline.Test.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 false diff --git a/Source/DafnyPipeline/DafnyPipeline.csproj b/Source/DafnyPipeline/DafnyPipeline.csproj index 46e2cea83f4..f591b097fed 100644 --- a/Source/DafnyPipeline/DafnyPipeline.csproj +++ b/Source/DafnyPipeline/DafnyPipeline.csproj @@ -7,7 +7,7 @@ false ..\..\Binaries\ TRACE - net6.0 + net8.0 MIT diff --git a/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj b/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj index f90c85ef0bf..ee3d4cd8477 100644 --- a/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj +++ b/Source/DafnyRuntime.Tests/DafnyRuntime.Tests.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 enable false diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index a37c79c0618..2a7a4063c09 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -5,7 +5,7 @@ DafnyServer false TRACE - net6.0 + net8.0 ..\..\Binaries\ MIT diff --git a/Source/DafnyServer/SuperLegacySymbolTable.cs b/Source/DafnyServer/SuperLegacySymbolTable.cs index 7f5ce9ab86b..82dd6fabd9b 100644 --- a/Source/DafnyServer/SuperLegacySymbolTable.cs +++ b/Source/DafnyServer/SuperLegacySymbolTable.cs @@ -228,8 +228,7 @@ private static void ParseUpdateStatement(Statement statement, List(); - var rightSideDots = rightSide.OfType(); - var allExprDotNames = leftSideDots.Concat(rightSideDots); + var allExprDotNames = leftSideDots; foreach (var exprDotName in allExprDotNames) { if (!(exprDotName.Lhs.Type is UserDefinedType)) { continue; @@ -305,11 +304,9 @@ private static IEnumerable ParseBodyForFieldReferences(IEn var leftSide = updateStmt.Lhss; var rightSide = updateStmt.Rhss; var leftSideDots = leftSide.OfType(); - var rightSideDots = rightSide.OfType(); - var exprDotNames = leftSideDots.Concat(rightSideDots); + var exprDotNames = leftSideDots; var leftSideNameSegments = leftSide.OfType(); - var rightSideNameSegments = rightSide.OfType(); - var nameSegments = leftSideNameSegments.Concat(rightSideNameSegments); + var nameSegments = leftSideNameSegments; 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..e12eab90d72 100644 --- a/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj +++ b/Source/DafnyTestGeneration.Test/DafnyTestGeneration.Test.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 false diff --git a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj index ff8036f7a30..8de8f88fdb7 100644 --- a/Source/DafnyTestGeneration/DafnyTestGeneration.csproj +++ b/Source/DafnyTestGeneration/DafnyTestGeneration.csproj @@ -8,7 +8,7 @@ ..\..\Binaries\ true TRACE - net6.0 + net8.0 enable false MIT diff --git a/Source/IntegrationTests/IntegrationTests.csproj b/Source/IntegrationTests/IntegrationTests.csproj index 5370699a473..2d90bc485ca 100644 --- a/Source/IntegrationTests/IntegrationTests.csproj +++ b/Source/IntegrationTests/IntegrationTests.csproj @@ -1,7 +1,7 @@ - net6.0 + net8.0 true false enable diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj index d8b5e8b41ad..eefc01ebbeb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/RunAllTests/RunAllTests.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 false diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj index 768e4f6f829..58a723cd452 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/DafnyTests/TestAttribute/TestAttribute.csproj @@ -1,7 +1,7 @@  - net6.0 + net8.0 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj index 41f1d5ad4b2..a269962b552 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/manualcompile/ManualCompile.csproj @@ -2,7 +2,7 @@ Exe - net6.0 + net8.0 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/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/examples/Simple_compiler/csharp/SimpleCompiler.csproj b/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler/csharp/SimpleCompiler.csproj index c3a9eccf93e..5afee869737 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,7 +2,7 @@ Exe - net6.0 + net8.0 enable CS3021; CS0162; CS0164 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/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/boogie b/boogie new file mode 160000 index 00000000000..fcd9f83b8d7 --- /dev/null +++ b/boogie @@ -0,0 +1 @@ +Subproject commit fcd9f83b8d715be3c0278777aeedb9f5d0f6a904 diff --git a/dotnet-tools.json b/dotnet-tools.json index c263d70700e..799afea8de8 100644 --- a/dotnet-tools.json +++ b/dotnet-tools.json @@ -3,7 +3,7 @@ "isRoot": true, "tools": { "cocor": { - "version": "2014.12.24", + "version": "2014.12.25", "commands": [ "coco" ]