diff --git a/.nuget/NuGet.targets b/.nuget/NuGet.targets
deleted file mode 100644
index f9438127..00000000
--- a/.nuget/NuGet.targets
+++ /dev/null
@@ -1,144 +0,0 @@
-
-
-
- $(MSBuildProjectDirectory)\..\
-
-
- false
-
-
- false
-
-
- true
-
-
- false
-
-
-
-
-
-
-
-
-
-
- $([System.IO.Path]::Combine($(SolutionDir), ".nuget"))
-
-
-
-
- $(SolutionDir).nuget
-
-
-
- $(MSBuildProjectDirectory)\packages.$(MSBuildProjectName.Replace(' ', '_')).config
- $(MSBuildProjectDirectory)\packages.$(MSBuildProjectName).config
-
-
-
- $(MSBuildProjectDirectory)\packages.config
- $(PackagesProjectConfig)
-
-
-
-
- $(NuGetToolsPath)\NuGet.exe
- @(PackageSource)
-
- "$(NuGetExePath)"
- mono --runtime=v4.0.30319 $(NuGetExePath)
-
- $(TargetDir.Trim('\\'))
-
- -RequireConsent
- -NonInteractive
-
- "$(SolutionDir) "
- "$(SolutionDir)"
-
-
- $(NuGetCommand) install "$(PackagesConfig)" -source "$(PackageSources)" $(NonInteractiveSwitch) $(RequireConsentSwitch) -solutionDir $(PaddedSolutionDir)
- $(NuGetCommand) pack "$(ProjectPath)" -Properties "Configuration=$(Configuration);Platform=$(Platform)" $(NonInteractiveSwitch) -OutputDirectory "$(PackageOutputDir)" -symbols
-
-
-
- RestorePackages;
- $(BuildDependsOn);
-
-
-
-
- $(BuildDependsOn);
- BuildPackage;
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/CodeContracts.sln b/CodeContracts.sln
index d0f4f7e5..d192902d 100644
--- a/CodeContracts.sln
+++ b/CodeContracts.sln
@@ -296,13 +296,9 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsForRoslyn", "M
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CCDocGenAttributes", "microsoft.research\ManagedContract.Setup\CCDocGenAttributes\CCDocGenAttributes.csproj", "{449B96DF-2C90-4495-B081-D97D4F02620E}"
EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Adornments", "Microsoft.Research\VSAdornments\VS2010\Adornments.csproj", "{784AA6A9-013E-4D8E-82D6-934571CF1357}"
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Adornments", "Microsoft.Research\VSAdornments\Adornments.csproj", "{784AA6A9-013E-4D8E-82D6-934571CF1357}"
EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Adornments11", "Microsoft.Research\VSAdornments\VS2012\Adornments11.csproj", "{235196BB-603A-470A-AF8E-EF6C8D01C4DC}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ContractAdornments", "Microsoft.Research\ContractAdornments\VS2010\ContractAdornments.csproj", "{D3F9BE8B-BA9F-4919-87CE-EE1878EDA40C}"
-EndProject
-Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ContractAdornments11", "Microsoft.Research\ContractAdornments\VS2012\ContractAdornments11.csproj", "{5982130C-B0DD-4E10-82F7-A23F40A16315}"
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ContractAdornments", "Microsoft.Research\ContractAdornments\Extension\ContractAdornments.csproj", "{D3F9BE8B-BA9F-4919-87CE-EE1878EDA40C}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BLResults", "Microsoft.Research\CCTools\BLResults\BLResults.csproj", "{6603246B-9D29-485C-BC38-E8E03F737BC4}"
EndProject
@@ -318,6 +314,16 @@ 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}") = "ContractAdornments.CSharp.10", "Microsoft.Research\ContractAdornments\CSharp\ContractAdornments.CSharp.10.csproj", "{233B4116-291E-446E-9C44-04B7FBC514FF}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ContractAdornments.CSharp.11", "Microsoft.Research\ContractAdornments\CSharp\ContractAdornments.CSharp.11.csproj", "{A73F8AEB-7D31-4D67-9D94-853D1BB597A6}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ContractAdornments.CSharp.12", "Microsoft.Research\ContractAdornments\CSharp\ContractAdornments.CSharp.12.csproj", "{9C55B970-24B3-4623-9BA2-2D0F070E31A0}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ContractAdornments.CSharp.14", "Microsoft.Research\ContractAdornments\CSharp.Roslyn\ContractAdornments.CSharp.14.csproj", "{7FB60D9A-CF16-46C0-8154-696D85F8D451}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ContractAdornments.Interfaces", "Microsoft.Research\ContractAdornments\Interfaces\ContractAdornments.Interfaces.csproj", "{B0C91C82-C1D8-4697-B07E-18E17D11EB41}"
+EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Debug|Any CPU = Debug|Any CPU
@@ -2099,6 +2105,7 @@ Global
{449B96DF-2C90-4495-B081-D97D4F02620E}.Release|Win32.ActiveCfg = Release|Any CPU
{449B96DF-2C90-4495-B081-D97D4F02620E}.Release|x86.ActiveCfg = Release|Any CPU
{784AA6A9-013E-4D8E-82D6-934571CF1357}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {784AA6A9-013E-4D8E-82D6-934571CF1357}.Debug|Any CPU.Build.0 = Debug|Any CPU
{784AA6A9-013E-4D8E-82D6-934571CF1357}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{784AA6A9-013E-4D8E-82D6-934571CF1357}.Debug|Win32.ActiveCfg = Debug|Any CPU
{784AA6A9-013E-4D8E-82D6-934571CF1357}.Debug|x86.ActiveCfg = Debug|Any CPU
@@ -2118,28 +2125,8 @@ Global
{784AA6A9-013E-4D8E-82D6-934571CF1357}.Release|Mixed Platforms.Build.0 = Release|Any CPU
{784AA6A9-013E-4D8E-82D6-934571CF1357}.Release|Win32.ActiveCfg = Release|Any CPU
{784AA6A9-013E-4D8E-82D6-934571CF1357}.Release|x86.ActiveCfg = Release|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Debug|Win32.ActiveCfg = Debug|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Debug|x86.ActiveCfg = Debug|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Devlab9|Any CPU.ActiveCfg = Devlab9|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Devlab9|Mixed Platforms.ActiveCfg = Devlab9|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Devlab9|Mixed Platforms.Build.0 = Devlab9|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Devlab9|Win32.ActiveCfg = Devlab9|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Devlab9|x86.ActiveCfg = Devlab9|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Internal9|Any CPU.ActiveCfg = Internal9|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Internal9|Mixed Platforms.ActiveCfg = Internal9|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Internal9|Mixed Platforms.Build.0 = Internal9|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Internal9|Win32.ActiveCfg = Internal9|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Internal9|x86.ActiveCfg = Internal9|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Release|Any CPU.Build.0 = Release|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Release|Win32.ActiveCfg = Release|Any CPU
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC}.Release|x86.ActiveCfg = Release|Any CPU
{D3F9BE8B-BA9F-4919-87CE-EE1878EDA40C}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {D3F9BE8B-BA9F-4919-87CE-EE1878EDA40C}.Debug|Any CPU.Build.0 = Debug|Any CPU
{D3F9BE8B-BA9F-4919-87CE-EE1878EDA40C}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
{D3F9BE8B-BA9F-4919-87CE-EE1878EDA40C}.Debug|Win32.ActiveCfg = Debug|Any CPU
{D3F9BE8B-BA9F-4919-87CE-EE1878EDA40C}.Debug|x86.ActiveCfg = Debug|Any CPU
@@ -2158,26 +2145,6 @@ Global
{D3F9BE8B-BA9F-4919-87CE-EE1878EDA40C}.Release|Mixed Platforms.Build.0 = Release|Any CPU
{D3F9BE8B-BA9F-4919-87CE-EE1878EDA40C}.Release|Win32.ActiveCfg = Release|Any CPU
{D3F9BE8B-BA9F-4919-87CE-EE1878EDA40C}.Release|x86.ActiveCfg = Release|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Debug|Any CPU.Build.0 = Debug|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Debug|Win32.ActiveCfg = Debug|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Debug|x86.ActiveCfg = Debug|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Devlab9|Any CPU.ActiveCfg = Devlab9|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Devlab9|Mixed Platforms.ActiveCfg = Devlab9|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Devlab9|Mixed Platforms.Build.0 = Devlab9|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Devlab9|Win32.ActiveCfg = Devlab9|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Devlab9|x86.ActiveCfg = Devlab9|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Internal9|Any CPU.ActiveCfg = Internal9|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Internal9|Mixed Platforms.ActiveCfg = Internal9|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Internal9|Mixed Platforms.Build.0 = Internal9|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Internal9|Win32.ActiveCfg = Internal9|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Internal9|x86.ActiveCfg = Internal9|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Release|Any CPU.ActiveCfg = Release|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Release|Mixed Platforms.Build.0 = Release|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Release|Win32.ActiveCfg = Release|Any CPU
- {5982130C-B0DD-4E10-82F7-A23F40A16315}.Release|x86.ActiveCfg = Release|Any CPU
{6603246B-9D29-485C-BC38-E8E03F737BC4}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
{6603246B-9D29-485C-BC38-E8E03F737BC4}.Debug|Any CPU.Build.0 = Debug|Any CPU
{6603246B-9D29-485C-BC38-E8E03F737BC4}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
@@ -2334,6 +2301,116 @@ 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
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Debug|Win32.ActiveCfg = Debug|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Devlab9|Any CPU.ActiveCfg = Devlab9|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Devlab9|Mixed Platforms.ActiveCfg = Devlab9|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Devlab9|Mixed Platforms.Build.0 = Devlab9|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Devlab9|Win32.ActiveCfg = Devlab9|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Devlab9|x86.ActiveCfg = Devlab9|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Internal9|Any CPU.ActiveCfg = Internal9|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Internal9|Mixed Platforms.ActiveCfg = Internal9|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Internal9|Mixed Platforms.Build.0 = Internal9|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Internal9|Win32.ActiveCfg = Internal9|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Internal9|x86.ActiveCfg = Internal9|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Release|Any CPU.Build.0 = Release|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Release|Win32.ActiveCfg = Release|Any CPU
+ {233B4116-291E-446E-9C44-04B7FBC514FF}.Release|x86.ActiveCfg = Release|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Debug|Win32.ActiveCfg = Debug|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Devlab9|Any CPU.ActiveCfg = Devlab9|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Devlab9|Mixed Platforms.ActiveCfg = Devlab9|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Devlab9|Mixed Platforms.Build.0 = Devlab9|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Devlab9|Win32.ActiveCfg = Devlab9|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Devlab9|x86.ActiveCfg = Devlab9|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Internal9|Any CPU.ActiveCfg = Internal9|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Internal9|Mixed Platforms.ActiveCfg = Internal9|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Internal9|Mixed Platforms.Build.0 = Internal9|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Internal9|Win32.ActiveCfg = Internal9|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Internal9|x86.ActiveCfg = Internal9|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Release|Any CPU.Build.0 = Release|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Release|Win32.ActiveCfg = Release|Any CPU
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6}.Release|x86.ActiveCfg = Release|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Debug|Win32.ActiveCfg = Debug|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Devlab9|Any CPU.ActiveCfg = Devlab9|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Devlab9|Mixed Platforms.ActiveCfg = Devlab9|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Devlab9|Mixed Platforms.Build.0 = Devlab9|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Devlab9|Win32.ActiveCfg = Devlab9|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Devlab9|x86.ActiveCfg = Devlab9|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Internal9|Any CPU.ActiveCfg = Internal9|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Internal9|Mixed Platforms.ActiveCfg = Internal9|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Internal9|Mixed Platforms.Build.0 = Internal9|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Internal9|Win32.ActiveCfg = Internal9|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Internal9|x86.ActiveCfg = Internal9|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Release|Any CPU.Build.0 = Release|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Release|Win32.ActiveCfg = Release|Any CPU
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0}.Release|x86.ActiveCfg = Release|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Debug|Win32.ActiveCfg = Debug|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Devlab9|Any CPU.ActiveCfg = Devlab9|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Devlab9|Mixed Platforms.ActiveCfg = Devlab9|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Devlab9|Mixed Platforms.Build.0 = Devlab9|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Devlab9|Win32.ActiveCfg = Devlab9|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Devlab9|x86.ActiveCfg = Devlab9|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Internal9|Any CPU.ActiveCfg = Internal9|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Internal9|Mixed Platforms.ActiveCfg = Internal9|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Internal9|Mixed Platforms.Build.0 = Internal9|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Internal9|Win32.ActiveCfg = Internal9|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Internal9|x86.ActiveCfg = Internal9|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Release|Any CPU.Build.0 = Release|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Release|Win32.ActiveCfg = Release|Any CPU
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451}.Release|x86.ActiveCfg = Release|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Debug|Win32.ActiveCfg = Debug|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Devlab9|Any CPU.ActiveCfg = Devlab9|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Devlab9|Mixed Platforms.ActiveCfg = Devlab9|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Devlab9|Mixed Platforms.Build.0 = Devlab9|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Devlab9|Win32.ActiveCfg = Devlab9|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Devlab9|x86.ActiveCfg = Devlab9|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Internal9|Any CPU.ActiveCfg = Internal9|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Internal9|Mixed Platforms.ActiveCfg = Internal9|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Internal9|Mixed Platforms.Build.0 = Internal9|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Internal9|Win32.ActiveCfg = Internal9|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Internal9|x86.ActiveCfg = Internal9|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Release|Any CPU.Build.0 = Release|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Release|Win32.ActiveCfg = Release|Any CPU
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41}.Release|x86.ActiveCfg = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
@@ -2425,9 +2502,7 @@ Global
{F9E1200C-C624-498A-BCB5-7E55CA1335F4} = {6468A140-0BAF-4813-A1EF-094DD7854C64}
{449B96DF-2C90-4495-B081-D97D4F02620E} = {7CD8B829-346E-4FA0-ADDD-87152DDC5DDE}
{784AA6A9-013E-4D8E-82D6-934571CF1357} = {7A308E8B-00AB-4ACF-8563-BF457A379EF1}
- {235196BB-603A-470A-AF8E-EF6C8D01C4DC} = {7A308E8B-00AB-4ACF-8563-BF457A379EF1}
{D3F9BE8B-BA9F-4919-87CE-EE1878EDA40C} = {7A308E8B-00AB-4ACF-8563-BF457A379EF1}
- {5982130C-B0DD-4E10-82F7-A23F40A16315} = {7A308E8B-00AB-4ACF-8563-BF457A379EF1}
{6603246B-9D29-485C-BC38-E8E03F737BC4} = {8C9BFE1D-90BD-4F88-B58E-89FF1DA325B8}
{CC40F8DC-AA1F-4816-8E2D-18AC2B02E847} = {21B40F99-9AB5-4E2D-AA6E-B9687F5C865A}
{407EF6D9-A736-4FEE-A522-789C64E74509} = {8C9BFE1D-90BD-4F88-B58E-89FF1DA325B8}
@@ -2435,6 +2510,11 @@ 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}
+ {233B4116-291E-446E-9C44-04B7FBC514FF} = {7A308E8B-00AB-4ACF-8563-BF457A379EF1}
+ {A73F8AEB-7D31-4D67-9D94-853D1BB597A6} = {7A308E8B-00AB-4ACF-8563-BF457A379EF1}
+ {9C55B970-24B3-4623-9BA2-2D0F070E31A0} = {7A308E8B-00AB-4ACF-8563-BF457A379EF1}
+ {7FB60D9A-CF16-46C0-8154-696D85F8D451} = {7A308E8B-00AB-4ACF-8563-BF457A379EF1}
+ {B0C91C82-C1D8-4697-B07E-18E17D11EB41} = {7A308E8B-00AB-4ACF-8563-BF457A379EF1}
EndGlobalSection
GlobalSection(TestCaseManagementSettings) = postSolution
CategoryFile = CodeContracts10.vsmdi
diff --git a/Microsoft.Research/Clousot.Cache/Clousot.Cache.csproj b/Microsoft.Research/Clousot.Cache/Clousot.Cache.csproj
index 06ff85a4..6aba7359 100644
--- a/Microsoft.Research/Clousot.Cache/Clousot.Cache.csproj
+++ b/Microsoft.Research/Clousot.Cache/Clousot.Cache.csproj
@@ -17,7 +17,6 @@
v4.0
512
..\..\
- true
true
@@ -181,13 +180,6 @@
-
-
-
- This project references NuGet package(s) that are missing on this computer. Enable NuGet Package Restore to download them. For more information, see http://go.microsoft.com/fwlink/?LinkID=322105. The missing file is {0}.
-
-
-
+
\ No newline at end of file
diff --git a/Microsoft.Research/ContractAdornments/CSharp.Roslyn/Contracts/CSharpToCCIHelper.cs b/Microsoft.Research/ContractAdornments/CSharp.Roslyn/Contracts/CSharpToCCIHelper.cs
new file mode 100644
index 00000000..d3bb88e5
--- /dev/null
+++ b/Microsoft.Research/ContractAdornments/CSharp.Roslyn/Contracts/CSharpToCCIHelper.cs
@@ -0,0 +1,402 @@
+// CodeContracts
+//
+// Copyright (c) Microsoft Corporation
+//
+// All rights reserved.
+//
+// MIT License
+//
+// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+//
+// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+//
+// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using Microsoft.Cci;
+using Microsoft.CodeAnalysis;
+
+namespace ContractAdornments {
+ ///
+ /// A helper class for the Visual Studio semantic CSharp model. This helper is aware of cci.
+ ///
+ ///
+ /// All methods in this class are [Pure], meaning they are side-effect free.
+ ///
+ public static class CSharpToCCIHelper {
+ ///
+ /// Gets the CCI CallingConventions for a semantic member. The calling convention for a CSharp method is "Defualt" (always) and "Generic" (if it is generic) and/or "HasThis" (if it is non-static).
+ ///
+ /// Thrown if the semantic member/type has fields that are null or empty and are required to not be so for the proper operation of this method.
+ [Pure]
+ public static CallingConvention GetCallingConventionFor(ISymbol semanticMember) {
+ Contract.Requires(semanticMember != null);
+
+ var callingConvention = CallingConvention.Default;
+ IMethodSymbol methodSymbol = semanticMember as IMethodSymbol;
+ if (methodSymbol != null && methodSymbol.IsGenericMethod)
+ callingConvention = callingConvention | CallingConvention.Generic;
+ if (!semanticMember.IsStatic)
+ callingConvention = callingConvention | CallingConvention.HasThis;
+ return callingConvention;
+ }
+ ///
+ /// Gets the CCI PrimitiveTypeCode for a semantic type. If the semantic type isn't a primitive type, the PrimitiveTypeCode "NotPrimitive" is used.
+ ///
+ /// Thrown if the semantic member/type has fields that are null or empty and are required to not be so for the proper operation of this method.
+ [Pure]
+ public static PrimitiveTypeCode GetPrimitiveTypeCode(ITypeSymbol type) {
+ Contract.Requires(type != null);
+ Contract.Ensures(Contract.Result() != PrimitiveTypeCode.Pointer &&
+ Contract.Result() != PrimitiveTypeCode.Reference &&
+ Contract.Result() != PrimitiveTypeCode.Invalid,
+ "These types aren't checked for; all others are.");
+ if(type.Name == null || String.IsNullOrEmpty(type.Name)) throw new IllFormedSemanticModelException("A CSharpType was found with a null or empty 'Name' field.", type);
+ switch (type.Name) {
+ case "Boolean": return PrimitiveTypeCode.Boolean;
+ case "Char": return PrimitiveTypeCode.Char;
+ case "SByte": return PrimitiveTypeCode.Int8;
+ case "Single": return PrimitiveTypeCode.Float32;
+ case "Double": return PrimitiveTypeCode.Float64;
+ case "Int16": return PrimitiveTypeCode.Int16;
+ case "Int32": return PrimitiveTypeCode.Int32;
+ case "Int64": return PrimitiveTypeCode.Int64;
+ case "IntPtr": return PrimitiveTypeCode.IntPtr;
+ case "String": return PrimitiveTypeCode.String;
+ case "Byte": return PrimitiveTypeCode.UInt8;
+ case "UInt16": return PrimitiveTypeCode.UInt32;
+ case "UInt32": return PrimitiveTypeCode.UInt64;
+ case "UIntPtr": return PrimitiveTypeCode.UIntPtr;
+ case "Void": return PrimitiveTypeCode.Void;
+ default: return PrimitiveTypeCode.NotPrimitive;
+ }
+ }
+ ///
+ /// Checks if two enumerables are equivalent.
+ ///
+ [Pure]
+ public static bool EnumerablesAreEquivalent(IEnumerable list1, IEnumerable list2, Func comparison) {
+ Contract.Requires(list1 != null);
+ Contract.Requires(list2 != null);
+ Contract.Requires(comparison != null);
+
+ var list1Enum = list1.GetEnumerator();
+ var list2Enum = list2.GetEnumerator();
+ bool list1Moved = list1Enum.MoveNext();
+ bool list2Moved = list2Enum.MoveNext();
+ if (list1Moved ^ list2Moved)
+ return false;
+ while (list1Moved && list2Moved) {
+ var item1 = list1Enum.Current;
+ var item2 = list2Enum.Current;
+ if (!comparison(item1, item2))
+ return false;
+ list1Moved = list1Enum.MoveNext();
+ list2Moved = list2Enum.MoveNext();
+ if (list1Moved ^ list2Moved)
+ return false;
+ }
+ return true;
+ }
+ ///
+ /// Checks if two semantic methods are equivalent.
+ ///
+ /// Thrown if the semantic member/type has fields that are null or empty and are required to not be so for the proper operation of this method.
+ [Pure]
+ public static bool MembersAreEquivalent(ISymbol member1, ISymbol member2) {
+ Contract.Requires(member1 != null);
+ Contract.Requires(member2 != null);
+ #region Check kind
+ if (member1.Kind != member2.Kind) return false;
+ if (member1.MethodKind() != member2.MethodKind()) return false;
+ if (member1.IsIndexer() ^ member2.IsIndexer()) return false;
+ #endregion
+ #region Check name
+ if (member1.Name == null ^ member2.Name == null) return false;
+ if (member1.Name!= null && member2.Name != null
+ && !member1.Name.Equals(member2.Name)) return false;
+ #endregion
+ #region Check explicit interface implementation
+ if (member1.ExplicitInterfaceImplementation() != null ^ member2.ExplicitInterfaceImplementation() != null) return false;
+ if (member1.ExplicitInterfaceImplementation() != null && member2.ExplicitInterfaceImplementation() != null
+ && !TypesAreEquivalent(member1.ExplicitInterfaceImplementation(), member2.ExplicitInterfaceImplementation())) return false;
+ #endregion
+ #region Check parameters
+ if (member1.Parameters().IsDefault ^ member2.Parameters().IsDefault) return false;
+ if (!member1.Parameters().IsDefault && !member2.Parameters().IsDefault
+ && !ParameterListsAreEquivalent(member1.Parameters(), member2.Parameters())) return false;
+ #endregion
+ #region Check return type
+ if (member1.ReturnType() == null) throw new IllFormedSemanticModelException("A CSharpMember (member) was found with a null 'ReturnType' field.", member1);
+ if (member2.ReturnType() == null) throw new IllFormedSemanticModelException("A CSharpMember (member) was found with a null 'ReturnType' field.", member2);
+ if (!TypesAreEquivalent(member1.ReturnType(), member2.ReturnType())) return false;
+ #endregion
+ return true;
+ }
+ ///
+ /// Checks if two parameters are equivalent.
+ ///
+ /// Thrown if the semantic member/type has fields that are null or empty and are required to not be so for the proper operation of this method.
+ [Pure]
+ public static bool ParametersAreEquivalent(IParameterSymbol param1, IParameterSymbol param2) {
+ Contract.Requires(param1 != null);
+ Contract.Requires(param2 != null);
+ //return param1.Equals(param2); //Doesn't work for our purposes.
+ if (param1.Type == null) throw new IllFormedSemanticModelException("A CSharpParameter was found with a null 'Type' field.", param1);
+ if (param2.Type == null) throw new IllFormedSemanticModelException("A CSharpParameter was found with a null 'Type' field.", param2);
+ if (!TypesAreEquivalent(param1.Type, param2.Type)) return false;
+ if ((param1.RefKind == RefKind.Out) ^ (param2.RefKind == RefKind.Out)) return false;
+ if (param1.IsParams ^ param2.IsParams) return false;
+ if ((param1.RefKind == RefKind.Ref) ^ (param2.RefKind == RefKind.Ref)) return false;
+ if (param1.IsThis ^ param2.IsThis) return false;
+ return true;
+ }
+ ///
+ /// Checks if two parameter lists are equivalent.
+ ///
+ /// Thrown if the semantic member/type has fields that are null or empty and are required to not be so for the proper operation of this method.
+ [Pure]
+ public static bool ParameterListsAreEquivalent(IEnumerable paramList1, IEnumerable paramList2) {
+ Contract.Requires(paramList1 != null);
+ Contract.Requires(paramList2 != null);
+ return EnumerablesAreEquivalent(paramList1, paramList2, (p1, p2) => ParametersAreEquivalent(p1, p2));
+ }
+ ///
+ /// Crawls upward in the semantic tree looking for the first base method this method inherits from.
+ ///
+ /// Thrown if the semantic member/type has fields that are null or empty and are required to not be so for the proper operation of this method.
+ [Pure]
+ public static bool TryGetBaseMember(ISymbol member, out ISymbol baseMember) {
+ Contract.Requires(member != null);
+ Contract.Ensures(!Contract.Result() ||
+ member.Kind == Contract.ValueAtReturn(out baseMember).Kind);
+
+ baseMember = null;
+
+ if (member.ContainingType == null) throw new IllFormedSemanticModelException("A CSharpMember (method) was found with a null 'ContainingType' field.", member);
+ if (member.ContainingType.TypeKind != TypeKind.Class) return false;
+ var containingType = member.ContainingType;
+ var baseClass = containingType.BaseType;
+ while (baseClass != null) {
+ if (TryGetMemberWithSameSignatureFromType(baseClass, member, out baseMember))
+ {
+ Contract.Assume(member.Kind == baseMember.Kind);
+ return true;
+ }
+ baseClass = baseClass.BaseType;
+ }
+ return false;
+ }
+ ///
+ ///
+ ///
+ /// Thrown if the semantic member/type has fields that are null or empty and are required to not be so for the proper operation of this method.
+ [Pure]
+ public static bool TryGetMemberWithSameSignatureFromType(ITypeSymbol type, ISymbol memberToMatch, out ISymbol member) {
+ Contract.Requires(type != null);
+ Contract.Requires(memberToMatch != null);
+ Contract.Ensures(!Contract.Result() || Contract.ValueAtReturn(out member) != null);
+
+ member = null;
+ var members = type.GetMembers();
+ foreach (var m in members) {
+ if (m == null) throw new IllFormedSemanticModelException("An null 'member' was found in a CSharpType's 'Members' field.", type);
+ if (MembersAreEquivalent(m, memberToMatch)) {
+ member = m;
+ return true;
+ }
+ }
+ return false;
+ }
+ ///
+ /// Crawls upward in the semantic tree looking for the first interface method that this method implements.
+ ///
+ /// Thrown if the semantic member/type has fields that are null or empty and are required to not be so for the proper operation of this method.
+ [Pure]
+ public static bool TryGetInterfaceMember(ISymbol member, out ISymbol interfaceMethod) {
+ Contract.Requires(member != null);
+ Contract.Ensures(!Contract.Result() ||
+ Contract.ValueAtReturn(out interfaceMethod) != null);
+
+ interfaceMethod = null;
+
+ if (member.ExplicitInterfaceImplementation() != null)
+ if (TryGetMemberWithSameSignatureFromType(member.ExplicitInterfaceImplementation(), member, out interfaceMethod))
+ {
+ return true;
+ }
+
+ if (member.ContainingType == null || member.ContainingType.AllInterfaces.IsDefault)
+ {
+ return false;
+ }
+
+ foreach (var i in member.ContainingType.AllInterfaces)
+ {
+ if (i == null) continue;
+ if (TryGetMemberWithSameSignatureFromType(i, member, out interfaceMethod))
+ {
+ return true;
+ }
+ }
+ return false;
+ }
+ ///
+ /// Checks if two types are equivalent.
+ ///
+ /// Thrown if the semantic member/type has fields that are null or empty and are required to not be so for the proper operation of this method.
+ [Pure]
+ public static bool TypesAreEquivalent(ITypeSymbol type1, ITypeSymbol type2) {
+ if (type1 == null && type2 == null) return true;
+ if (type1 == null) return false;
+ if (type2 == null) return false;
+
+ #region Check if type parameter
+ if ((type1.TypeKind == TypeKind.TypeParameter) != (type2.TypeKind == TypeKind.TypeParameter))
+ return false;
+ if (type1.TypeKind == TypeKind.TypeParameter) {
+ ITypeParameterSymbol typeParameter1 = (ITypeParameterSymbol)type1;
+ ITypeParameterSymbol typeParameter2 = (ITypeParameterSymbol)type2;
+ if (typeParameter1.HasReferenceTypeConstraint ^ typeParameter2.HasReferenceTypeConstraint) return false;
+ if (typeParameter1.HasValueTypeConstraint ^ typeParameter2.HasValueTypeConstraint) return false;
+ return true;
+ }
+ #endregion
+ //return type1.Equals(type2); //TODO: Can we use this? Doesn't seem to work for generic types like 'List'
+ #region Check name
+ //if (type1.Name == null) throw new IllFormedSemanticModelException("A CSharpType was founded with a null 'Name' field.", type1);
+ //if (type2.Name == null) throw new IllFormedSemanticModelException("A CSharpType was founded with a null 'Name' field.", type2);
+ //It seems array types always have null names
+ if (type1.Name != null ^ type2.Name != null) return false;
+ if (type1.Name != null && type2.Name != null &&
+ !type1.Name.Equals(type2.Name)) return false;
+ #endregion
+ #region Check containing type and namespace
+ if (type1.ContainingType != null ^ type2.ContainingType != null) return false;
+ if (type1.ContainingType != null && type2.ContainingType != null) {
+ if (!TypesAreEquivalent(type1.ContainingType, type2.ContainingType)) return false;
+ } else {
+ if (type1.ContainingNamespace != null ^ type2.ContainingNamespace != null) return false;
+ if (type1.ContainingNamespace != null && type2.ContainingNamespace != null &&
+ !type1.ContainingNamespace.Equals(type2.ContainingNamespace)) return false;
+ }
+ #endregion
+ #region Check type parameters
+ if (!type1.TypeParameters().IsDefault ^ !type2.TypeParameters().IsDefault) return false;
+ if (!type1.TypeParameters().IsDefault && !type2.TypeParameters().IsDefault &&
+ type1.TypeParameters().Length != type2.TypeParameters().Length) return false;
+ #endregion
+ #region Check type arguments
+
+ if (!type1.TypeArguments().IsDefault ^ !type2.TypeArguments().IsDefault) return false;
+ if (!type1.TypeArguments().IsDefault && !type2.TypeArguments().IsDefault &&
+ !TypeListsAreEquivalent(type1.TypeArguments(), type2.TypeArguments())) return false;
+ #endregion
+ #region Check array
+ if ((type1.TypeKind == TypeKind.Array) ^ (type2.TypeKind == TypeKind.Array)) return false;
+ if ((type1.TypeKind == TypeKind.Array) && (type2.TypeKind == TypeKind.Array))
+ return TypesAreEquivalent(type1.ElementType(), type2.ElementType());
+ #endregion
+ #region Check pointer
+ if ((type1.TypeKind == TypeKind.Pointer) ^ (type2.TypeKind == TypeKind.Pointer)) return false;
+ if ((type1.TypeKind == TypeKind.Pointer) && (type2.TypeKind == TypeKind.Pointer))
+ return TypesAreEquivalent(type1.ElementType(), type2.ElementType());
+ #endregion
+ if ((type1.TypeKind == TypeKind.Class) != (type2.TypeKind == TypeKind.Class)
+ || (type1.TypeKind == TypeKind.Struct) != (type2.TypeKind == TypeKind.Struct)
+ || type1.IsStatic != type2.IsStatic
+ || type1.IsValueType != type2.IsValueType)
+ return false;
+ return true;
+ }
+ ///
+ /// Checks if two type lists are equivalent.
+ ///
+ /// Thrown if the semantic member/type has fields that are null or empty and are required to not be so for the proper operation of this method.
+ [Pure]
+ public static bool TypeListsAreEquivalent(IEnumerable typeList1, IEnumerable typeList2) {
+ Contract.Requires(typeList1 != null);
+ Contract.Requires(typeList2 != null);
+ return EnumerablesAreEquivalent(typeList1, typeList2, (t1, t2) => TypesAreEquivalent(t1, t2));
+ }
+ [Pure]
+ public static ISymbol Uninstantiate(this ISymbol member) {
+ Contract.Requires(member != null);
+ Contract.Ensures(Contract.Result() != null);
+ Contract.Ensures(member.Kind == Contract.Result().Kind);
+
+ var uninstantiatedMember = member.OriginalDefinition;
+
+ Contract.Assume(member.Kind == uninstantiatedMember.Kind);
+ return uninstantiatedMember;
+ }
+ [Pure]
+ public static ITypeSymbol Uninstantiate(this ITypeSymbol type) {
+ Contract.Requires(type != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ var uninstantiatedType = type.OriginalDefinition;
+
+ return uninstantiatedType;
+ }
+ }
+
+ [Serializable]
+ public class IllFormedSemanticModelException : Exception {
+ public ISymbol BadMember { get; private set; }
+ public ITypeSymbol BadType { get; private set; }
+ public IParameterSymbol BadParameter { get; private set; }
+ public INamespaceSymbol BadNamespace { get; private set; }
+ public CSharpKind Kind { get; private set; }
+
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant((BadMember != null) == (Kind == CSharpKind.CSharpMember));
+ Contract.Invariant((BadType != null) == (Kind == CSharpKind.CSharpType));
+ Contract.Invariant((BadParameter != null) == (Kind == CSharpKind.CSharpParameter));
+ Contract.Invariant((BadNamespace != null) == (Kind == CSharpKind.CSharpNamespace));
+ }
+
+ public IllFormedSemanticModelException() { }
+ public IllFormedSemanticModelException(string message) : base(message) { }
+ public IllFormedSemanticModelException(string message, Exception inner) : base(message, inner) { }
+ public IllFormedSemanticModelException(string message, ITypeSymbol badType) : base(message) {
+ Contract.Requires(badType != null);
+
+ BadType = badType;
+ Kind = CSharpKind.CSharpType;
+ }
+ public IllFormedSemanticModelException(string message, ISymbol badMember) : base(message) {
+ Contract.Requires(badMember != null);
+
+ BadMember = badMember;
+ Kind = CSharpKind.CSharpMember;
+ }
+ public IllFormedSemanticModelException(string message, IParameterSymbol badParameter) : base(message) {
+ Contract.Requires(badParameter != null);
+
+ BadParameter = badParameter;
+ Kind = CSharpKind.CSharpParameter;
+ }
+ public IllFormedSemanticModelException(string message, INamespaceSymbol badNamespace) : base(message) {
+ Contract.Requires(badNamespace != null);
+
+ BadNamespace = badNamespace;
+ Kind = CSharpKind.CSharpNamespace;
+ }
+ protected IllFormedSemanticModelException(
+ System.Runtime.Serialization.SerializationInfo info,
+ System.Runtime.Serialization.StreamingContext context)
+ : base(info, context) { }
+ }
+
+ public enum CSharpKind {
+ None,
+ CSharpMember,
+ CSharpType,
+ CSharpParameter,
+ CSharpNamespace
+ }
+}
\ No newline at end of file
diff --git a/Microsoft.Research/ContractAdornments/CSharp.Roslyn/Contracts/ContractsProvider.cs b/Microsoft.Research/ContractAdornments/CSharp.Roslyn/Contracts/ContractsProvider.cs
new file mode 100644
index 00000000..3cde68b1
--- /dev/null
+++ b/Microsoft.Research/ContractAdornments/CSharp.Roslyn/Contracts/ContractsProvider.cs
@@ -0,0 +1,806 @@
+// CodeContracts
+//
+// Copyright (c) Microsoft Corporation
+//
+// All rights reserved.
+//
+// MIT License
+//
+// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+//
+// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+//
+// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.IO;
+using ContractAdornments.Interfaces;
+using Microsoft.Cci;
+using Microsoft.Cci.Contracts;
+using Microsoft.Cci.MutableContracts;
+using Microsoft.CodeAnalysis;
+using AssemblyIdentity = Microsoft.Cci.AssemblyIdentity;
+
+namespace ContractAdornments {
+ public class ContractsProvider : IContractsProvider {
+ readonly IProjectTracker _projectTracker;
+ INonlockingHost Host {
+ get {
+ Contract.Requires(_projectTracker.Host != null);
+ Contract.Ensures(Contract.Result() != null);
+
+ return _projectTracker.Host;
+ }
+ }
+
+ readonly Dictionary _semanticMembersToCCIMethods;
+ readonly Dictionary _semanticTypesToCCITypes;
+ readonly Dictionary _semanticAssemblysToCCIAssemblys;
+ readonly Dictionary> _semanticPropertiesToCCIAccessorMethods;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(_semanticAssemblysToCCIAssemblys != null);
+ Contract.Invariant(_semanticMembersToCCIMethods != null);
+ Contract.Invariant(_semanticTypesToCCITypes != null);
+ Contract.Invariant(_semanticPropertiesToCCIAccessorMethods != null);
+ Contract.Invariant(_projectTracker != null);
+ Contract.Invariant(Host != null);
+ }
+
+ public ContractsProvider(IProjectTracker projectTracker) {
+ Contract.Requires(projectTracker != null);
+
+ //Grab a pointer back to our project tracker
+ _projectTracker = projectTracker;
+
+ //Initialize our caches
+ _semanticMembersToCCIMethods = new Dictionary();
+ _semanticTypesToCCITypes = new Dictionary();
+ _semanticAssemblysToCCIAssemblys = new Dictionary();
+ _semanticPropertiesToCCIAccessorMethods = new Dictionary>();
+ }
+
+ public void Clear() {
+ //host = null;
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Clearing all caches in ContractsProvider.");
+
+ //Clear caches
+ _semanticAssemblysToCCIAssemblys.Clear();
+ _semanticMembersToCCIMethods.Clear();
+ _semanticTypesToCCITypes.Clear();
+ _semanticPropertiesToCCIAccessorMethods.Clear();
+ }
+ //int counter = 0;
+ [ContractVerification(true)]
+ public bool TryGetAssemblyReference(IAssemblySymbol semanticAssembly, out IAssemblyReference cciAssembly) {
+ Contract.Ensures(!Contract.Result() || Contract.ValueAtReturn(out cciAssembly) != null);
+
+ cciAssembly = null;
+
+ #region Check input
+ if (semanticAssembly == null) {
+ return false;
+ }
+ #endregion
+ #region Check cache
+ if (ContractsPackageAccessor.Current.VSOptionsPage.Caching)
+ if (_semanticAssemblysToCCIAssemblys.TryGetValue(semanticAssembly, out cciAssembly))
+ return cciAssembly != Dummy.AssemblyReference && cciAssembly != null;
+ #endregion
+ // distinguish between the AssemblyName and the ProjectName
+
+ var semanticAssemblyFileName = (semanticAssembly.Name == null) ? null : semanticAssembly.Name;
+ if (string.IsNullOrWhiteSpace(semanticAssemblyFileName)) return false;
+ var semanticAssemblyName = Path.GetFileName(semanticAssemblyFileName);
+ if (semanticAssemblyName.EndsWith(".dll") || semanticAssemblyName.EndsWith(".exe"))
+ semanticAssemblyName = semanticAssemblyName.Remove(semanticAssemblyName.Length - 4, 4);
+
+ #region Try to get assembly from previously loaded assemblies from host
+ foreach (var unit in Host.LoadedUnits) {
+ if (unit == null) continue;
+ if (unit is Dummy) continue;
+ if (unit.Name.Value == semanticAssemblyName) {
+ cciAssembly = (IAssemblyReference)unit;
+ if (cciAssembly.ResolvedAssembly.Location == semanticAssemblyFileName)
+ {
+ goto ReturnTrue;
+ }
+ }
+ }
+ #endregion
+ #region Check if assembly is the same as the current project's output assembly
+ if (_projectTracker.AssemblyIdentity != null && _projectTracker.AssemblyIdentity.Name != null) {
+ if (semanticAssemblyName.Equals(_projectTracker.AssemblyIdentity.Name.Value, StringComparison.OrdinalIgnoreCase) || semanticAssemblyName.Equals(_projectTracker.ProjectName, StringComparison.OrdinalIgnoreCase)) {
+ cciAssembly = new Microsoft.Cci.Immutable.AssemblyReference(this.Host, _projectTracker.AssemblyIdentity);
+ Host.AddLibPath(Path.Combine(Path.GetDirectoryName(semanticAssemblyFileName), "CodeContracts"));
+ Host.AddLibPath(Path.Combine(Path.GetDirectoryName(semanticAssemblyFileName), @"..\Debug\CodeContracts"));
+ goto ReturnTrue;
+ }
+ } else
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Assembly identity for the project: " + _projectTracker.ProjectName + " was null.");
+ #endregion
+ #region Build assembly reference
+ if (semanticAssembly.Name == null || string.IsNullOrWhiteSpace(semanticAssembly.Name)) goto ReturnFalseNoOutput; // because we have no name.
+ var projectName = Path.GetFileName(semanticAssembly.Name);
+ if (projectName.EndsWith(".dll") || projectName.EndsWith(".exe"))
+ projectName = projectName.Remove(projectName.Length - 4, 4);
+ var references = _projectTracker.References;
+ VSLangProj.Reference reference = null;
+ for (int i = 1, refcount = references == null ? 0 : references.Count; i <= refcount; i++)
+ {
+ var tempRef = references.Item(i);
+ if (tempRef == null) continue;
+ string refName = tempRef.Name;//Path.GetFileNameWithoutExtension(tempRef.Name);
+ if (refName == null) continue;
+ if (refName.Equals(projectName, StringComparison.OrdinalIgnoreCase)) {
+ reference = tempRef;
+ break;
+ }
+ }
+ if (reference != null) {
+ IName iName = Host.NameTable.GetNameFor(Path.GetFileNameWithoutExtension(reference.Path));
+ string culture = reference.Culture ?? "en";
+ Version version = new Version(reference.MajorVersion, reference.MinorVersion, reference.BuildNumber, reference.RevisionNumber);
+ string location = reference.Path;
+ if (!string.IsNullOrEmpty(location))
+ {
+ Host.AddLibPath(Path.Combine(location.Substring(0, location.Length - Path.GetFileName(location).Length), "CodeContracts"));
+ var assemblyIdentity = new AssemblyIdentity(iName, culture, version, Enumerable.Empty, location);
+ cciAssembly = new Microsoft.Cci.Immutable.AssemblyReference(this.Host, assemblyIdentity);
+ goto ReturnTrue;
+ }
+ }
+ goto ReturnFalse;
+ #endregion
+ #region ReturnTrue:
+ ReturnTrue:
+ if (ContractsPackageAccessor.Current.VSOptionsPage.Caching)
+ _semanticAssemblysToCCIAssemblys[semanticAssembly] = cciAssembly;
+ EnsureAssemblyIsLoaded(semanticAssembly, ref cciAssembly);
+ return true;
+ #endregion
+ #region ReturnFalse:
+ ReturnFalse:
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Failed to build assembly reference for: " + semanticAssembly.Name);
+ ReturnFalseNoOutput:
+ if (ContractsPackageAccessor.Current.VSOptionsPage.Caching)
+ _semanticAssemblysToCCIAssemblys[semanticAssembly] = Dummy.AssemblyReference;
+ return false;
+ #endregion
+ }
+ public bool TryGetPropertyContract(ISymbol semanticMember, out IMethodContract getterContract, out IMethodContract setterContract)
+ {
+ Contract.Requires(semanticMember == null || semanticMember.Kind == SymbolKind.Property);
+
+ getterContract = null;
+ setterContract = null;
+
+ #region Check input
+ if (semanticMember == null)
+ {
+ return false;
+ }
+ #endregion
+ IMethodReference getter, setter;
+ if (!TryGetPropertyAccessorReferences(semanticMember, out getter, out setter)) { return false; }
+
+ var success = false;
+ if (getter != null)
+ {
+ success |= TryGetMethodContract(getter, out getterContract);
+ }
+ if (setter != null)
+ {
+ success |= TryGetMethodContract(setter, out setterContract);
+ }
+ return success;
+ }
+ public bool TryGetMethodContract(ISymbol semanticMethod, out IMethodContract methodContract)
+ {
+ Contract.Requires(semanticMethod == null || semanticMethod.Kind == SymbolKind.Method);
+ Contract.Ensures(!Contract.Result() || (Contract.ValueAtReturn(out methodContract) != null));
+
+ methodContract = null;
+
+ #region Check input
+ if (semanticMethod == null) {
+ return false;
+ }
+ #endregion
+
+ #region Try get the reference then check for contracts
+ IMethodReference cciMethod;
+ if (TryGetMethodReference(semanticMethod, out cciMethod)) {
+ if (TryGetMethodContract(cciMethod, out methodContract)) {
+ return true;
+ } else {
+ //No need, detailed logs are written at all code paths in "TryGetMethodContract"
+ //ContractsPackageAccessor.Current.Logger.WriteToLog("Failed to get method contracts for: " + cciMethod.Name);
+ }
+ } else {
+ methodContract = null;
+ if (semanticMethod.Name != null)
+ {
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Failed to get CCI reference for: " + semanticMethod.Name);
+ }
+ }
+ return false;
+ #endregion
+ }
+ public bool TryGetMethodContract(IMethodReference method, out IMethodContract methodContract) {
+ Contract.Ensures(!Contract.Result() || (Contract.ValueAtReturn(out methodContract) != null));
+
+ methodContract = null;
+
+ #region Check input
+ if (method == null) {
+ return false;
+ }
+ #endregion
+ try {
+ // Resolving the method works *only* if the unit it is defined in has already been loaded.
+ // That should have happened as part of creating the IMethodReference.
+ var resolvedMethod = method.ResolvedMethod;
+ if (resolvedMethod != Dummy.Method) {
+ methodContract = ContractHelper.GetMethodContractForIncludingInheritedContracts(Host, resolvedMethod);
+ if (methodContract == null) {
+ methodContract = ContractDummy.MethodContract;
+ ContractsPackageAccessor.Current.Logger.WriteToLog(String.Format("Did not find any method contract(s) for '{0}'", method.Name));
+ } else {
+ ContractsPackageAccessor.Current.Logger.WriteToLog(
+ String.Format("Got method contract(s) for '{0}': {1} preconditions, {2} postconditions",
+ method.Name,
+ Microsoft.Cci.IteratorHelper.EnumerableCount(methodContract.Preconditions),
+ Microsoft.Cci.IteratorHelper.EnumerableCount(methodContract.Postconditions)));
+ }
+ } else {
+ ContractsPackageAccessor.Current.Logger.WriteToLog(String.Format("Method '{0}' resolved to dummy", method.Name));
+ }
+ } catch (NullReferenceException) {
+ methodContract = null;
+ ContractsPackageAccessor.Current.Logger.WriteToLog(String.Format("NullReferenceException thrown when getting contracts for '{0}'", method.Name));
+ }
+ return methodContract != null;
+ }
+ public bool TryGetMethodContractSafe(ISymbol semanticMehod, out IMethodContract methodContract) {
+ Contract.Requires(semanticMehod == null || semanticMehod.Kind == SymbolKind.Method);
+ Contract.Ensures(!Contract.Result() || (Contract.ValueAtReturn(out methodContract) != null));
+
+ methodContract = null;
+
+ #region Check input
+ if (semanticMehod == null) {
+ return false;
+ }
+ #endregion
+ #region Call TryGetMethodContract cautiously
+ try {
+ //Can we get contracts?
+ if (!TryGetMethodContract(semanticMehod, out methodContract))
+ return false;
+ }
+ #endregion
+ #region Abort on exception
+ //Give up on our contracts if we get an exception
+ catch (IllFormedSemanticModelException) {
+ return false;
+ } catch (InvalidOperationException e) {
+ if (!e.Message.Contains(ContractsPackageAccessor.InvalidOperationExceptionMessage_TheSnapshotIsOutOfDate))
+ throw e;
+ else
+ return false;
+ } catch (System.Runtime.InteropServices.COMException e) {
+ if (!e.Message.Contains(ContractsPackageAccessor.COMExceptionMessage_BindingFailed))
+ throw e;
+ else
+ return false;
+ }
+ #endregion
+
+ return methodContract != null;
+ }
+ public bool TryGetMethodReference(ISymbol semanticMethod, out IMethodReference cciMethod) {
+ Contract.Requires(semanticMethod == null || semanticMethod.Kind == SymbolKind.Method);
+ Contract.Ensures(!Contract.Result() || Contract.ValueAtReturn(out cciMethod) != null);
+
+ cciMethod = null;
+
+ #region Check input
+ if (semanticMethod == null) {
+ return false;
+ }
+ #endregion
+ #region Check cache
+ if (ContractsPackageAccessor.Current.VSOptionsPage.Caching)
+ if (_semanticMembersToCCIMethods.TryGetValue(semanticMethod, out cciMethod))
+ return (!(cciMethod is Dummy)) && cciMethod != null;
+ #endregion
+ #region Set up our working cci method
+ var workingCciMethod = new Microsoft.Cci.MutableCodeModel.MethodReference();
+ #endregion
+ #region Set the intern factory
+ workingCciMethod.InternFactory = Host.InternFactory;
+ #endregion
+ #region Get calling conventions
+ workingCciMethod.CallingConvention = CSharpToCCIHelper.GetCallingConventionFor(semanticMethod);
+ #endregion
+ #region Get containing type reference
+ ITypeReference containingType;
+ if (!TryGetTypeReference(semanticMethod.ContainingType, out containingType))
+ goto ReturnFalse;
+ workingCciMethod.ContainingType = containingType;
+ #endregion
+ #region Get return type reference
+ if (semanticMethod.IsConstructor())
+ workingCciMethod.Type = this.Host.PlatformType.SystemVoid;
+ else {
+ ITypeReference returnType;
+ if (!TryGetTypeReference(semanticMethod.ReturnType(), out returnType))
+ goto ReturnFalse;
+ workingCciMethod.Type = returnType;
+ }
+ #endregion
+ #region Get name
+ if (!semanticMethod.IsConstructor() && semanticMethod.Name == null) goto ReturnFalse;
+ workingCciMethod.Name = Host.NameTable.GetNameFor(semanticMethod.IsConstructor()?".ctor":semanticMethod.Name);
+ #endregion
+ #region Get generic param count
+ if (semanticMethod.TypeParameters().IsDefault)
+ workingCciMethod.GenericParameterCount = 0;
+ else
+ workingCciMethod.GenericParameterCount = (ushort)semanticMethod.TypeParameters().Length;
+ #endregion
+ #region Get parameter references
+ List cciParameters;
+ if (semanticMethod.Parameters().IsDefault) goto ReturnFalse;
+ Contract.Assume(semanticMethod.Parameters().Length <= ushort.MaxValue, "Should be a postcondition?");
+ if (!TryGetParametersList(semanticMethod.Parameters(), out cciParameters))
+ goto ReturnFalse;
+ workingCciMethod.Parameters = cciParameters;
+ #endregion
+ #region Get the assembly reference (this also ensures the assembly gets loaded properly)
+ IAssemblyReference assemblyReference;
+ TryGetAssemblyReference(semanticMethod.ContainingAssembly, out assemblyReference);
+ #endregion
+ cciMethod = workingCciMethod;
+ return true;
+ #region ReturnFalse:
+ ReturnFalse:
+ cciMethod = Dummy.MethodReference;
+ if (ContractsPackageAccessor.Current.VSOptionsPage.Caching)
+ _semanticMembersToCCIMethods[semanticMethod] = cciMethod;
+ return false;
+ #endregion
+ }
+ public bool TryGetNamespaceReference(INamespaceSymbol semanticNamespace, IAssemblyReference cciAssembly, out IUnitNamespaceReference cciNamespace) {
+ Contract.Ensures(!Contract.Result() || (Contract.ValueAtReturn(out cciNamespace) != null));
+
+ cciNamespace = null;
+
+ #region Check input
+ if (semanticNamespace == null || cciAssembly == null) {
+ return false;
+ }
+ #endregion
+ #region If root
+ try {
+ if (semanticNamespace.IsGlobalNamespace) {
+ cciNamespace = new Microsoft.Cci.MutableCodeModel.RootUnitNamespaceReference() { Unit = cciAssembly };
+ goto ReturnTrue;
+ }
+ } catch (InvalidOperationException e) { //For some reason, an InvalidOperationException may get thrown.
+ if (e.Message.Contains(ContractsPackageAccessor.InvalidOperationExceptionMessage_TheSnapshotIsOutOfDate))
+ goto ReturnFalse;
+ else
+ throw e;
+ }
+ #endregion
+ #region If nested
+ if (semanticNamespace.ContainingNamespace != null) {
+ IUnitNamespaceReference parentNs;
+ if (!TryGetNamespaceReference(semanticNamespace.ContainingNamespace, cciAssembly, out parentNs))
+ goto ReturnFalse;
+ if (semanticNamespace.Name == null) goto ReturnFalse;
+ cciNamespace = new Microsoft.Cci.Immutable.NestedUnitNamespaceReference(parentNs, Host.NameTable.GetNameFor(semanticNamespace.Name));
+ goto ReturnTrue;
+ }
+ #endregion
+ Contract.Assert(cciNamespace == null);
+ goto ReturnFalse;
+
+ #region ReturnTrue:
+ ReturnTrue:
+ return true;
+ #endregion
+ #region ReturnFalse:
+ ReturnFalse:
+ return false;
+ #endregion
+ }
+ public bool TryGetParametersList(IList semanticParameters, out List cciParameters, ushort indexOffset = 0) {
+ Contract.Requires(semanticParameters != null);
+ Contract.Ensures(!Contract.Result() || Contract.ValueAtReturn(out cciParameters) != null);
+ cciParameters = null;
+
+ #region Check input
+ if (semanticParameters == null || semanticParameters.Count + indexOffset > ushort.MaxValue) {
+ return false;
+ }
+ #endregion
+ #region Get parameter count
+ var paramCount = semanticParameters.Count;
+ #endregion
+ #region Initialize our parameter list
+ cciParameters = new List(paramCount);
+ #endregion
+ #region Populate the parameter list
+ for (ushort i = 0; i < paramCount; i++) {
+ var semanticParam = semanticParameters[i];
+ Contract.Assume(semanticParam != null);
+ IParameterTypeInformation cciParam;
+ if (!TryGetParameterReference(semanticParam, (ushort)(i + indexOffset), out cciParam))
+ goto ReturnFalse;
+ cciParameters.Add(cciParam);
+ }
+ #endregion
+ return true;
+ #region ReturnFalse:
+ ReturnFalse:
+ return false;
+ #endregion
+ }
+ public bool TryGetParameterReference(IParameterSymbol semanticParameter, ushort index, out IParameterTypeInformation cciParameter) {
+
+ cciParameter = null;
+
+ #region Check input
+ if (semanticParameter == null) {
+ return false;
+ }
+ #endregion
+ #region Set up our working cci parameter
+ Microsoft.Cci.MutableCodeModel.ParameterTypeInformation workingParameter = null;
+ cciParameter = workingParameter = new Microsoft.Cci.MutableCodeModel.ParameterTypeInformation();
+ #endregion
+ #region Get our parameter type
+ ITypeReference paramType;
+ if (!TryGetTypeReference(semanticParameter.Type, out paramType))
+ goto ReturnFalse;
+ workingParameter.Type = paramType;
+ #endregion
+ #region Get our index
+ workingParameter.Index = index;
+ #endregion
+ #region Get our reference status
+ workingParameter.IsByReference = semanticParameter.RefKind == RefKind.Out || semanticParameter.RefKind == RefKind.Ref;
+ #endregion
+ #region ReturnTrue:
+ //ReturnTrue:
+ return cciParameter != Dummy.ParameterTypeInformation;
+ #endregion
+ #region ReturnFalse:
+ ReturnFalse:
+ if (semanticParameter.Name != null)
+ {
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Failed to build parameter reference for: " + semanticParameter.Name);
+ }
+ return false;
+ #endregion
+ }
+ public bool TryGetPropertyAccessorReferences(ISymbol semanticProperty, out IMethodReference getter, out IMethodReference setter) {
+ Contract.Requires(semanticProperty == null || semanticProperty.Kind == SymbolKind.Property);
+
+ getter = setter = null;
+
+ #region Check input
+ if (semanticProperty == null) {
+ return false;
+ }
+ #endregion
+ #region Check cache
+ Tuple cacheOutput;
+ if (_semanticPropertiesToCCIAccessorMethods.TryGetValue(semanticProperty, out cacheOutput)) {
+ Contract.Assume(cacheOutput != null, "Non-null only dictionary");
+ getter = cacheOutput.Item1;
+ setter = cacheOutput.Item2;
+ return (getter != null && getter != Dummy.MethodReference) || (setter != null && setter != Dummy.MethodReference);
+ }
+ #endregion
+ #region Get calling conventions
+ var callingConventions = CSharpToCCIHelper.GetCallingConventionFor(semanticProperty);
+ #endregion
+ #region get containing type
+ ITypeReference containingType;
+ if (!TryGetTypeReference(semanticProperty.ContainingType, out containingType))
+ goto ReturnFalse;
+ #endregion
+ #region Get return type
+ ITypeReference returnType;
+ if (!TryGetTypeReference(semanticProperty.ReturnType(), out returnType))
+ goto ReturnFalse;
+ #endregion
+ #region Get the property's name
+ string propertyName;
+ if (semanticProperty.IsIndexer())
+ propertyName = "Item";
+ else
+ {
+ if (semanticProperty.Name == null) goto ReturnFalse;
+ propertyName = semanticProperty.Name;
+ }
+ #endregion
+ #region Get the parameters
+ List getterParams;
+ if (!semanticProperty.Parameters().IsDefault) {
+ if (!TryGetParametersList(semanticProperty.Parameters(), out getterParams))
+ goto ReturnFalse;
+ } else
+ getterParams = new List();
+
+ List setterParams;
+ if (!semanticProperty.Parameters().IsDefault) {
+ if (!TryGetParametersList(semanticProperty.Parameters(), out setterParams, 1))
+ goto ReturnFalse;
+ #region Append the "value" param
+ var valParam = new Microsoft.Cci.MutableCodeModel.ParameterTypeInformation() {
+ Type = returnType,
+ Index = 0,
+ IsByReference = false
+ };
+ setterParams.Insert(0, valParam);
+ #endregion
+ } else
+ setterParams = new List();
+ #endregion
+ #region Build the getter
+ getter = new Microsoft.Cci.MutableCodeModel.MethodReference() {
+ InternFactory = Host.InternFactory,
+ CallingConvention = callingConventions,
+ ContainingType = containingType,
+ Type = returnType,
+ Name = Host.NameTable.GetNameFor("get_" + propertyName),
+ GenericParameterCount = 0,
+ Parameters = getterParams
+ };
+ #endregion
+ #region Build the setter
+ setter = new Microsoft.Cci.MutableCodeModel.MethodReference() {
+ InternFactory = Host.InternFactory,
+ CallingConvention = callingConventions,
+ ContainingType = containingType,
+ Type = Host.PlatformType.SystemVoid,
+ Name = Host.NameTable.GetNameFor("set_" + propertyName),
+ GenericParameterCount = 0,
+ Parameters = setterParams
+ };
+ #endregion
+ #region Get the assembly reference (this also ensures the assembly gets loaded properly)
+ IAssemblyReference assemblyReference;
+ TryGetAssemblyReference(semanticProperty.ContainingAssembly, out assemblyReference);
+ #endregion
+ #region ReturnTrue:
+ //ReturnTrue:
+ _semanticPropertiesToCCIAccessorMethods[semanticProperty] = new Tuple(getter, setter);
+ return true;
+ #endregion
+ #region ReturnFalse:
+ ReturnFalse:
+ if (semanticProperty.Name != null)
+ {
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Failed to build accessor references for: " + semanticProperty.Name);
+ }
+ _semanticPropertiesToCCIAccessorMethods[semanticProperty] = new Tuple(Dummy.MethodReference, Dummy.MethodReference);
+ return false;
+ #endregion
+ }
+ public bool TryGetTypeReference(ITypeSymbol semanticType, IAssemblyReference cciAssembly, out ITypeReference cciType) {
+ Contract.Ensures(!Contract.Result() || (Contract.ValueAtReturn(out cciType) != null));
+
+ cciType = null;
+
+ #region Check input
+ if (semanticType == null || cciAssembly == null) {
+ return false;
+ }
+ #endregion
+ #region Check cache
+ if (ContractsPackageAccessor.Current.VSOptionsPage.Caching)
+ if (_semanticTypesToCCITypes.TryGetValue(semanticType, out cciType))
+ return cciType != null && cciType != Dummy.TypeReference;
+ #endregion
+ #region If generic
+ if (!semanticType.TypeArguments().IsDefault && semanticType.TypeArguments().Length > 0) {
+ var genericArguments = new List();
+ foreach (var semanticTypeArg in semanticType.TypeArguments()) {
+ if (semanticTypeArg == null) goto ReturnFalse;
+ ITypeReference cciTypeArg = null;
+ if (TryGetTypeReference(semanticTypeArg, out cciTypeArg)) {
+ genericArguments.Add(cciTypeArg);
+ } else {
+ goto ReturnFalse;
+ }
+ }
+ ITypeReference genericType = null;
+ if (!TryGetTypeReference(semanticType.ContainingType, out genericType)) {
+ goto ReturnFalse;
+ }
+ cciType = new Microsoft.Cci.MutableCodeModel.GenericTypeInstanceReference() {
+ InternFactory = this.Host.InternFactory,
+ GenericArguments = genericArguments,
+ GenericType = (INamedTypeReference) genericType,
+ };
+ goto ReturnTrue;
+ }
+ #endregion
+ #region If array
+ if (semanticType.TypeKind == TypeKind.Array) {
+ ITypeReference eleType;
+ if (!TryGetTypeReference(semanticType.ElementType(), out eleType))
+ goto ReturnFalse;
+ if (semanticType.ElementType().TypeKind == TypeKind.Array) {
+ Contract.Assume(((IArrayTypeSymbol)semanticType).Rank > 0);
+ cciType = new Microsoft.Cci.MutableCodeModel.MatrixTypeReference() {
+ ElementType = eleType,
+ InternFactory = this.Host.InternFactory,
+ Rank = (uint)((IArrayTypeSymbol)semanticType).Rank
+ };
+ goto ReturnTrue;
+ } else {
+ cciType = new Microsoft.Cci.MutableCodeModel.VectorTypeReference() {
+ ElementType = eleType,
+ InternFactory = this.Host.InternFactory,
+ };
+ goto ReturnTrue;
+ }
+ }
+ #endregion
+ #region If type parameter
+ if (semanticType.TypeKind == TypeKind.TypeParameter) {
+ if (semanticType.ContainingSymbol != null && semanticType.ContainingSymbol.Kind == SymbolKind.Method) {
+ cciType = new Microsoft.Cci.MutableCodeModel.GenericMethodParameterReference() {
+ Index = (ushort)(!semanticType.ContainingSymbol.TypeParameters().IsDefault ? semanticType.ContainingSymbol.TypeParameters().IndexOf((ITypeParameterSymbol)semanticType) : 0),
+ InternFactory = this.Host.InternFactory,
+ Name = Host.NameTable.GetNameFor(semanticType.Name != null ? semanticType.Name : "T"),
+ };
+ goto ReturnTrue;
+ } else if (semanticType.ContainingType != null) {
+ ITypeReference cciDefiningType;
+ if (!TryGetTypeReference(semanticType.ContainingType, out cciDefiningType))
+ goto ReturnFalse;
+ cciType = new Microsoft.Cci.MutableCodeModel.GenericTypeParameterReference() {
+ DefiningType = cciDefiningType,
+ Index = (ushort)(semanticType.ContainingType.TypeParameters != null ? semanticType.ContainingType.TypeParameters.IndexOf((ITypeParameterSymbol)semanticType) : 0),
+ InternFactory = this.Host.InternFactory,
+ Name = Host.NameTable.GetNameFor(semanticType.Name != null ? semanticType.Name : "T"),
+ };
+ goto ReturnTrue;
+ }
+ }
+ #endregion
+ #region If namespace type
+ if (semanticType.ContainingType == null)
+ {
+ IUnitNamespaceReference cciNamespace;
+ var namespaceName = semanticType.ContainingNamespace;
+ if (namespaceName == null || !TryGetNamespaceReference(namespaceName, cciAssembly, out cciNamespace))
+ {
+ cciNamespace = new Microsoft.Cci.MutableCodeModel.RootUnitNamespaceReference() { Unit = cciAssembly };
+ }
+ if (semanticType.ContainingType == null)
+ {
+ if (semanticType.Name == null || semanticType.Name == null) goto ReturnFalse;
+ cciType = new Microsoft.Cci.MutableCodeModel.NamespaceTypeReference()
+ {
+ ContainingUnitNamespace = cciNamespace,
+ GenericParameterCount = (ushort) (semanticType.TypeParameters().IsDefault ? 0 : semanticType.TypeParameters().Length),
+ InternFactory = Host.InternFactory,
+ IsValueType = semanticType.IsValueType,
+ IsEnum = semanticType.TypeKind == TypeKind.Enum,
+ Name = Host.NameTable.GetNameFor(semanticType.Name),
+ TypeCode = CSharpToCCIHelper.GetPrimitiveTypeCode(semanticType),
+ };
+ goto ReturnTrue;
+ }
+ }
+ #endregion
+ #region If nested type
+ if (semanticType.ContainingType != null) {
+ ITypeReference containingType;
+ if (!TryGetTypeReference(semanticType.ContainingType, cciAssembly, out containingType))
+ goto ReturnFalse;
+ if (semanticType.Name == null || semanticType.Name == null) goto ReturnFalse;
+ cciType = new Microsoft.Cci.MutableCodeModel.NestedTypeReference()
+ {
+ ContainingType = containingType,
+ GenericParameterCount = (ushort)(semanticType.TypeParameters().IsDefault ? 0 : semanticType.TypeParameters().Length),
+ InternFactory = this.Host.InternFactory,
+ MangleName = true,
+ Name = Host.NameTable.GetNameFor(semanticType.Name)
+ };
+ goto ReturnTrue;
+ }
+ #endregion
+ #region ReturnTrue:
+ ReturnTrue:
+ if (ContractsPackageAccessor.Current.VSOptionsPage.Caching)
+ _semanticTypesToCCITypes[semanticType] = cciType;
+ return true;
+ #endregion
+ #region ReturnFalse:
+ ReturnFalse:
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Failed to build type reference for: " + (semanticType.Name != null ? semanticType.Name : semanticType.ToString()));
+ if (ContractsPackageAccessor.Current.VSOptionsPage.Caching)
+ _semanticTypesToCCITypes[semanticType] = Dummy.TypeReference;
+ return false;
+ #endregion
+ }
+ public bool TryGetTypeReference(ITypeSymbol semanticType, out ITypeReference cciType) {
+ Contract.Ensures(!Contract.Result() || Contract.ValueAtReturn(out cciType) != null && semanticType != null);
+
+ cciType = null;
+
+ #region Check input
+ if (semanticType == null) {
+ return false;
+ }
+ #endregion
+ #region Check cache
+ if (ContractsPackageAccessor.Current.VSOptionsPage.Caching)
+ if (_semanticTypesToCCITypes.TryGetValue(semanticType, out cciType))
+ return cciType != null && cciType != Dummy.TypeReference;
+ #endregion
+ #region Get assembly reference
+ IAssemblyReference cciAssembly;
+ if (!TryGetAssemblyReference(semanticType.ContainingAssembly, out cciAssembly))
+ goto ReturnFalse;
+ #endregion
+ return TryGetTypeReference(semanticType, cciAssembly, out cciType);
+ #region ReturnFalse:
+ ReturnFalse:
+ if (ContractsPackageAccessor.Current.VSOptionsPage.Caching)
+ _semanticTypesToCCITypes[semanticType] = Dummy.TypeReference;
+ return false;
+ #endregion
+ }
+
+ [ContractVerification(true)]
+ void EnsureAssemblyIsLoaded(IAssemblySymbol semanticAssembly, ref IAssemblyReference assemblyReference) {
+ Contract.Ensures(assemblyReference != null || Contract.OldValue(assemblyReference) == null);
+ #region Check input
+ if (semanticAssembly == null || assemblyReference == null) {
+ return;
+ }
+ #endregion
+
+ var assembly = assemblyReference as IAssembly;
+ if (assembly == null) {
+ assembly = Host.FindAssembly(assemblyReference.AssemblyIdentity);
+ if (assembly == Dummy.Assembly) {
+ var location = assemblyReference.AssemblyIdentity.Location;
+ if (File.Exists(location)) {
+ ContractsPackageAccessor.Current.Logger.WriteToLog(String.Format("Calling LoadUnitFrom on assembly '{0}' for future resolution.", location));
+ ContractsPackageAccessor.Current.Logger.WriteToLog(String.Format("core assembly: '{0}'", Host.CoreAssemblySymbolicIdentity.ToString()));
+ assembly = Host.LoadUnitFrom(location) as IAssembly;
+ if (assembly != null){
+ assemblyReference = assembly;
+ if(ContractsPackageAccessor.Current.VSOptionsPage.Caching)
+ _semanticAssemblysToCCIAssemblys[semanticAssembly] = assembly;
+ }
+ else{
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Warning: Found a unit at '" + location + "', but it wasn't an assembly!");
+ }
+ } else{
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Assembly not found at: '" + location + "'. This could be because the assembly hasn't been built yet.");
+ }
+ } else {
+ assemblyReference = assembly;
+ if(ContractsPackageAccessor.Current.VSOptionsPage.Caching)
+ _semanticAssemblysToCCIAssemblys[semanticAssembly] = assembly;
+ }
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/Microsoft.Research/ContractAdornments/CSharp.Roslyn/Extensions.cs b/Microsoft.Research/ContractAdornments/CSharp.Roslyn/Extensions.cs
new file mode 100644
index 00000000..035c1516
--- /dev/null
+++ b/Microsoft.Research/ContractAdornments/CSharp.Roslyn/Extensions.cs
@@ -0,0 +1,118 @@
+// CodeContracts
+//
+// Copyright (c) Microsoft Corporation
+//
+// All rights reserved.
+//
+// MIT License
+//
+// Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+//
+// The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+//
+// THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+using System.Diagnostics.Contracts;
+using Adornments;
+using ContractAdornments.Interfaces;
+using Microsoft.CodeAnalysis;
+using Microsoft.CodeAnalysis.CSharp.Syntax;
+using Microsoft.CodeAnalysis.Text;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Editor;
+
+namespace ContractAdornments {
+ static class HelperExtensions {
+ public static string GetFileName(this ITextView @this) {
+ Contract.Requires(@this != null);
+
+ if (@this.TextBuffer == null) return null;
+ return @this.TextBuffer.GetFileName();
+ }
+ public static string GetFileName(this ITextBuffer @this) {
+ Contract.Requires(@this != null);
+ ITextDocument doc;
+ if (@this.Properties == null) return null;
+ if (@this.Properties.TryGetProperty(typeof(ITextDocument), out doc)) {
+ Contract.Assume(doc != null);
+ if (doc.FilePath == null) { return null; }
+ return doc.FilePath.ToLower();
+ }
+ return null;
+ }
+
+ public static SnapshotSpan Convert(this LinePositionSpan span, ITextSnapshot snapshot) {
+ Contract.Requires(snapshot != null);
+ var startIndex = snapshot.GetPositionFromLineColumn(span.Start.Line, span.Start.Character);
+ var endIndex = snapshot.GetPositionFromLineColumn(span.End.Line, span.End.Character);
+ // still need to do range check: have seen this be too long
+ var len = endIndex - startIndex;
+ var maxLen = snapshot.Length - startIndex;
+ var usableLength = len > maxLen ? maxLen : len; // min(len,maxLen)
+ return new SnapshotSpan(snapshot, startIndex, usableLength);
+ }
+
+ public static LinePosition Convert(this ITrackingPoint point, ITextSnapshot snapshot) {
+ Contract.Requires(point != null);
+
+ var snapshotPoint = point.GetPoint(snapshot);
+ var line = snapshotPoint.GetContainingLine();
+ if (line == null) return default(LinePosition);
+ int lineIndex = line.LineNumber;
+ int charIndex = snapshotPoint.Position - line.Start.Position;
+ return new LinePosition(lineIndex, charIndex);
+ }
+
+ public static int GetPositionFromLineColumn(this ITextSnapshot snapshot, int line, int column) {
+ Contract.Requires(snapshot != null);
+
+ var textline = snapshot.GetLineFromLineNumber(line);
+ if (textline == null) return 0;
+ return textline.Start.Position + column;
+ }
+
+ public static string GetName(this PropertyDeclarationSyntax @this, ITextSnapshot snapshot) {
+ Contract.Requires(@this != null);
+ Contract.Requires(snapshot != null);
+ return @this.Identifier.ValueText;
+ }
+
+ public static string GetName(this MethodDeclarationSyntax @this, ITextSnapshot snapshot) {
+ Contract.Requires(@this != null);
+ Contract.Requires(snapshot != null);
+ return @this.Identifier.ValueText;
+ }
+
+ public static string GetName(this BaseTypeDeclarationSyntax @this, ITextSnapshot snapshot) {
+ Contract.Requires(@this != null);
+ Contract.Requires(snapshot != null);
+ return @this.Identifier.ValueText;
+ }
+
+ public static bool IsModelReady(this SyntaxTree parseTree) {
+ Contract.Requires(parseTree != null);
+ SyntaxNode ignored;
+ return parseTree.TryGetRoot(out ignored);
+ }
+ }
+ public static class AdornmentOptionsHelper {
+ public static AdornmentOptions GetAdornmentOptions(IContractOptionsPage options) {
+ var result = AdornmentOptions.None;
+
+ if (options == null)
+ return result;
+
+ if (options.SmartFormatting)
+ result = result | AdornmentOptions.SmartFormatting;
+
+ if (options.SyntaxColoring)
+ result = result | AdornmentOptions.SyntaxColoring;
+
+ if (options.CollapseMetadataContracts)
+ {
+ result = result | AdornmentOptions.CollapseWithRegion;
+ }
+ return result;
+ }
+ }
+}
\ No newline at end of file
diff --git a/Microsoft.Research/ContractAdornments/CSharp.Roslyn/ISymbolExtensions.cs b/Microsoft.Research/ContractAdornments/CSharp.Roslyn/ISymbolExtensions.cs
new file mode 100644
index 00000000..92d34899
--- /dev/null
+++ b/Microsoft.Research/ContractAdornments/CSharp.Roslyn/ISymbolExtensions.cs
@@ -0,0 +1,126 @@
+// Copyright (c) Microsoft. All rights reserved.
+// Licensed under the MIT license. See LICENSE file in the project root for full license information.
+
+namespace ContractAdornments
+{
+ using System;
+ using System.Collections.Immutable;
+ using System.Linq;
+ using Microsoft.CodeAnalysis;
+
+ internal static class ISymbolExtensions
+ {
+ public static MethodKind? MethodKind(this ISymbol symbol)
+ {
+ IMethodSymbol methodSymbol = symbol as IMethodSymbol;
+ if (methodSymbol == null)
+ return null;
+
+ return methodSymbol.MethodKind;
+ }
+
+ public static bool IsConstructor(this ISymbol symbol)
+ {
+ return symbol.MethodKind() == Microsoft.CodeAnalysis.MethodKind.Constructor;
+ }
+
+ public static bool IsIndexer(this ISymbol symbol)
+ {
+ IPropertySymbol propertySymbol = symbol as IPropertySymbol;
+ if (propertySymbol == null)
+ return false;
+
+ return propertySymbol.IsIndexer;
+ }
+
+ public static ITypeSymbol ReturnType(this ISymbol symbol)
+ {
+ switch (symbol.Kind)
+ {
+ case SymbolKind.Property:
+ return ((IPropertySymbol)symbol).Type;
+
+ case SymbolKind.Method:
+ return ((IMethodSymbol)symbol).ReturnType;
+
+ default:
+ return null;
+ }
+ }
+
+ public static ImmutableArray TypeArguments(this ITypeSymbol symbol)
+ {
+ INamedTypeSymbol namedTypeSymbol = symbol as INamedTypeSymbol;
+ if (namedTypeSymbol == null)
+ return default(ImmutableArray);
+
+ return namedTypeSymbol.TypeArguments;
+ }
+
+ public static ITypeSymbol ElementType(this ITypeSymbol symbol)
+ {
+ switch (symbol.TypeKind)
+ {
+ case TypeKind.Array:
+ return ((IArrayTypeSymbol)symbol).ElementType;
+
+ case TypeKind.Pointer:
+ return ((IPointerTypeSymbol)symbol).PointedAtType;
+
+ default:
+ return null;
+ }
+ }
+
+ public static ImmutableArray TypeParameters(this ISymbol symbol)
+ {
+ switch (symbol.Kind)
+ {
+ case SymbolKind.Method:
+ return ((IMethodSymbol)symbol).TypeParameters;
+
+ case SymbolKind.NamedType:
+ return ((INamedTypeSymbol)symbol).TypeParameters;
+
+ default:
+ return ImmutableArray.Empty;
+ }
+ }
+
+ public static ImmutableArray Parameters(this ISymbol symbol)
+ {
+ switch (symbol.Kind)
+ {
+ case SymbolKind.Property:
+ return ((IPropertySymbol)symbol).Parameters;
+
+ case SymbolKind.Method:
+ return ((IMethodSymbol)symbol).Parameters;
+
+ default:
+ throw new NotSupportedException();
+ }
+ }
+
+ public static ITypeSymbol ExplicitInterfaceImplementation(this ISymbol symbol)
+ {
+ switch (symbol.Kind)
+ {
+ case SymbolKind.Property:
+ IPropertySymbol firstProperty = ((IPropertySymbol)symbol).ExplicitInterfaceImplementations.FirstOrDefault();
+ return firstProperty != null ? firstProperty.ContainingType : null;
+
+ case SymbolKind.Method:
+ IMethodSymbol firstMethod = ((IMethodSymbol)symbol).ExplicitInterfaceImplementations.FirstOrDefault();
+ return firstMethod != null ? firstMethod.ContainingType : null;
+
+ case SymbolKind.Event:
+ IEventSymbol firstEvent = ((IEventSymbol)symbol).ExplicitInterfaceImplementations.FirstOrDefault();
+ return firstEvent != null ? firstEvent.ContainingType : null;
+
+ default:
+ throw new NotSupportedException();
+ }
+ }
+ }
+}
diff --git a/Microsoft.Research/ContractAdornments/Sources/Inheritance/InheritanceTracker.cs b/Microsoft.Research/ContractAdornments/CSharp.Roslyn/Inheritance/InheritanceTracker.cs
similarity index 65%
rename from Microsoft.Research/ContractAdornments/Sources/Inheritance/InheritanceTracker.cs
rename to Microsoft.Research/ContractAdornments/CSharp.Roslyn/Inheritance/InheritanceTracker.cs
index 296544fd..ded19ecc 100644
--- a/Microsoft.Research/ContractAdornments/Sources/Inheritance/InheritanceTracker.cs
+++ b/Microsoft.Research/ContractAdornments/CSharp.Roslyn/Inheritance/InheritanceTracker.cs
@@ -73,7 +73,7 @@ private InheritanceTracker(TextViewTracker textViewTracker) {
Contract.Requires(textViewTracker != null);
Contract.Requires(textViewTracker.TextView != null);
if (!AdornmentManager.TryGetAdornmentManager(textViewTracker.TextView, "InheritanceAdornments", out _adornmentManager)) {
- VSServiceProvider.Current.Logger.WriteToLog("Inheritance adornment layer not instantiated.");
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Inheritance adornment layer not instantiated.");
throw new InvalidOperationException("Inheritance adornment layer not instantiated.");
}
@@ -96,7 +96,7 @@ void OnClosed(object sender, EventArgs e) {
}
void OnBuildDone() {
- VSServiceProvider.Current.Logger.WriteToLog("Removing all old adornments because of a new build for text file: " + _textViewTracker.FileName);
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Removing all old adornments because of a new build for text file: " + _textViewTracker.FileName);
_adornmentManager.Adornments.Clear();
_methodsNeedingContractLookup.Clear();
_propertiesNeedingContractLookup.Clear();
@@ -110,10 +110,10 @@ void OnLatestSourceFileChanged(object sender, LatestSourceFileChangedEventArgs e
if (e.WasLatestSourceFileStale == true) {
//Revaluate the inheritance adornments on the text view when we next have focus
- if (VSServiceProvider.Current.VSOptionsPage.InheritanceOnMethods)
- VSServiceProvider.Current.QueueWorkItem(() => RevaluateMethodInheritanceAdornments(this), () => _textViewTracker.TextView.HasAggregateFocus);
- if (VSServiceProvider.Current.VSOptionsPage.InheritanceOnProperties)
- VSServiceProvider.Current.QueueWorkItem(() => RevaluatePropertyInheritanceAdornments(this), () => _textViewTracker.TextView.HasAggregateFocus);
+ if (ContractsPackageAccessor.Current.VSOptionsPage.InheritanceOnMethods)
+ ContractsPackageAccessor.Current.QueueWorkItem(() => RevaluateMethodInheritanceAdornments(this), () => _textViewTracker.TextView.HasAggregateFocus);
+ if (ContractsPackageAccessor.Current.VSOptionsPage.InheritanceOnProperties)
+ ContractsPackageAccessor.Current.QueueWorkItem(() => RevaluatePropertyInheritanceAdornments(this), () => _textViewTracker.TextView.HasAggregateFocus);
}
}
void OnLatestCompilationChanged(object sender, LatestCompilationChangedEventArgs e) {
@@ -121,19 +121,19 @@ void OnLatestCompilationChanged(object sender, LatestCompilationChangedEventArgs
Contract.Requires(e.LatestCompilation != null);
//Do any methods need their contract information looked up?
- if (VSServiceProvider.Current.VSOptionsPage.InheritanceOnMethods && _methodsNeedingContractLookup.Count > 0) {
+ if (ContractsPackageAccessor.Current.VSOptionsPage.InheritanceOnMethods && _methodsNeedingContractLookup.Count > 0) {
//Recursively look up the needed contract information
- VSServiceProvider.Current.Logger.WriteToLog("Attempting to lookup contracts for " + _methodsNeedingContractLookup.Count + " methods.");
- VSServiceProvider.Current.QueueWorkItem(() => RecursivelyLookupContractsForMethods(this), () => _textViewTracker.TextView.HasAggregateFocus);
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Attempting to lookup contracts for " + _methodsNeedingContractLookup.Count + " methods.");
+ ContractsPackageAccessor.Current.QueueWorkItem(() => RecursivelyLookupContractsForMethods(this), () => _textViewTracker.TextView.HasAggregateFocus);
}
//Do any properties need their contract information looked up?
- if (VSServiceProvider.Current.VSOptionsPage.InheritanceOnProperties && _propertiesNeedingContractLookup.Count > 0) {
+ if (ContractsPackageAccessor.Current.VSOptionsPage.InheritanceOnProperties && _propertiesNeedingContractLookup.Count > 0) {
//Recursively look up the needed contract information
- VSServiceProvider.Current.Logger.WriteToLog("Attempting to lookup contracts for " + _propertiesNeedingContractLookup.Count + " properties.");
- VSServiceProvider.Current.QueueWorkItem(() => RecursivelyLookupContractsForProperties(this), () => _textViewTracker.TextView.HasAggregateFocus);
+ ContractsPackageAccessor.Current.Logger.WriteToLog("Attempting to lookup contracts for " + _propertiesNeedingContractLookup.Count + " properties.");
+ ContractsPackageAccessor.Current.QueueWorkItem(() => RecursivelyLookupContractsForProperties(this), () => _textViewTracker.TextView.HasAggregateFocus);
}
}
@@ -144,9 +144,9 @@ static void RevaluateMethodInheritanceAdornments(InheritanceTracker @this) {
//Check if model is ready
var parseTree = @this._textViewTracker.LatestSourceFile == null ? null : @this._textViewTracker.LatestSourceFile.GetParseTree();
- if (parseTree == null || !VSServiceProvider.IsModelReady(parseTree)) {
+ if (parseTree == null || !parseTree.IsModelReady()) {
@this._textViewTracker.IsLatestSourceFileStale = true;
- Utilities.Delay(() => VSServiceProvider.Current.AskForNewVSModel(), DelayOnVSModelFailedBeforeTryingAgain);
+ Utilities.Delay(() => ContractsPackageAccessor.Current.AskForNewVSModel(), DelayOnVSModelFailedBeforeTryingAgain);
return;
}
@@ -157,41 +157,41 @@ static void RevaluateMethodInheritanceAdornments(InheritanceTracker @this) {
//Calculate which methods are new
var newKeys = new List