From 03bee0d5efb4c9ac739523a586924ad393d44a87 Mon Sep 17 00:00:00 2001 From: Yaakov Date: Wed, 3 Feb 2016 13:52:50 +1100 Subject: [PATCH 1/6] Use .NET 4.6 reference assemblies for 4.6.1 Also use .NET 4.6 reference assemblies when building 4.6/4.6.1 with Visual Studio 2013 --- .../MSBuild/v12.0/Microsoft.CodeContracts.targets | 13 ++++++++++++- .../MSBuild/v14.0/Microsoft.CodeContracts.targets | 5 +++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/Microsoft.Research/ManagedContract.Setup/MSBuild/v12.0/Microsoft.CodeContracts.targets b/Microsoft.Research/ManagedContract.Setup/MSBuild/v12.0/Microsoft.CodeContracts.targets index a1c9563c..9c6c7eef 100644 --- a/Microsoft.Research/ManagedContract.Setup/MSBuild/v12.0/Microsoft.CodeContracts.targets +++ b/Microsoft.Research/ManagedContract.Setup/MSBuild/v12.0/Microsoft.CodeContracts.targets @@ -59,7 +59,18 @@ $(CodeContractsInstallDir)Contracts\.NETFramework\v4.5 - + + + + $(CodeContractsInstallDir)Contracts\.NETFramework\v4.6 + + + + + $(CodeContractsInstallDir)Contracts\.NETFramework\v4.6 + + + $(CodeContractsInstallDir)Contracts\v3.5 diff --git a/Microsoft.Research/ManagedContract.Setup/MSBuild/v14.0/Microsoft.CodeContracts.targets b/Microsoft.Research/ManagedContract.Setup/MSBuild/v14.0/Microsoft.CodeContracts.targets index ce4ce6ab..da61f2b3 100644 --- a/Microsoft.Research/ManagedContract.Setup/MSBuild/v14.0/Microsoft.CodeContracts.targets +++ b/Microsoft.Research/ManagedContract.Setup/MSBuild/v14.0/Microsoft.CodeContracts.targets @@ -70,6 +70,11 @@ $(CodeContractsInstallDir)Contracts\.NETFramework\v4.6 + + + $(CodeContractsInstallDir)Contracts\.NETFramework\v4.6 + + $(CodeContractsInstallDir)Contracts\v3.5 From 65828ffe75f8391cd6a1d52add607b00dcd55c96 Mon Sep 17 00:00:00 2001 From: Yaakov Smith Date: Thu, 19 May 2016 14:41:49 +1000 Subject: [PATCH 2/6] Fix whitespace in System.Type.cs --- .../Contracts/MsCorlib/System.Type.cs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Type.cs b/Microsoft.Research/Contracts/MsCorlib/System.Type.cs index 5b2109c2..fe4999e4 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Type.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Type.cs @@ -888,7 +888,7 @@ public virtual MethodInfo[] GetMethods() Contract.Ensures(Contract.Result() != null); Contract.Ensures(Contract.ForAll(Contract.Result(), el => el != null)); - return default( MethodInfo[]); + return default(MethodInfo[]); } [Pure] @@ -896,7 +896,7 @@ public virtual MethodInfo GetMethod(string name) { Contract.Requires(name != null); - return default( MethodInfo); + return default(MethodInfo); } [Pure] @@ -904,7 +904,7 @@ public virtual MethodInfo GetMethod(string name, BindingFlags bindingAttr) { Contract.Requires(name != null); - return default( MethodInfo); + return default(MethodInfo); } [Pure] @@ -913,7 +913,7 @@ public virtual MethodInfo GetMethod(string name, Type[] types) Contract.Requires(name != null); Contract.Requires(types != null); - return default( MethodInfo); + return default(MethodInfo); } //public MethodInfo GetMethod(string name, Type[] types, ParameterModifier[] modifiers) //{ @@ -942,7 +942,7 @@ public virtual ConstructorInfo[] GetConstructors(BindingFlags arg0) { Contract.Ensures(Contract.Result< ConstructorInfo[]>() != null); - return default( ConstructorInfo[]); + return default(ConstructorInfo[]); } [Pure] @@ -951,14 +951,14 @@ public virtual ConstructorInfo[] GetConstructors() Contract.Ensures(Contract.Result< ConstructorInfo[]>() != null); Contract.Ensures(Contract.ForAll(Contract.Result(), el => el != null)); - return default( ConstructorInfo[]); + return default(ConstructorInfo[]); } [Pure] public virtual ConstructorInfo GetConstructor(Type[] types) { - return default( ConstructorInfo); + return default(ConstructorInfo); } #if false From dff095b904174fe4329cd006e2cc9a4660a9c9e5 Mon Sep 17 00:00:00 2001 From: Yaakov Smith Date: Thu, 19 May 2016 14:43:16 +1000 Subject: [PATCH 3/6] Add missing postcondition to System.Type.GetMethods(). Fixes #414. --- Microsoft.Research/Contracts/MsCorlib/System.Type.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Microsoft.Research/Contracts/MsCorlib/System.Type.cs b/Microsoft.Research/Contracts/MsCorlib/System.Type.cs index fe4999e4..74cb325a 100644 --- a/Microsoft.Research/Contracts/MsCorlib/System.Type.cs +++ b/Microsoft.Research/Contracts/MsCorlib/System.Type.cs @@ -870,6 +870,7 @@ public virtual Type[] GetGenericParameterConstraints() { public virtual MethodInfo[] GetMethods(BindingFlags arg0) { Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.ForAll(Contract.Result(), el => el != null)); return default(MethodInfo[]); } From 818cf826f65f82791388b955b75a9c58ebe02ff5 Mon Sep 17 00:00:00 2001 From: Yaakov Smith Date: Thu, 19 May 2016 14:44:27 +1000 Subject: [PATCH 4/6] Remove precondition on Expression.NewArrayInit that is statically unprovable when the compiler generates Expression calls from LINQ. Fixes #424. --- .../System.Core.Contracts/System.Linq.Expressions.Expression.cs | 1 - 1 file changed, 1 deletion(-) diff --git a/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs b/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs index 63568859..f2e4de47 100644 --- a/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs +++ b/Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs @@ -7666,7 +7666,6 @@ public static NewArrayExpression NewArrayInit(Type type, params Expression[] ini { Contract.Requires(type != null); Contract.Requires(initializers != null); - Contract.Requires(initializers.Length >= 1); Contract.Ensures(Contract.Result() != null); return default(NewArrayExpression); } From 76f833b33dc638ae4881c9565556e54d9b8f000b Mon Sep 17 00:00:00 2001 From: Yaakov Smith Date: Thu, 19 May 2016 14:47:23 +1000 Subject: [PATCH 5/6] Remove ContractDeclarativeAssemblyAttribute from static analysis in an attempt to mitigate #423. --- Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.cs | 1 + Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb | 1 + 2 files changed, 2 insertions(+) diff --git a/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.cs b/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.cs index 427e8090..d7d7119b 100644 --- a/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.cs +++ b/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.cs @@ -11,6 +11,7 @@ namespace System.Diagnostics.Contracts { [AttributeUsage(global::System.AttributeTargets.Assembly)] + [ContractVerification(false)] internal sealed class ContractDeclarativeAssemblyAttribute : global::System.Attribute { } diff --git a/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb b/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb index fb02d6b7..91d5cb81 100644 --- a/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb +++ b/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb @@ -7,6 +7,7 @@ ' + NotInheritable Class ContractDeclarativeAssemblyAttribute Inherits Global.System.Attribute End Class From dd1a1d14d1ee809beb8a57255ba2be829bc405e6 Mon Sep 17 00:00:00 2001 From: Yaakov Smith Date: Thu, 19 May 2016 16:22:23 +1000 Subject: [PATCH 6/6] Fix ContractDeclarativeAssemblyAttribute definition in VB --- Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb b/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb index 91d5cb81..25ec8aeb 100644 --- a/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb +++ b/Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb @@ -5,9 +5,9 @@ ' This file is included when building a contract declarative assembly ' in order to mark it as such for recognition by the tools ' - + - + NotInheritable Class ContractDeclarativeAssemblyAttribute Inherits Global.System.Attribute End Class