Boogie: VCGeneration port part 3/3: Updating sources to reference new project; making Core work with the port by removing the nonnull requirements on one abstract method.

7 files changed, 24 insertions, 23 deletions

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index 0a3f8adb..0b365158 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -13,8 +13,6 @@ Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "Graph", "Graph\Graph.sscpro
 EndProject

 Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "VCExpr", "VCExpr\VCExpr.sscproj", "{CF42B700-10AA-4DA9-8992-48A800251C11}"

 EndProject

-Project("{07C4E3D1-6B67-4060-8A92-940DB82041ED}") = "VCGeneration", "VCGeneration\VCGeneration.sscproj", "{F65666DE-FB56-457C-8782-09BE243450FC}"

-EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BoogieDriver", "BoogieDriver\BoogieDriver.csproj", "{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}"

 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Isabelle", "Provers\Isabelle\Isabelle.csproj", "{435D5BD0-6F62-49F8-BB24-33E2257519AD}"

@@ -27,6 +25,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "Provers\SMTLib\SM
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Simplify", "Provers\Simplify\Simplify.csproj", "{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}"

 EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "VCGeneration\VCGeneration.csproj", "{E1F10180-C7B9-4147-B51F-FA1B701966DC}"

+EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Debug|.NET = Debug|.NET

@@ -87,16 +87,6 @@ Global
 		{CF42B700-10AA-4DA9-8992-48A800251C11}.Release|Any CPU.ActiveCfg = Release|.NET

 		{CF42B700-10AA-4DA9-8992-48A800251C11}.Release|Mixed Platforms.ActiveCfg = Release|.NET

 		{CF42B700-10AA-4DA9-8992-48A800251C11}.Release|Mixed Platforms.Build.0 = Release|.NET

-		{F65666DE-FB56-457C-8782-09BE243450FC}.Debug|.NET.ActiveCfg = Debug|.NET

-		{F65666DE-FB56-457C-8782-09BE243450FC}.Debug|.NET.Build.0 = Debug|.NET

-		{F65666DE-FB56-457C-8782-09BE243450FC}.Debug|Any CPU.ActiveCfg = Debug|.NET

-		{F65666DE-FB56-457C-8782-09BE243450FC}.Debug|Mixed Platforms.ActiveCfg = Debug|.NET

-		{F65666DE-FB56-457C-8782-09BE243450FC}.Debug|Mixed Platforms.Build.0 = Debug|.NET

-		{F65666DE-FB56-457C-8782-09BE243450FC}.Release|.NET.ActiveCfg = Release|.NET

-		{F65666DE-FB56-457C-8782-09BE243450FC}.Release|.NET.Build.0 = Release|.NET

-		{F65666DE-FB56-457C-8782-09BE243450FC}.Release|Any CPU.ActiveCfg = Release|.NET

-		{F65666DE-FB56-457C-8782-09BE243450FC}.Release|Mixed Platforms.ActiveCfg = Release|.NET

-		{F65666DE-FB56-457C-8782-09BE243450FC}.Release|Mixed Platforms.Build.0 = Release|.NET

 		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.ActiveCfg = Debug|Any CPU

 		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|.NET.Build.0 = Debug|Any CPU

 		{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

@@ -159,6 +149,16 @@ Global
 		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Any CPU.Build.0 = Release|Any CPU

 		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|.NET.ActiveCfg = Debug|Any CPU

+		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|.NET.ActiveCfg = Release|Any CPU

+		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Any CPU.Build.0 = Release|Any CPU

+		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{E1F10180-C7B9-4147-B51F-FA1B701966DC}.Release|Mixed Platforms.Build.0 = Release|Any CPU

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index 5a0f4ef1..8b7c31ce 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -129,8 +129,8 @@
       <Project>{CF42B700-10AA-4DA9-8992-48A800251C11}</Project>

       <Name>VCExpr</Name>

     </ProjectReference>

-    <ProjectReference Include="..\VCGeneration\VCGeneration.sscproj">

-      <Project>{F65666DE-FB56-457C-8782-09BE243450FC}</Project>

+    <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">

+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

   </ItemGroup>

diff --git a/Source/Core/VCExp.ssc b/Source/Core/VCExp.ssc
index 4b42a639..650b3145 100644
--- a/Source/Core/VCExp.ssc
+++ b/Source/Core/VCExp.ssc
@@ -143,7 +143,8 @@ namespace Microsoft.Boogie {
   public abstract class ProverFactory

   {

     // Really returns ProverInterface.

-    public abstract object! SpawnProver(ProverOptions! options, object! ctxt);

+    //public abstract object! SpawnProver(ProverOptions! options, object! ctxt);

+    public abstract object SpawnProver(ProverOptions options, object ctxt);

 

     // Really returns ProverContext

     public abstract object! NewProverContext(ProverOptions! options);

diff --git a/Source/Provers/Isabelle/Isabelle.csproj b/Source/Provers/Isabelle/Isabelle.csproj
index 799131d6..9347d72f 100644
--- a/Source/Provers/Isabelle/Isabelle.csproj
+++ b/Source/Provers/Isabelle/Isabelle.csproj
@@ -89,8 +89,8 @@
       <Project>{CF42B700-10AA-4DA9-8992-48A800251C11}</Project>

       <Name>VCExpr</Name>

     </ProjectReference>

-    <ProjectReference Include="..\..\VCGeneration\VCGeneration.sscproj">

-      <Project>{F65666DE-FB56-457C-8782-09BE243450FC}</Project>

+    <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj">

+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

   </ItemGroup>

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index 55acbc78..21941194 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -99,8 +99,8 @@
       <Project>{CF42B700-10AA-4DA9-8992-48A800251C11}</Project>

       <Name>VCExpr</Name>

     </ProjectReference>

-    <ProjectReference Include="..\..\VCGeneration\VCGeneration.sscproj">

-      <Project>{F65666DE-FB56-457C-8782-09BE243450FC}</Project>

+    <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj">

+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

     <ProjectReference Include="..\Simplify\Simplify.csproj">

diff --git a/Source/Provers/Simplify/Simplify.csproj b/Source/Provers/Simplify/Simplify.csproj
index 4a817fec..86d8eb31 100644
--- a/Source/Provers/Simplify/Simplify.csproj
+++ b/Source/Provers/Simplify/Simplify.csproj
@@ -96,8 +96,8 @@
       <Project>{CF42B700-10AA-4DA9-8992-48A800251C11}</Project>

       <Name>VCExpr</Name>

     </ProjectReference>

-    <ProjectReference Include="..\..\VCGeneration\VCGeneration.sscproj">

-      <Project>{F65666DE-FB56-457C-8782-09BE243450FC}</Project>

+    <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj">

+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

   </ItemGroup>

diff --git a/Source/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj
index 305e56bc..7e2b546a 100644
--- a/Source/Provers/Z3/Z3.csproj
+++ b/Source/Provers/Z3/Z3.csproj
@@ -97,8 +97,8 @@
       <Project>{CF42B700-10AA-4DA9-8992-48A800251C11}</Project>

       <Name>VCExpr</Name>

     </ProjectReference>

-    <ProjectReference Include="..\..\VCGeneration\VCGeneration.sscproj">

-      <Project>{F65666DE-FB56-457C-8782-09BE243450FC}</Project>

+    <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj">

+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

       <Name>VCGeneration</Name>

     </ProjectReference>

     <ProjectReference Include="..\Simplify\Simplify.csproj">