Merge branch 'master' of https://github.com/dafny-lang/dafny into run…

…time-coverage-report

.github/workflows/msbuild.yml

@@ -34,6 +34,9 @@ jobs:
  - name: Restore tools
  working-directory: dafny
  run: dotnet tool restore
+ - name: Check whitespace and style
+ working-directory: dafny
+ run: dotnet format whitespace Source/Dafny.sln --verify-no-changes --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
  - name: Get Boogie Version
  run: |
  sudo apt-get update
@@ -51,9 +54,6 @@ jobs:
  - name: Build Dafny with local Boogie
  working-directory: dafny
  run: dotnet build Source/Dafny.sln
- - name: Check whitespace and style
- working-directory: dafny
- run: dotnet tool run dotnet-format -w -s error --check Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs --exclude DafnyRuntime/DafnyRuntimeSystemModule.cs
  - name: Create NuGet package (just to make sure it works)
  run: dotnet pack --no-build dafny/Source/Dafny.sln
  - name: Check uniformity of integration tests that exercise backends

.pre-commit-config.yaml

@@ -4,5 +4,5 @@ repos:
  - id: dotnet-format
  name: dotnet-format
  language: system
- entry: dotnet tool run dotnet-format --folder -w --include
+ entry: dotnet format whitespace Source/Dafny.sln --include
  types_or: ["c#"]

Makefile

@@ -62,7 +62,7 @@ z3-ubuntu:
  chmod +x ${DIR}/Binaries/z3/bin/z3-*
 
 format:
- dotnet tool run dotnet-format -w -s error Source/Dafny.sln --exclude DafnyCore/Scanner.cs --exclude DafnyCore/Parser.cs --exclude DafnyCore/GeneratedFromDafny.cs
+ dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
 
 clean:
  (cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)

Source/DafnyCore.Test/DafnyProjectTest.cs

@@ -1,6 +1,6 @@
 using Microsoft.Dafny;
 
-namespace DafnyCore.Test; 
+namespace DafnyCore.Test;
 
 public class DafnyProjectTest {
  [Fact]

Source/DafnyCore/AST/Members/Function.cs

@@ -28,6 +28,8 @@ public class Function : MemberDecl, TypeParameter.ParentType, ICallable, ICanFor
  k = WhatKind;
  }
 
+ // If this function is opaque due to the opaque keyword, include it.
+ k = (IsOpaque && !Attributes.Contains(Attributes, "opaque")) ? "opaque " + k : k;
  return HasStaticKeyword ? "static " + k : k;
  }
 

Source/DafnyCore/AST/Members/ICanAutoReveal.cs

@@ -1,4 +1,4 @@
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public interface ICanAutoRevealDependencies {
  public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, DafnyOptions Options, ErrorReporter Reporter);

Source/DafnyCore/Compilers/Dafny/WrapException.cs

@@ -1,4 +1,4 @@
-namespace Microsoft.Dafny.Compilers; 
+namespace Microsoft.Dafny.Compilers;
 
 public class WrapException {
 

Source/DafnyCore/Compilers/Library/LibraryBackend.cs

@@ -6,7 +6,7 @@
 using System.Linq;
 using DafnyCore;
 
-namespace Microsoft.Dafny.Compilers; 
+namespace Microsoft.Dafny.Compilers;
 
 public class LibraryBackend : ExecutableBackend {
  public LibraryBackend(DafnyOptions options) : base(options) {

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -5741,21 +5741,18 @@ private class ArrayLvalueImpl : ILvalue {
  IToken tok, ConcreteSyntaxTree wr, bool isReturning = false, bool elseReturnValue = false,
  bool isSubfiltering = false) {
  if (!boundVarType.Equals(collectionElementType, true) &&
- boundVarType.NormalizeExpand(true) is UserDefinedType
- {
+ boundVarType.NormalizeExpand(true) is UserDefinedType {
  TypeArgs: var typeArgs,
  ResolvedClass:
- SubsetTypeDecl
- {
+ SubsetTypeDecl {
  TypeArgs: var typeParametersArgs,
  Var: var variable,
  Constraint: var constraint
  }
  }) {
- if (variable.Type.NormalizeExpandKeepConstraints() is UserDefinedType
- {
- ResolvedClass: SubsetTypeDecl
- } normalizedVariableType) {
+ if (variable.Type.NormalizeExpandKeepConstraints() is UserDefinedType {
+ ResolvedClass: SubsetTypeDecl
+ } normalizedVariableType) {
  wr = MaybeInjectSubsetConstraint(boundVar, normalizedVariableType, collectionElementType,
  inLetExprBody, tok, wr, isReturning, elseReturnValue, true);
  }

Source/DafnyCore/CoverageReport/CoverageReport.cs

@@ -5,7 +5,7 @@
 using System.Linq;
 using System.Threading;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public class CoverageReport {
 

Source/DafnyCore/CoverageReport/CoverageSpan.cs

@@ -2,7 +2,7 @@
 using System;
 using System.Diagnostics.Contracts;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public class CoverageSpan : IComparable<CoverageSpan> {
 

Source/DafnyCore/DafnyGeneratedFromDafny.sh

@@ -28,4 +28,4 @@ with open ('$output.cs', 'r' ) as f:
 with open('$output.cs', 'w') as w:
  w.write(content_new)
 "
-dotnet tool run dotnet-format -w --include $output.cs 
+dotnet format whitespace --include $output.cs 

Source/DafnyCore/DooFile.cs

@@ -9,7 +9,7 @@
 using Microsoft.Dafny;
 using Tomlyn;
 
-namespace DafnyCore; 
+namespace DafnyCore;
 
 // Model class for the .doo file format for Dafny libraries.
 // Contains the validation logic for safely consuming libraries as well.

Source/DafnyCore/Generic/TomlUtil.cs

@@ -4,7 +4,7 @@
 using System.Linq;
 using Tomlyn.Model;
 
-namespace DafnyCore.Generic; 
+namespace DafnyCore.Generic;
 
 public static class TomlUtil {
 

Source/DafnyCore/Options/DafnyProject.cs

@@ -16,7 +16,7 @@
 using Tomlyn;
 using Tomlyn.Model;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public class DafnyProject : IEquatable<DafnyProject> {
  public const string FileName = "dfyconfig.toml";

Source/DafnyCore/Plugins/CompilerInstrumenter.cs

@@ -1,6 +1,6 @@
 using Microsoft.Dafny.Compilers;
 
-namespace Microsoft.Dafny.Plugins; 
+namespace Microsoft.Dafny.Plugins;
 
 /// <summary>
 /// A hook for plugins to customize some of the code generation of other IExecutableBackends.

Source/DafnyCore/Plugins/ErrorReportingBase.cs

@@ -1,6 +1,6 @@
 using System.Diagnostics.Contracts;
 
-namespace Microsoft.Dafny.Plugins; 
+namespace Microsoft.Dafny.Plugins;
 
 /// <summary>
 /// Abstract base class for plugin interfaces that may report errors.

Source/DafnyCore/Resolver/FuelAdjustment.cs

@@ -2,7 +2,7 @@
 using System.Diagnostics.Contracts;
 using System.Numerics;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public static class FuelAdjustment {
 

Source/DafnyCore/Resolver/SubsetConstraintGhostChecker.cs

@@ -85,8 +85,7 @@ private class FirstErrorCollector : ErrorReporter {
 
  if (e is ForallExpr || e is ExistsExpr || e is SetComprehension || e is MapComprehension) {
  foreach (var boundVar in e.BoundVars) {
- if (boundVar.Type.AsSubsetType is
- {
+ if (boundVar.Type.AsSubsetType is {
  Constraint: var constraint,
  ConstraintIsCompilable: false and var constraintIsCompilable
  } and var subsetTypeDecl

Source/DafnyCore/Rewriters/RewriterCollection.cs

@@ -1,6 +1,6 @@
 using System.Collections.Generic;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public static class RewriterCollection {
 

Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs

@@ -22,7 +22,7 @@
 using PODesc = Microsoft.Dafny.ProofObligationDescription;
 using static Microsoft.Dafny.GenericErrors;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public partial class BoogieGenerator {
 

Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs

@@ -22,7 +22,7 @@
 using PODesc = Microsoft.Dafny.ProofObligationDescription;
 using static Microsoft.Dafny.GenericErrors;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public partial class BoogieGenerator {
 

Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs

@@ -9,7 +9,7 @@
 using PODesc = Microsoft.Dafny.ProofObligationDescription;
 using static Microsoft.Dafny.GenericErrors;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public partial class BoogieGenerator {
 

Source/DafnyCore/Verifier/BoogieGenerator.Types.cs

@@ -22,7 +22,7 @@
 using PODesc = Microsoft.Dafny.ProofObligationDescription;
 using static Microsoft.Dafny.GenericErrors;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public partial class BoogieGenerator {
 

Source/DafnyCore/Verifier/BoogieGenerator.cs

@@ -3994,8 +3994,7 @@ public ForceCheckToken(IToken tok)
  "it may have read effects");
  } else {
  desc = new PODesc.SubrangeCheck(errorMessagePrefix, sourceType.ToString(), targetType.ToString(),
- targetType.NormalizeExpandKeepConstraints() is UserDefinedType
- {
+ targetType.NormalizeExpandKeepConstraints() is UserDefinedType {
  ResolvedClass: SubsetTypeDecl or NewtypeDecl { Var: { } }
  },
  false, null);

Source/DafnyDriver/Commands/CoverageReportCommand.cs

@@ -9,7 +9,7 @@
 using System.Threading.Tasks;
 using DafnyCore;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 static class CoverageReportCommand {
 

Source/DafnyDriver/CoverageReporter.cs

@@ -7,7 +7,7 @@
 using DafnyCore.Verifier;
 using Microsoft.Boogie;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public class CoverageReporter {
 

Source/DafnyLanguageServer.Test/Diagnostics/VerificationDiagnostics.cs

@@ -6,7 +6,7 @@
 using Xunit;
 using Xunit.Abstractions;
 
-namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization; 
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization;
 
 public class VerificationDiagnostics : ClientBasedLanguageServerTest {
 

Source/DafnyLanguageServer.Test/MultipleFilesNoProjectTest.cs

@@ -6,7 +6,7 @@
 using Xunit;
 using Xunit.Abstractions;
 
-namespace Microsoft.Dafny.LanguageServer.IntegrationTest; 
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest;
 
 public class MultipleFilesNoProjectTest : ClientBasedLanguageServerTest {
  [Fact]

Source/DafnyLanguageServer.Test/Performance/ThreadUsageTest.cs

@@ -8,7 +8,7 @@
 using Xunit.Abstractions;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
-namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Performance; 
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Performance;
 
 [Collection("Sequential Collection")] // Seems to deadlock when run in parallel
 public class ThreadUsageTest : ClientBasedLanguageServerTest {

Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs

@@ -10,7 +10,7 @@
 using Xunit.Abstractions;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
-namespace Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles; 
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles;
 
 public class CompetingProjectFilesTest : ClientBasedLanguageServerTest {
 

Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs

@@ -11,7 +11,7 @@
 using Xunit.Abstractions;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
-namespace Microsoft.Dafny.LanguageServer.IntegrationTest; 
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest;
 
 public class ProjectFilesTest : ClientBasedLanguageServerTest {
 

Source/DafnyLanguageServer.Test/Refinement/RefinementTests.cs

@@ -6,7 +6,7 @@
 using Xunit;
 using Xunit.Abstractions;
 
-namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Refinement; 
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Refinement;
 
 public class RefinementTests : ClientBasedLanguageServerTest {
  [Fact]

Source/DafnyLanguageServer.Test/Synchronization/CachingTest.cs

@@ -15,7 +15,7 @@
 using Xunit.Abstractions;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
-namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization; 
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization;
 
 public class CachingTest : ClientBasedLanguageServerTest {
  private InMemorySink sink;

Source/DafnyLanguageServer.Test/Synchronization/ProjectManagerDatabaseTest.cs

@@ -9,7 +9,7 @@
 using Xunit;
 using Xunit.Abstractions;
 
-namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization; 
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Synchronization;
 
 [Collection("Sequential Collection")]
 public class ProjectManagerDatabaseTest : ClientBasedLanguageServerTest {

Source/DafnyLanguageServer.Test/Unit/ByteArrayEqualityTest.cs

@@ -2,7 +2,7 @@
 using Microsoft.Dafny.LanguageServer.Language;
 using Xunit;
 
-namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit; 
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit;
 
 public class ByteArrayEqualityTest {
  [Fact]

Source/DafnyLanguageServer.Test/Unit/CompilationManagerTest.cs

@@ -7,7 +7,7 @@
 using Moq;
 using Xunit;
 
-namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit; 
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit;
 
 public class CompilationManagerTest {
  [Fact]

Source/DafnyLanguageServer.Test/Unit/TextReaderFromCharArraysTest.cs

@@ -2,7 +2,7 @@
 using Microsoft.Dafny.LanguageServer.Language;
 using Xunit;
 
-namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit; 
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Unit;
 
 public class TextReaderFromCharArraysTest {
 

Source/DafnyLanguageServer.Test/Util/StringifyTest.cs

@@ -2,7 +2,7 @@
 using System.Collections.Generic;
 using Xunit;
 
-namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Util; 
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
 
 public class StringifyTest {
 

Source/DafnyLanguageServer/Caching/PruneIfNotUsedSinceLastPruneCache.cs

@@ -5,7 +5,7 @@
 using System.Linq;
 using Microsoft.Dafny.LanguageServer.Workspace;
 
-namespace Microsoft.Dafny; 
+namespace Microsoft.Dafny;
 
 public class PruneIfNotUsedSinceLastPruneCache<TKey, TValue>
  where TValue : class

Source/DafnyLanguageServer/Util/PositionExtensions.cs

@@ -1,7 +1,7 @@
 using Microsoft.Dafny.LanguageServer.Language;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
-namespace Microsoft.Dafny.LanguageServer.Util; 
+namespace Microsoft.Dafny.LanguageServer.Util;
 
 public static class PositionExtensions {
  public static DafnyPosition ToDafnyPosition(this IToken token) {

Source/DafnyStandardLibraries/README.md

@@ -42,6 +42,7 @@ The sections below describe how to use each library:
 - [DafnyStdLibs.Wrappers](src/DafnyStdLibs/Wrappers) -- simple datatypes to support common patterns, such as optional values or the result of operations that can fail
 - [DafnyStdLibs.Relations](src/DafnyStdLibs/Relations) -- properties of relations
 - [DafnyStdLibs.Functions](src/DafnyStdLibs/Functions) -- properties of functions
+- [DafnyStdLibs.Base64](src/DafnyStdLibs/Base64) -- base-64 encoding and decoding
 
 We are in the process of importing many more libraries,
 in particular from the existing [`dafny-lang/libraries`](https://github.com/dafny-lang/libraries) GitHub repository.