string.IsNullOrWhiteSpace() not considered Pure by Requires() or Invariant() when running on .NET 4.6.1

[Desarc]

There seems to be an issue with string.IsNullOrWhiteSpace() when running Code Contracts on .NET 4.6.1. Given the following sample code:

public void StringTests()
{
     RequiresNotNullOrWhiteSpace("test");
}

public void RequiresNotNullOrWhiteSpace(string s)
{
      Contract.Requires(!string.IsNullOrWhiteSpace(s));
}

The static checker gives the following warning on the Requires() -call:

Warning CC1036  Detected call to method 'System.String.IsNullOrWhiteSpace(System.String)' 
without [Pure] in contracts of method '....TestNullOrWhiteSpace(System.String)'.

... and additionally the following warning on the RequiresNotNullOrWhiteSpace("test") -call:

CodeContracts: requires unproven: !string.IsNullOrWhiteSpace(s). Are you making some assumption 
on IsNullOrWhiteSpace that the static checker is unaware of?

I compiled exactly the same code on .NET 4.0, 4.5.1 and 4.6 without getting these warnings.

From the user documentation:

 Code Contract tools currently assume the following things are pure:
• Any method whose fully qualified name begins with System.Diagnostics.Contracts.Contract, 
System.String, System.IO.Path, or System.Type.

Additionally, the IsNullOrWhiteSpace() method is actually marked as [Pure] in .NET 4.6.1

The same problem applies to Invariant(). Given the following code, the same warnings are displayed:

private string testString = "test";

[ContractInvariantMethod]
private void TestInvariant()
{
     Contract.Invariant(!string.IsNullOrWhiteSpace(testString));
}

[yaakov-h]

I suspect this is because of the conditional here combined with the fact that we fall back to .NET 3.5 contract reference assemblies if we don't have a matching condition in the targets file. #359 should fix this.

[fourpastmidnight]

I can verify that #359 does fix this issue. I modified my Microsoft.CodeContracts.targets files and the issue went away. Though, I did need to use the v4.5 assemblies when the project framework version is set to 4.6 and above. But hopefully, the PR associated with #359 takes care of all these framework version issues.

[joshjeppson]

There also seems to be an issue where CodeContracts doesn't realize that IsNullOrWhiteSpace is a stronger assertion than IsNullOrEmpty. Does #359 also fix that issue? Or just the missing [Pure] attribute?

Generates warning:

Contract.Requires(!String.IsNullOrWhiteSpace(path));
var contents = File.ReadAllText(path);

Works:

Contract.Requires(!String.IsNullOrEmpty(path));
var contents = File.ReadAllText(path);

[yaakov-h]

I believe #359 will fix that as well, but only if your project is targeting .NET 4.6 (in VS2013) or 4.6.1 (in VS2013 or VS2015). Anything else is a separate issue.