Update copyright/license headers (#1084)

RustanLeino · web-flow · commit 1f48c750eaf6 · 2021-01-29T15:57:49.000-08:00
* Update copyright/license headers
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
@@ -4,6 +4,8 @@
 // Edited sequence axioms 20 October 2009 by Alex Summers.
 // Modified 2014 by Dan Rosen.
 // Copyright (c) 2008-2014, Microsoft.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 
 const $$Language$Dafny: bool;  // To be recognizable to the ModelViewer as
 axiom $$Language$Dafny;        // coming from a Dafny program.
diff --git a/Binaries/DafnyRuntime.go b/Binaries/DafnyRuntime.go
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny
 
 import (
diff --git a/Binaries/DafnyRuntime.h b/Binaries/DafnyRuntime.h
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 #pragma once
 
 #include <iostream>
diff --git a/Binaries/DafnyRuntime.js b/Binaries/DafnyRuntime.js
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 const BigNumber = require('bignumber.js');
 BigNumber.config({ MODULO_MODE: BigNumber.EUCLID })
 let _dafny = (function() {
diff --git a/README.md b/README.md
@@ -76,10 +76,6 @@ Then run
 
 This will install pre-commit hooks in your .git/hooks directory.
 
-# Code of Conduct
-
-This project has adopted the [Microsoft Open Source Code of Conduct](https://opensource.microsoft.com/codeofconduct/). For more information see the [Code of Conduct FAQ](https://opensource.microsoft.com/codeofconduct/faq/) or contact [opencode@microsoft.com](mailto:opencode@microsoft.com) with any additional questions or comments.
-
 # License
 
 Dafny itself is licensed under the MIT license. (See LICENSE.txt in the root directory for details.) The subdirectory `third_party` contains third party material; see NOTICES.txt for more details.
diff --git a/Source/Dafny/BigIntegerParser.cs b/Source/Dafny/BigIntegerParser.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 using System;
 using System.Numerics;
 using System.Globalization;
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 using System;
 using System.Collections.Generic;
 using System.Numerics;
diff --git a/Source/Dafny/Compiler-Csharp.cs b/Source/Dafny/Compiler-Csharp.cs
@@ -1,6 +1,8 @@
 //-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
 using System;
diff --git a/Source/Dafny/Compiler-cpp.cs b/Source/Dafny/Compiler-cpp.cs
@@ -1,8 +1,10 @@
 //-----------------------------------------------------------------------------
 //
-// Copyright (C) Amazon.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
+
 using System;
 using System.CodeDom;
 using System.Collections.Generic;
diff --git a/Source/Dafny/Compiler-go.cs b/Source/Dafny/Compiler-go.cs
@@ -1,6 +1,7 @@
 //-----------------------------------------------------------------------------
 //
-// Copyright (C) Amazon.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
 using System;
diff --git a/Source/Dafny/Compiler-java.cs b/Source/Dafny/Compiler-java.cs
@@ -1,8 +1,10 @@
 //-----------------------------------------------------------------------------
 //
-// Copyright (C) Amazon.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
+
 using System;
 using System.Collections.Generic;
 using System.Linq;
diff --git a/Source/Dafny/Compiler-js.cs b/Source/Dafny/Compiler-js.cs
@@ -1,8 +1,10 @@
 //-----------------------------------------------------------------------------
 //
-// Copyright (C) Amazon.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
+
 using System;
 using System.Collections.Generic;
 using System.Linq;
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
@@ -1,6 +1,8 @@
 //-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
 using System;
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
@@ -1,6 +1,8 @@
 /*-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------*/
 /*---------------------------------------------------------------------------
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
@@ -2,6 +2,8 @@
 //-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
 using System;
diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs
@@ -1,6 +1,8 @@
 //-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
 using System;
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 using System;
 using System.Collections.Generic;
 using System.Linq;
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
@@ -1,8 +1,11 @@
 //-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
+
 using System;
 using System.IO;
 using System.Collections.Generic;
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
@@ -1,6 +1,8 @@
 //-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
 // This file contains the transformations that are applied to a module that is
diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 using Microsoft.Boogie;
 using System;
 using System.Collections.Generic;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
@@ -2,6 +2,8 @@
 //-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
 using System;
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
@@ -1,6 +1,8 @@
 ﻿//-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
 using System;
@@ -12234,7 +12236,7 @@ void TrCallStmt(CallStmt s, BoogieStmtListBuilder builder, List<Variable> locals
         for (int i = 0; i < s.Lhs.Count; i++) {
           var lhs = s.Lhs[i];
           lhsTypes.Add(lhs.Type);
-          builder.Add(new CommentCmd("TrCallStmt: Adding lhs " + lhs + " with type " + lhs.Type));
+          builder.Add(new CommentCmd("TrCallStmt: Adding lhs with type " + lhs.Type));
           if (bLhss[i] == null) {  // (in the current implementation, the second parameter "true" to ProcessLhss implies that all bLhss[*] will be null)
             // create temporary local and assign it to bLhss[i]
             string nm = CurrentIdGenerator.FreshId("$rhs##");
diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 using Microsoft.Boogie;
 using System;
 using System.Collections.Generic;
diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 #define QUANTIFIER_WARNINGS
 
 using System;
diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 using System;
 using System.Collections.Generic;
 using System.Linq;
diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 #define THROW_UNSUPPORTED_COMPARISONS
 
 using Microsoft.Dafny;
diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 #define DEBUG_AUTO_TRIGGERS
 
 using System;
diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 using System;
 using System.Collections.Generic;
 using System.Linq;
diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 using System;
 using System.Collections.Generic;
 using System.Linq;
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
@@ -1,6 +1,8 @@
 //-----------------------------------------------------------------------------
 //
 // Copyright (C) Microsoft Corporation.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
 //
 //-----------------------------------------------------------------------------
 //---------------------------------------------------------------------------------------------
diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 #if ISDAFNYRUNTIMELIB
 using System; // for Func
 using System.Numerics;
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Array.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Array.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 import java.util.List;
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/BigOrdinal.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/BigOrdinal.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 import java.math.BigInteger;
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/BigRational.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/BigRational.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 import java.math.BigInteger;
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnyEuclidean.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnyEuclidean.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 import java.math.BigInteger;
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnyHaltException.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnyHaltException.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 public class DafnyHaltException extends RuntimeException {
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnyMap.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnyMap.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 import java.util.*;
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnyMultiset.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnyMultiset.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 import java.math.BigInteger;
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnySequence.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnySequence.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 import java.math.BigInteger;
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnySet.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnySet.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 import java.util.*;
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 import java.lang.reflect.InvocationTargetException;
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Tuple2.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Tuple2.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 @SuppressWarnings({"unchecked", "deprecation"})
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Tuple3.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Tuple3.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 @SuppressWarnings({"unchecked", "deprecation"})
diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/TypeDescriptor.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/TypeDescriptor.java
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 package dafny;
 
 import java.lang.reflect.InvocationTargetException;
diff --git a/Source/DafnyServer/CounterExampleProvider.cs b/Source/DafnyServer/CounterExampleProvider.cs
@@ -1,4 +1,7 @@
-﻿using System;
+﻿// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
+using System;
 using System.Collections.Generic;
 using System.IO;
 using System.Reflection;
diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 using System;
 using System.Collections.Generic;
 using System.IO;
diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs
@@ -1,3 +1,6 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
 using System;
 using System.IO;
 using System.Text;
diff --git a/Source/DafnyServer/SymbolTable.cs b/Source/DafnyServer/SymbolTable.cs
diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs
diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs
diff --git a/Source/DafnyServer/VersionCheck.cs b/Source/DafnyServer/VersionCheck.cs
diff --git a/Source/DafnyServer/boogie/BaseProvider.cs b/Source/DafnyServer/boogie/BaseProvider.cs
diff --git a/Source/DafnyServer/boogie/DafnyProvider.cs b/Source/DafnyServer/boogie/DafnyProvider.cs
diff --git a/Source/DafnyServer/boogie/DataModel.cs b/Source/DafnyServer/boogie/DataModel.cs
diff --git a/Source/DafnyServer/boogie/Namer.cs b/Source/DafnyServer/boogie/Namer.cs
diff --git a/Source/DafnyServer/boogie/VccProvider.cs b/Source/DafnyServer/boogie/VccProvider.cs
