Add some missing system contracts; fix bad contracts in Application and ...

CodeContracts.sln

@@ -1,7 +1,7 @@
 
 Microsoft Visual Studio Solution File, Format Version 12.00
 # Visual Studio 2013
-VisualStudioVersion = 12.0.30723.0
+VisualStudioVersion = 12.0.31101.0
 MinimumVisualStudioVersion = 10.0.40219.1
 Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "CodeProviders", "CodeProviders", "{76F9B10B-70B6-40FF-B5A7-3562734BF8E4}"
 EndProject
@@ -317,6 +317,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ParseStats", "Microsoft.Res
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "RevisedSimplexMethod", "Microsoft.Research\RevisedSimplexMethod\RevisedSimplexMethod\RevisedSimplexMethod.csproj", "{52B1843A-04C6-48A8-A8F7-C11392C44E7F}"
 EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SystemRequiresVerificationTests", "Microsoft.Research\Contracts\SystemRequiresVerificationTests\SystemRequiresVerificationTests.csproj", "{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}"
+EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
 		Debug|Any CPU = Debug|Any CPU
@@ -2333,6 +2335,30 @@ Global
 		{52B1843A-04C6-48A8-A8F7-C11392C44E7F}.Release|Mixed Platforms.Build.0 = Devlab64|Any CPU
 		{52B1843A-04C6-48A8-A8F7-C11392C44E7F}.Release|Win32.ActiveCfg = Devlab64|Any CPU
 		{52B1843A-04C6-48A8-A8F7-C11392C44E7F}.Release|x86.ActiveCfg = Devlab64|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Debug|Win32.ActiveCfg = Debug|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Debug|x86.ActiveCfg = Debug|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Devlab9|Any CPU.ActiveCfg = Debug|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Devlab9|Any CPU.Build.0 = Debug|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Devlab9|Mixed Platforms.ActiveCfg = Debug|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Devlab9|Mixed Platforms.Build.0 = Debug|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Devlab9|Win32.ActiveCfg = Debug|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Devlab9|x86.ActiveCfg = Debug|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Internal9|Any CPU.ActiveCfg = Release|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Internal9|Any CPU.Build.0 = Release|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Internal9|Mixed Platforms.ActiveCfg = Release|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Internal9|Mixed Platforms.Build.0 = Release|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Internal9|Win32.ActiveCfg = Release|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Internal9|x86.ActiveCfg = Release|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Release|Any CPU.Build.0 = Release|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Release|Win32.ActiveCfg = Release|Any CPU
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC}.Release|x86.ActiveCfg = Release|Any CPU
 	EndGlobalSection
 	GlobalSection(SolutionProperties) = preSolution
 		HideSolutionNode = FALSE
@@ -2434,6 +2460,7 @@ Global
 		{4CDCA734-7AA6-4283-B915-F9EB13A23D7F} = {8C9BFE1D-90BD-4F88-B58E-89FF1DA325B8}
 		{9A6A7CB1-138C-4342-B630-93C04FF48317} = {8C9BFE1D-90BD-4F88-B58E-89FF1DA325B8}
 		{52B1843A-04C6-48A8-A8F7-C11392C44E7F} = {C6F8F507-B843-4D08-8E4B-FF4AF23FC864}
+		{34BEDC68-AC8A-44F9-BF92-01ECAE6A28CC} = {5C718DA9-A4F2-4F73-B095-B2E180033C15}
 	EndGlobalSection
 	GlobalSection(TestCaseManagementSettings) = postSolution
 		CategoryFile = CodeContracts10.vsmdi

Microsoft.Research/Clousot.Cache/Clousot.Cache.csproj

@@ -116,6 +116,7 @@
     <Reference Include="System.ComponentModel.DataAnnotations" />
     <Reference Include="System.Core" />
     <Reference Include="System.Data.Entity" />
+    <Reference Include="System.Data.Linq" />
     <Reference Include="System.Xml.Linq" />
     <Reference Include="System.Data.DataSetExtensions" />
     <Reference Include="Microsoft.CSharp" />

Microsoft.Research/Clousot.Cache/SQLCacheModel.cs

@@ -16,6 +16,9 @@
 
 using System;
 using System.Collections.Generic;
+using System.Data.Common;
+using System.Data.Linq;
+using System.Globalization;
 using System.Linq;
 using System.Text;
 using Microsoft.Research.CodeAnalysis.Caching.Models;
@@ -28,7 +31,7 @@
 using System.Data.Entity.Migrations;
 using System.Data.Entity.Infrastructure;
 // Entityframework v5:
-#if EF5 
+#if EF5
 using System.Data.Objects;
 #else
 // Entity Framework v6
@@ -92,7 +95,7 @@ private void ObjectInvariant()
       Contract.Invariant(cachename != null);
     }
 
-    
+
     private bool isFresh;
     private int nbWaitingChanges = 0;
     const int MaxWaitingChanges = 500;
@@ -173,7 +176,7 @@ public Method MethodByHash(byte[] hash)
       try
       {
         var query = base.Methods.Where(m => m.Hash.Equals(hash));
-        
+
         return query.FirstOrDefault();
       }
       catch (Exception e)
@@ -338,7 +341,8 @@ public bool IsValid
     {
       get
       {
-        try {
+        try
+        {
           return base.Database != null
             && base.Database.Connection != null
             && base.Database.Connection.State != System.Data.ConnectionState.Broken;
@@ -411,7 +415,7 @@ private void FixupPendingChanges()
       RemoveDuplicateAdds<Method>(objContext, method => this.MethodByHash(method.Hash));
     }
 
-    private void RemoveDuplicateAdds<T>(ObjectContext objContext, Func<T,T> getStored) where T:class
+    private void RemoveDuplicateAdds<T>(ObjectContext objContext, Func<T, T> getStored) where T : class
     {
       Contract.Requires(objContext != null);
       Contract.Requires(getStored != null);
@@ -425,7 +429,8 @@ private void RemoveDuplicateAdds<T>(ObjectContext objContext, Func<T,T> getStore
       foreach (var p in pendingAssemblyInfo)
       {
         Contract.Assume(p != null);
-        if (getStored(p.Entity) != null) {
+        if (getStored(p.Entity) != null)
+        {
           objContext.Detach(p.Entity);
         }
       }
@@ -476,7 +481,7 @@ private bool ValidMethodModel(Method methodModel, bool warn = false)
 
     public void AddOrUpdate(Method methodModel)
     {
-      if (!ValidMethodModel(methodModel, warn:true)) return;
+      if (!ValidMethodModel(methodModel, warn: true)) return;
       try
       {
         // don't use Migrations.AddOrUpdate method. It is really slow. Assume we can update (no cache hit)
@@ -510,23 +515,23 @@ public void AddOrUpdate(IdHashTimeToMethod idhash)
 
     public void AddOrUpdate(Method method, AssemblyInfo assemblyInfo)
     {
-        if (!ValidMethodModel(method)) return;
-        try
+      if (!ValidMethodModel(method)) return;
+      try
+      {
+        if (!method.Assemblies.AssumeNotNull()
+          .Where(a => a.AssemblyId == assemblyInfo.AssemblyId).AssumeNotNull()
+          .Any())
         {
-            if (!method.Assemblies.AssumeNotNull()
-              .Where(a => a.AssemblyId == assemblyInfo.AssemblyId).AssumeNotNull()
-              .Any())
-            {
-                method.Assemblies.Add(assemblyInfo);
-            }
+          method.Assemblies.Add(assemblyInfo);
         }
-        catch (Exception e)
+      }
+      catch (Exception e)
+      {
+        if (this.trace)
         {
-            if (this.trace)
-            {
-                Console.WriteLine("[cache] SqlCacheModel: AddOrUpdate method assembly binding failed: {0}", e.Message);
-            }
+          Console.WriteLine("[cache] SqlCacheModel: AddOrUpdate method assembly binding failed: {0}", e.Message);
         }
+      }
     }
 
     public void AddOrUpdate(BaselineMethod baseline)
@@ -550,14 +555,41 @@ public void AddOrUpdate(BaselineMethod baseline)
           Console.WriteLine("[cache] SqlCacheModel: AddOrUpdate baseline binding failed: {0}", e.Message);
         }
       }
-
-    }
 
+    }
 
     public string CacheName
     {
       get { return this.cachename; }
     }
+
+    protected static void DetachDeletedDb(string connection)
+    {
+      // If anyone has manually deleted the cache file, it might be still registered with LocalDB. 
+      // If this is the case, we can't create a new database and the user is stuck unless he knows the tricky internals of LocalDB and how to get rid of the registration.
+      // => If we use LocalDB and the file does not exist, we try to detach it. 
+      try
+      {
+        var connectionString = new DbConnectionStringBuilder { ConnectionString = connection };
+        var fileName = (string)connectionString["AttachDbFileName"];
+        if (File.Exists(fileName)) 
+          return;
+
+        var catalog = (string)connectionString["Initial Catalog"];
+        var dataSource = (string)connectionString["Data Source"];
+
+        using (var master = new DataContext(string.Format(CultureInfo.InvariantCulture, @"Data Source={0};Initial Catalog=master;Integrated Security=True", dataSource)))
+        {
+          master.ExecuteCommand(@"exec sp_detach_db {0}", catalog);
+        }
+      }
+      catch
+      {
+        // Ignore any errors here, could be 
+        // - not using LocalDB at all (any of the connection string parameters did not exist)
+        // - file was never registered (first time used) or already detached.
+      }
+    }
   }
 
   public class SqlCacheModelNoCreate : SQLCacheModel
@@ -567,8 +599,10 @@ static SqlCacheModelNoCreate()
       Database.SetInitializer<SqlCacheModelNoCreate>(null);
     }
 
-    public SqlCacheModelNoCreate(string connection, string cacheName, bool trace) : base(connection, cacheName, trace) {
-      Contract.Requires(cacheName != null);    
+    public SqlCacheModelNoCreate(string connection, string cacheName, bool trace)
+      : base(connection, cacheName, trace)
+    {
+      Contract.Requires(cacheName != null);
     }
   }
 
@@ -583,7 +617,8 @@ protected override void Seed(SqlCacheModelUseExisting context)
       }
     }
 
-    static SqlCacheModelUseExisting() {
+    static SqlCacheModelUseExisting()
+    {
       Database.SetInitializer<SqlCacheModelUseExisting>(new Policy());
     }
 
@@ -614,6 +649,8 @@ public SqlCacheModelClearExisting(string connection, string cachename, bool trac
       : base(connection, cachename, trace)
     {
       Contract.Requires(cachename != null);
+
+      DetachDeletedDb(connection);
     }
   }
 
@@ -637,6 +674,8 @@ public SqlCacheModelDropOnModelChange(string connection, string cachename, bool
       : base(connection, cachename, trace)
     {
       Contract.Requires(cachename != null);
+
+      DetachDeletedDb(connection);
     }
   }
 

Microsoft.Research/Contracts/Microsoft.VisualBasic.Contracts/Microsoft.VisualBasic10.vbproj

@@ -14,7 +14,7 @@
     <AssemblyName>Microsoft.VisualBasic</AssemblyName>
     <FileAlignment>512</FileAlignment>
     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
-    <MyType>Windows</MyType>
+    <MyType>Empty</MyType>
     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
     <TargetFrameworkProfile />
   </PropertyGroup>

Microsoft.Research/Contracts/MsCorlib/MsCorlib.Contracts10.csproj

@@ -328,8 +328,11 @@
     <Compile Include="System.Collections.Concurrent.ConcurrentDictionary.cs" />
     <Compile Include="System.Collections.Generic.IReadOnlyCollection.cs" />
     <Compile Include="System.Collections.Generic.IReadOnlyList.cs" />
+    <Compile Include="System.Collections.ObjectModel.Collection.cs" />
     <Compile Include="System.Diagnostic.Tracing.EventSource.cs" />
     <Compile Include="System.Diagnostic.Tracing.EventWrittenEventArgs.cs" />
+    <Compile Include="System.Globalization.CalendarWeekRule.cs" />
+    <Compile Include="System.Globalization.DateTimeFormatInfo.cs" />
     <Compile Include="System.IO.DirectoryNotFoundException.cs" />
     <Compile Include="System.IO.FileNotFoundException.cs" />
     <Compile Include="System.IO.PathTooLongException.cs" />
@@ -848,6 +851,7 @@ Include="System.Security.Principal.WindowsPrincipal.cs" /> -->
     <Compile Include="System.Security.Cryptography.HashAlgorithm.cs" />
     <Compile Include="System.Security.Cryptography.ICryptoTransform.cs" />
     <Compile Include="System.Security.Cryptography.MD5.cs" />
+    <Compile Include="System.Security.Cryptography.SymmetricAlgorithm.cs" />
     <Compile Include="System.Security.Principal.IIdentity.cs" />
     <Compile Include="System.Security.Principal.IPrincipal.cs" />
     <Compile Include="System.Security.Principal.SecurityIdentifier.cs" />