Introduce unit tests which use NUnit. NUnit is now a dependency

so developers need to install it via NuGet.

There aren't many tests yet. Just a few for Core and Basetypes but
hopefully more will be added in the future.

More information can be found in Source/UnitTests/README.md

6 files changed, 195 insertions, 0 deletions

diff --git a/Source/UnitTests/TestUtil/AssertionTextWriterTraceListener.cs b/Source/UnitTests/TestUtil/AssertionTextWriterTraceListener.cs
new file mode 100644
index 00000000..961ed0df
--- /dev/null
+++ b/Source/UnitTests/TestUtil/AssertionTextWriterTraceListener.cs
@@ -0,0 +1,27 @@
+using NUnit.Framework;
+using System;
+using System.Diagnostics;
+
+namespace Microsoft.Boogie
+{
+  namespace TestUtil
+  {
+
+    public class AssertionTextWriterTraceListener : TextWriterTraceListener {
+      public AssertionTextWriterTraceListener(System.IO.Stream stream) : base(stream) { }
+
+      public AssertionTextWriterTraceListener(System.IO.TextWriter writer) : base(writer) { }
+
+      public override void Fail(string message) {
+        base.Fail(message);
+        Assert.Fail(message);
+      }
+
+      public override void Fail(string message, string detailMessage) {
+        base.Fail(message, detailMessage);
+        Assert.Fail(message + " : " + detailMessage);
+      }
+    }
+  }
+}
+
diff --git a/Source/UnitTests/TestUtil/BoogieTestBase.cs b/Source/UnitTests/TestUtil/BoogieTestBase.cs
new file mode 100644
index 00000000..2bac71a4
--- /dev/null
+++ b/Source/UnitTests/TestUtil/BoogieTestBase.cs
@@ -0,0 +1,24 @@
+using NUnit.Framework;
+using System;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace Microsoft.Boogie
+{
+  namespace TestUtil
+  {
+    public class BoogieTestBase {
+
+      public BoogieTestBase() {
+        // Debug log output goes to standard error.
+        // Failing System.Diagnostics failures trigger NUnit assertion failures
+        Debug.Listeners.Add(new AssertionTextWriterTraceListener(Console.Error));
+
+        // FIXME: THIS IS A HACK. Boogie's methods
+        // depend on its command line parser being set!
+        CommandLineOptions.Install(new Microsoft.Boogie.CommandLineOptions());
+      }
+    }
+  }
+}
+
diff --git a/Source/UnitTests/TestUtil/ProgramLoader.cs b/Source/UnitTests/TestUtil/ProgramLoader.cs
new file mode 100644
index 00000000..bc5f647a
--- /dev/null
+++ b/Source/UnitTests/TestUtil/ProgramLoader.cs
@@ -0,0 +1,33 @@
+using NUnit.Framework;
+using System;
+using Microsoft.Boogie;
+
+namespace TestUtil
+{
+	public class ProgramLoader
+	{
+		public static Program LoadProgramFrom(string programText, string fileName="file.bpl")
+		{
+			Assert.IsNotNullOrEmpty (programText);
+			Assert.IsNotNullOrEmpty (fileName);
+
+
+			int errors = 0;
+			Program p = null;
+			errors = Parser.Parse(programText, fileName, out p, /*useBaseName=*/false);
+			Assert.AreEqual(0, errors);
+			Assert.IsNotNull(p);
+
+			// Resolve
+			errors = p.Resolve();
+			Assert.AreEqual(0, errors);
+
+			// Type check
+			errors = p.Typecheck();
+			Assert.AreEqual(0, errors);
+
+			return p;
+		}
+	}
+}
+
diff --git a/Source/UnitTests/TestUtil/Properties/AssemblyInfo.cs b/Source/UnitTests/TestUtil/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..05c9fee5
--- /dev/null
+++ b/Source/UnitTests/TestUtil/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("TestUtil")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

+[assembly: AssemblyCompany("")]

+[assembly: AssemblyProduct("TestUtil")]

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

+[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("5630b725-b802-4f97-9e46-6cdfd6819269")]

+

+// 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/UnitTests/TestUtil/TestUtil.csproj b/Source/UnitTests/TestUtil/TestUtil.csproj
new file mode 100644
index 00000000..7642b134
--- /dev/null
+++ b/Source/UnitTests/TestUtil/TestUtil.csproj
@@ -0,0 +1,71 @@
+<?xml version="1.0" encoding="utf-8"?>

+<Project ToolsVersion="12.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>{59118E35-4236-495E-AF6E-0D641302ED2C}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>TestUtil</RootNamespace>

+    <AssemblyName>TestUtil</AssemblyName>

+    <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+  </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

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

+    <DebugType>pdbonly</DebugType>

+    <Optimize>true</Optimize>

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

+    <DefineConstants>TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="nunit.framework">

+      <HintPath>..\..\packages\NUnit.2.6.3\lib\nunit.framework.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

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

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

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

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

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

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

+  </ItemGroup>

+  <ItemGroup>

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

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

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

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

+  </ItemGroup>

+  <ItemGroup>

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

+  </ItemGroup>

+  <ItemGroup>

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

+      <Project>{b230a69c-c466-4065-b9c1-84d80e76d802}</Project>

+      <Name>Core</Name>

+    </ProjectReference>

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

+      <Project>{fcd3ac7f-9dfd-46c8-ab1e-09f0b0f16dc5}</Project>

+      <Name>ParserHelper</Name>

+    </ProjectReference>

+  </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/UnitTests/TestUtil/packages.config b/Source/UnitTests/TestUtil/packages.config
new file mode 100644
index 00000000..d4e241a2
--- /dev/null
+++ b/Source/UnitTests/TestUtil/packages.config
@@ -0,0 +1,4 @@
+<?xml version="1.0" encoding="utf-8"?>

+<packages>

+  <package id="NUnit" version="2.6.3" targetFramework="net45" />

+</packages>
\ No newline at end of file