Skip to content
This repository has been archived by the owner on Jul 15, 2023. It is now read-only.

Fixes for various issues #426

Merged
merged 7 commits into from
May 24, 2016
Merged

Fixes for various issues #426

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
03bee0d
Use .NET 4.6 reference assemblies for 4.6.1
yaakov-h Feb 3, 2016
8dc8b66
Merge remote-tracking branch 'yaakov/pr/fix-framework-targetting' int…
yaakov-h May 4, 2016
65828ff
Fix whitespace in System.Type.cs
yaakov-h May 19, 2016
dff095b
Add missing postcondition to System.Type.GetMethods(). Fixes #414.
yaakov-h May 19, 2016
818cf82
Remove precondition on Expression.NewArrayInit that is statically unp…
yaakov-h May 19, 2016
76f833b
Remove ContractDeclarativeAssemblyAttribute from static analysis in a…
yaakov-h May 19, 2016
dd1a1d1
Fix ContractDeclarativeAssemblyAttribute definition in VB
yaakov-h May 19, 2016
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@
namespace System.Diagnostics.Contracts
{
[AttributeUsage(global::System.AttributeTargets.Assembly)]
[ContractVerification(false)]
internal sealed class ContractDeclarativeAssemblyAttribute : global::System.Attribute
{
}
Expand Down
3 changes: 2 additions & 1 deletion Foxtrot/Contracts/ContractDeclarativeAssemblyAttribute.vb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,9 @@
' This file is included when building a contract declarative assembly
' in order to mark it as such for recognition by the tools
'
<Assembly: ContractDeclarativeAssemblyAttribute()>
<Assembly: ContractDeclarativeAssemblyAttribute()>

<System.Diagnostics.Contracts.ContractVerification(False)>
NotInheritable Class ContractDeclarativeAssemblyAttribute
Inherits Global.System.Attribute
End Class
Expand Down
15 changes: 8 additions & 7 deletions Microsoft.Research/Contracts/MsCorlib/System.Type.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -870,6 +870,7 @@ public virtual Type[] GetGenericParameterConstraints() {
public virtual MethodInfo[] GetMethods(BindingFlags arg0)
{
Contract.Ensures(Contract.Result<MethodInfo[]>() != null);
Contract.Ensures(Contract.ForAll(Contract.Result<MethodInfo[]>(), el => el != null));

return default(MethodInfo[]);
}
Expand All @@ -888,23 +889,23 @@ public virtual MethodInfo[] GetMethods()
Contract.Ensures(Contract.Result<MethodInfo[]>() != null);
Contract.Ensures(Contract.ForAll(Contract.Result<MethodInfo[]>(), el => el != null));

return default( MethodInfo[]);
return default(MethodInfo[]);
}

[Pure]
public virtual MethodInfo GetMethod(string name)
{
Contract.Requires(name != null);

return default( MethodInfo);
return default(MethodInfo);
}

[Pure]
public virtual MethodInfo GetMethod(string name, BindingFlags bindingAttr)
{
Contract.Requires(name != null);

return default( MethodInfo);
return default(MethodInfo);
}

[Pure]
Expand All @@ -913,7 +914,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)
//{
Expand Down Expand Up @@ -942,7 +943,7 @@ public virtual ConstructorInfo[] GetConstructors(BindingFlags arg0)
{
Contract.Ensures(Contract.Result< ConstructorInfo[]>() != null);

return default( ConstructorInfo[]);
return default(ConstructorInfo[]);
}

[Pure]
Expand All @@ -951,14 +952,14 @@ public virtual ConstructorInfo[] GetConstructors()
Contract.Ensures(Contract.Result< ConstructorInfo[]>() != null);
Contract.Ensures(Contract.ForAll(Contract.Result<ConstructorInfo[]>(), el => el != null));

return default( ConstructorInfo[]);
return default(ConstructorInfo[]);
}

[Pure]
public virtual ConstructorInfo GetConstructor(Type[] types)
{

return default( ConstructorInfo);
return default(ConstructorInfo);
}

#if false
Expand Down
1 change: 0 additions & 1 deletion Microsoft.Research/Contracts/System.Core.Contracts/System.Linq.Expressions.Expression.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<NewArrayExpression>() != null);
return default(NewArrayExpression);
}
Expand Down
13 changes: 12 additions & 1 deletion Microsoft.Research/ManagedContract.Setup/MSBuild/v12.0/Microsoft.CodeContracts.targets
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,18 @@
<PropertyGroup>
<CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\.NETFramework\v4.5</CodeContractsReferenceAssemblyLibPath>
</PropertyGroup>
</When> <Otherwise>
</When>
<When Condition="'$(TargetFrameworkVersion)' == 'v4.6'">
<PropertyGroup>
<CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\.NETFramework\v4.6</CodeContractsReferenceAssemblyLibPath>
</PropertyGroup>
</When>
<When Condition="'$(TargetFrameworkVersion)' == 'v4.6.1'">
<PropertyGroup>
<CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\.NETFramework\v4.6</CodeContractsReferenceAssemblyLibPath>
</PropertyGroup>
</When>
<Otherwise>
<PropertyGroup>
<CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\v3.5</CodeContractsReferenceAssemblyLibPath>
</PropertyGroup>
Expand Down
5 changes: 5 additions & 0 deletions Microsoft.Research/ManagedContract.Setup/MSBuild/v14.0/Microsoft.CodeContracts.targets
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,11 @@
<CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\.NETFramework\v4.6</CodeContractsReferenceAssemblyLibPath>
</PropertyGroup>
</When>
<When Condition="'$(TargetFrameworkVersion)' == 'v4.6.1'">
<PropertyGroup>
<CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\.NETFramework\v4.6</CodeContractsReferenceAssemblyLibPath>
</PropertyGroup>
</When>
<Otherwise>
<PropertyGroup>
<CodeContractsReferenceAssemblyLibPath>$(CodeContractsInstallDir)Contracts\v3.5</CodeContractsReferenceAssemblyLibPath>
Expand Down