Split up the model viewer into a library and an application and added some functionality.

7 files changed, 208 insertions, 24 deletions

diff --git a/Source/BVD/App.config b/Source/BVD/App.config
new file mode 100644
index 00000000..fad249e4
--- /dev/null
+++ b/Source/BVD/App.config
@@ -0,0 +1,6 @@
+<?xml version="1.0" encoding="utf-8" ?>

+<configuration>

+    <startup> 

+        <supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.5" />

+    </startup>

+</configuration>
\ No newline at end of file
diff --git a/Source/BVD/BVD.csproj b/Source/BVD/BVD.csproj
new file mode 100644
index 00000000..0b32dd22
--- /dev/null
+++ b/Source/BVD/BVD.csproj
@@ -0,0 +1,99 @@
+<?xml version="1.0" encoding="utf-8"?>

+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

+  <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

+  <PropertyGroup>

+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

+    <ProjectGuid>{8A05D14E-F2BF-4890-BBE0-D76B18A50797}</ProjectGuid>

+    <OutputType>WinExe</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>Microsoft.Boogie.ModelViewer</RootNamespace>

+    <AssemblyName>BVD</AssemblyName>

+    <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+    <PublishUrl>publish\</PublishUrl>

+    <Install>true</Install>

+    <InstallFrom>Disk</InstallFrom>

+    <UpdateEnabled>false</UpdateEnabled>

+    <UpdateMode>Foreground</UpdateMode>

+    <UpdateInterval>7</UpdateInterval>

+    <UpdateIntervalUnits>Days</UpdateIntervalUnits>

+    <UpdatePeriodically>false</UpdatePeriodically>

+    <UpdateRequired>false</UpdateRequired>

+    <MapFileExtensions>true</MapFileExtensions>

+    <ApplicationRevision>0</ApplicationRevision>

+    <ApplicationVersion>1.0.0.%2a</ApplicationVersion>

+    <IsWebBootstrapper>false</IsWebBootstrapper>

+    <UseApplicationTrust>false</UseApplicationTrust>

+    <BootstrapperEnabled>true</BootstrapperEnabled>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>..\..\Binaries\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <DebugType>pdbonly</DebugType>

+    <Optimize>true</Optimize>

+    <OutputPath>bin\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <PropertyGroup>

+    <StartupObject />

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="System" />

+    <Reference Include="System.Core" />

+    <Reference Include="System.Data" />

+    <Reference Include="System.Deployment" />

+    <Reference Include="System.Drawing" />

+    <Reference Include="System.Numerics" />

+    <Reference Include="System.Windows.Forms" />

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="Program.cs" />

+    <Compile Include="Properties\AssemblyInfo.cs" />

+  </ItemGroup>

+  <ItemGroup>

+    <None Include="App.config" />

+  </ItemGroup>

+  <ItemGroup>

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

+      <Project>{a678c6eb-b329-46a9-bbfc-7585f01acd7c}</Project>

+      <Name>ModelViewer</Name>

+    </ProjectReference>

+  </ItemGroup>

+  <ItemGroup>

+    <BootstrapperPackage Include=".NETFramework,Version=v4.5">

+      <Visible>False</Visible>

+      <ProductName>Microsoft .NET Framework 4.5 %28x86 and x64%29</ProductName>

+      <Install>true</Install>

+    </BootstrapperPackage>

+    <BootstrapperPackage Include="Microsoft.Net.Client.3.5">

+      <Visible>False</Visible>

+      <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>

+      <Install>false</Install>

+    </BootstrapperPackage>

+    <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">

+      <Visible>False</Visible>

+      <ProductName>.NET Framework 3.5 SP1</ProductName>

+      <Install>false</Install>

+    </BootstrapperPackage>

+  </ItemGroup>

+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

+       Other similar extension points exist, see Microsoft.Common.targets.

+  <Target Name="BeforeBuild">

+  </Target>

+  <Target Name="AfterBuild">

+  </Target>

+  -->

+</Project>
\ No newline at end of file
diff --git a/Source/ModelViewer/Program.cs b/Source/BVD/Program.cs
index 669ea995..669ea995 100644
--- a/Source/ModelViewer/Program.cs
+++ b/Source/BVD/Program.cs
diff --git a/Source/BVD/Properties/AssemblyInfo.cs b/Source/BVD/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..3512374e
--- /dev/null
+++ b/Source/BVD/Properties/AssemblyInfo.cs
@@ -0,0 +1,36 @@
+using System.Reflection;

+using System.Runtime.CompilerServices;

+using System.Runtime.InteropServices;

+

+// General Information about an assembly is controlled through the following 

+// set of attributes. Change these attribute values to modify the information

+// associated with an assembly.

+[assembly: AssemblyTitle("BVD")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

+[assembly: AssemblyCompany("")]

+[assembly: AssemblyProduct("BVD")]

+[assembly: AssemblyCopyright("Copyright ©  2013")]

+[assembly: AssemblyTrademark("")]

+[assembly: AssemblyCulture("")]

+

+// Setting ComVisible to false makes the types in this assembly not visible 

+// to COM components.  If you need to access a type in this assembly from 

+// COM, set the ComVisible attribute to true on that type.

+[assembly: ComVisible(false)]

+

+// The following GUID is for the ID of the typelib if this project is exposed to COM

+[assembly: Guid("00610a12-cf4c-4c29-af30-31a99d22b9d8")]

+

+// Version information for an assembly consists of the following four values:

+//

+//      Major Version

+//      Minor Version 

+//      Build Number

+//      Revision

+//

+// You can specify all the values or you can default the Build and Revision Numbers 

+// by using the '*' as shown below:

+// [assembly: AssemblyVersion("1.0.*")]

+[assembly: AssemblyVersion("1.0.0.0")]

+[assembly: AssemblyFileVersion("1.0.0.0")]

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index b93bc31f..cadcaacb 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -35,6 +35,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Doomed", "Doomed\Doomed.csp
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "ExecutionEngine\ExecutionEngine.csproj", "{EAA5EB79-D475-4601-A59B-825C191CD25F}"

 EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BVD", "BVD\BVD.csproj", "{8A05D14E-F2BF-4890-BBE0-D76B18A50797}"

+EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Checked|.NET = Checked|.NET

@@ -455,6 +457,30 @@ Global
 		{EAA5EB79-D475-4601-A59B-825C191CD25F}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{EAA5EB79-D475-4601-A59B-825C191CD25F}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

 		{EAA5EB79-D475-4601-A59B-825C191CD25F}.z3apidebug|x86.ActiveCfg = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|.NET.ActiveCfg = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|Any CPU.ActiveCfg = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|Any CPU.Build.0 = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|Mixed Platforms.Build.0 = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Checked|x86.ActiveCfg = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|.NET.ActiveCfg = Debug|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Debug|x86.ActiveCfg = Debug|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|.NET.ActiveCfg = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Any CPU.Build.0 = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.Release|x86.ActiveCfg = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|.NET.ActiveCfg = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Any CPU.Build.0 = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

+		{8A05D14E-F2BF-4890-BBE0-D76B18A50797}.z3apidebug|x86.ActiveCfg = Release|Any CPU

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/Source/ModelViewer/Main.cs b/Source/ModelViewer/Main.cs
index 2e612aa1..1caed654 100644
--- a/Source/ModelViewer/Main.cs
+++ b/Source/ModelViewer/Main.cs
@@ -10,6 +10,7 @@ using System.Windows.Forms;
 

 using System.IO;

 using Microsoft.Boogie;

+using System.Diagnostics.Contracts;

 

 namespace Microsoft.Boogie.ModelViewer

 {

@@ -92,6 +93,18 @@ namespace Microsoft.Boogie.ModelViewer
       }

     }

 

+    public void ReadModel(string model, int setModelIdTo = 0)

+    {

+      Contract.Requires(model != null);

+

+      using (var rd = new StringReader(model))

+      {

+        allModels = Model.ParseModels(rd).ToArray();

+      }

+

+      AddAndLoadModel(setModelIdTo);

+    }

+

     public void ReadModels(string modelFileName, int setModelIdTo)

     {

       this.lastModelFileName = modelFileName;

@@ -102,28 +115,34 @@ namespace Microsoft.Boogie.ModelViewer
           allModels = Model.ParseModels(rd).ToArray();

         }

 

-        modelId = setModelIdTo;

-

-        if (modelId >= allModels.Length)

-          modelId = 0;

-

-        currentModel = allModels[modelId];

-        AddModelMenu();

-

-        foreach (var p in Providers()) {

-          if (p.IsMyModel(currentModel)) {

-            this.langProvider = p;

-            break;

-          }

-        }

-

-        LoadModel(modelId);

+        AddAndLoadModel(setModelIdTo);

       } else {

         currentModel = new Model();

       }

 

       this.SetWindowTitle(modelFileName);

+    }

+

+    private void AddAndLoadModel(int setModelIdTo)

+    {

+      modelId = setModelIdTo;

+

+      if (modelId >= allModels.Length)

+        modelId = 0;

+

+      currentModel = allModels[modelId];

+      AddModelMenu();

+

+      foreach (var p in Providers())

+      {

+        if (p.IsMyModel(currentModel))

+        {

+          this.langProvider = p;

+          break;

+        }

+      }

 

+      LoadModel(modelId);

     }

 

     private void LoadModel(int idx)

diff --git a/Source/ModelViewer/ModelViewer.csproj b/Source/ModelViewer/ModelViewer.csproj
index ae46767b..f708ddda 100644
--- a/Source/ModelViewer/ModelViewer.csproj
+++ b/Source/ModelViewer/ModelViewer.csproj
@@ -6,10 +6,10 @@
     <ProductVersion>8.0.30703</ProductVersion>

     <SchemaVersion>2.0</SchemaVersion>

     <ProjectGuid>{A678C6EB-B329-46A9-BBFC-7585F01ACD7C}</ProjectGuid>

-    <OutputType>WinExe</OutputType>

+    <OutputType>Library</OutputType>

     <AppDesignerFolder>Properties</AppDesignerFolder>

     <RootNamespace>Microsoft.Boogie.ModelViewer</RootNamespace>

-    <AssemblyName>BVD</AssemblyName>

+    <AssemblyName>ModelViewer</AssemblyName>

     <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

     <TargetFrameworkProfile>Client</TargetFrameworkProfile>

     <FileAlignment>512</FileAlignment>

@@ -98,18 +98,17 @@
     <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

     <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

   </PropertyGroup>

+  <PropertyGroup>

+    <StartupObject />

+  </PropertyGroup>

   <ItemGroup>

     <Reference Include="System" />

     <Reference Include="System.Core" />

-    <Reference Include="System.Numerics" />

-    <Reference Include="System.Xml.Linq" />

-    <Reference Include="System.Data.DataSetExtensions" />

-    <Reference Include="Microsoft.CSharp" />

     <Reference Include="System.Data" />

+    <Reference Include="System.Numerics" />

     <Reference Include="System.Deployment" />

     <Reference Include="System.Drawing" />

     <Reference Include="System.Windows.Forms" />

-    <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

     <Compile Include="BaseProvider.cs" />

@@ -124,7 +123,6 @@
     </Compile>

     <Compile Include="..\Model\Model.cs" />

     <Compile Include="Namer.cs" />

-    <Compile Include="Program.cs" />

     <Compile Include="Properties\AssemblyInfo.cs" />

     <Compile Include="SourceView.cs">

       <SubType>Form</SubType>