summaryrefslogtreecommitdiff
path: root/Source/UnitTests
diff options
context:
space:
mode:
Diffstat (limited to 'Source/UnitTests')
-rw-r--r--Source/UnitTests/BasetypesTests/BasetypesTests.csproj69
-rw-r--r--Source/UnitTests/BasetypesTests/BigDecTests.cs29
-rw-r--r--Source/UnitTests/BasetypesTests/Properties/AssemblyInfo.cs36
-rw-r--r--Source/UnitTests/BasetypesTests/packages.config4
-rw-r--r--Source/UnitTests/CoreTests/AbsyMetadata.cs101
-rw-r--r--Source/UnitTests/CoreTests/CoreTests.csproj83
-rw-r--r--Source/UnitTests/CoreTests/Duplicator.cs258
-rw-r--r--Source/UnitTests/CoreTests/ExprEquality.cs179
-rw-r--r--Source/UnitTests/CoreTests/ExprTypeChecking.cs77
-rw-r--r--Source/UnitTests/CoreTests/Properties/AssemblyInfo.cs36
-rw-r--r--Source/UnitTests/CoreTests/packages.config4
-rw-r--r--Source/UnitTests/README.md55
-rw-r--r--Source/UnitTests/TestUtil/AssertionTextWriterTraceListener.cs27
-rw-r--r--Source/UnitTests/TestUtil/BoogieTestBase.cs24
-rw-r--r--Source/UnitTests/TestUtil/ProgramLoader.cs33
-rw-r--r--Source/UnitTests/TestUtil/Properties/AssemblyInfo.cs36
-rw-r--r--Source/UnitTests/TestUtil/TestUtil.csproj71
-rw-r--r--Source/UnitTests/TestUtil/packages.config4
-rwxr-xr-xSource/UnitTests/run-unittests.py124
19 files changed, 1250 insertions, 0 deletions
diff --git a/Source/UnitTests/BasetypesTests/BasetypesTests.csproj b/Source/UnitTests/BasetypesTests/BasetypesTests.csproj
new file mode 100644
index 00000000..a2056f95
--- /dev/null
+++ b/Source/UnitTests/BasetypesTests/BasetypesTests.csproj
@@ -0,0 +1,69 @@
+<?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>{D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>BasetypesTests</RootNamespace>
+ <AssemblyName>BasetypesTests</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.Numerics" />
+ <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="BigDecTests.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <None Include="packages.config" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\..\Basetypes\Basetypes.csproj">
+ <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>
+ <Name>Basetypes</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <ItemGroup>
+ <Service Include="{82A7F48D-3B50-4B1E-B82E-3ADA8210C358}" />
+ </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/BasetypesTests/BigDecTests.cs b/Source/UnitTests/BasetypesTests/BigDecTests.cs
new file mode 100644
index 00000000..cee80216
--- /dev/null
+++ b/Source/UnitTests/BasetypesTests/BigDecTests.cs
@@ -0,0 +1,29 @@
+using Microsoft.Basetypes;
+using NUnit.Framework;
+using System.Numerics;
+
+namespace BasetypesTests
+{
+ [TestFixture()]
+ public class BigDecTests {
+
+ [Test()]
+ public void FromStringNegative() {
+ // This tests for a Bug in Boogie that used to be present where BigDec
+ // would not parse strings with negative numbers correctly
+ //
+ // If this bug is present this test will fail when checking the mantissa
+ var v = BigDec.FromString("-1.5");
+ Assert.AreEqual(-1, v.Exponent);
+ Assert.AreEqual(new BigInteger(-15.0), v.Mantissa);
+ }
+
+ [Test()]
+ public void FromStringPositive() {
+ var v = BigDec.FromString("1.5");
+ Assert.AreEqual(-1, v.Exponent);
+ Assert.AreEqual(new BigInteger(15.0), v.Mantissa);
+ }
+ }
+}
+
diff --git a/Source/UnitTests/BasetypesTests/Properties/AssemblyInfo.cs b/Source/UnitTests/BasetypesTests/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..4ef7c05c
--- /dev/null
+++ b/Source/UnitTests/BasetypesTests/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("BasetypesTests")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("")]
+[assembly: AssemblyProduct("BasetypesTests")]
+[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("0cca79cc-3251-46d9-87c1-32bc782d9fdd")]
+
+// 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/BasetypesTests/packages.config b/Source/UnitTests/BasetypesTests/packages.config
new file mode 100644
index 00000000..d4e241a2
--- /dev/null
+++ b/Source/UnitTests/BasetypesTests/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
diff --git a/Source/UnitTests/CoreTests/AbsyMetadata.cs b/Source/UnitTests/CoreTests/AbsyMetadata.cs
new file mode 100644
index 00000000..156f38b5
--- /dev/null
+++ b/Source/UnitTests/CoreTests/AbsyMetadata.cs
@@ -0,0 +1,101 @@
+using Microsoft.Boogie;
+using NUnit.Framework;
+using System;
+
+namespace CoreTests
+{
+ [TestFixture ()]
+ public class AbsyMetadata {
+ private Absy GetAbsy() {
+ // The choice of Absy type here is arbitary
+ return new AssertCmd(Token.NoToken, Expr.True);
+ }
+
+ [Test(), ExpectedException(typeof(ArgumentOutOfRangeException))]
+ public void NoMetadata() {
+ var absy = GetAbsy();
+
+ Assert.AreEqual(0, absy.NumberedMetaDataCount);
+
+ string willFail = absy.GetMetadata<string>(0);
+ // use willFail in someway so the result is live
+ Assert.IsNotNullOrEmpty(willFail);
+ }
+
+ [Test(), ExpectedException(typeof(ArgumentOutOfRangeException))]
+ public void InvalidIndex() {
+ var absy = GetAbsy();
+
+ Assert.AreEqual(0, absy.NumberedMetaDataCount);
+ absy.SetMetadata(0, "hello");
+
+ string willFail = absy.GetMetadata<string>(1);
+ // use willFail in someway so the result is live
+ Assert.IsNotNullOrEmpty(willFail);
+ }
+
+ [Test()]
+ public void SimpleMetadata() {
+ var absy = GetAbsy();
+ Assert.AreEqual(0, absy.NumberedMetaDataCount);
+
+ var string1 = "hello";
+ var string2 = "hello2";
+ absy.SetMetadata(0, string1);
+ Assert.AreEqual(1, absy.NumberedMetaDataCount);
+ absy.SetMetadata(1, string2);
+ Assert.AreEqual(2, absy.NumberedMetaDataCount);
+
+ Assert.AreSame(string1, absy.GetMetadata<string>(0));
+ Assert.AreSame(string2, absy.GetMetadata<string>(1));
+
+ // Now try iterating over the metadata
+ int count = 0;
+ foreach (var o in absy.NumberedMetadata) {
+ Assert.AreEqual(count, o.Key);
+ Assert.IsNotNull(o.Value);
+ ++count;
+ }
+ Assert.AreEqual(2, count);
+ }
+
+ [Test(), ExpectedException(typeof(InvalidCastException))]
+ public void IncorrectType() {
+ var absy = GetAbsy();
+ Assert.AreEqual(0, absy.NumberedMetaDataCount);
+
+ var string0 = "hello world";
+ absy.SetMetadata(0, string0);
+
+ // Now try retrive wrong type
+ int wrongType = absy.GetMetadata<int>(0);
+ // use "wrongType" is someway so the variable is live
+ Assert.AreEqual(0, wrongType);
+ }
+
+ [Test()]
+ public void NullPadding() {
+ var absy = GetAbsy();
+ Assert.AreEqual(0, absy.NumberedMetaDataCount);
+
+ string foo = "foo";
+ absy.SetMetadata<string>(10, foo);
+ Assert.AreEqual(11, absy.NumberedMetaDataCount);
+
+ // Should nulls be made accessible? Right now its impossible to access
+ // them as we always throw an exception if the stored item is null
+ for (int i = 0; i <= 9 ; ++i) {
+ try {
+ absy.GetMetadata<String>(i);
+ Assert.Fail("Accesing unset metadata should of failed");
+ }
+ catch (InvalidCastException) {
+ }
+ }
+
+
+ Assert.AreSame(foo, absy.GetMetadata<String>(10));
+ }
+ }
+}
+
diff --git a/Source/UnitTests/CoreTests/CoreTests.csproj b/Source/UnitTests/CoreTests/CoreTests.csproj
new file mode 100644
index 00000000..76f7b985
--- /dev/null
+++ b/Source/UnitTests/CoreTests/CoreTests.csproj
@@ -0,0 +1,83 @@
+<?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>{961B3BCA-2067-43B2-8E43-23C4293F21B9}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>CoreTests</RootNamespace>
+ <AssemblyName>CoreTests</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="AbsyMetadata.cs" />
+ <Compile Include="Duplicator.cs" />
+ <Compile Include="ExprEquality.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ <Compile Include="ExprTypeChecking.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <None Include="packages.config" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\..\Basetypes\Basetypes.csproj">
+ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+ <Name>Basetypes</Name>
+ </ProjectReference>
+ <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>
+ <ProjectReference Include="..\TestUtil\TestUtil.csproj">
+ <Project>{59118E35-4236-495E-AF6E-0D641302ED2C}</Project>
+ <Name>TestUtil</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <ItemGroup>
+ <Service Include="{82A7F48D-3B50-4B1E-B82E-3ADA8210C358}" />
+ </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/CoreTests/Duplicator.cs b/Source/UnitTests/CoreTests/Duplicator.cs
new file mode 100644
index 00000000..978a041b
--- /dev/null
+++ b/Source/UnitTests/CoreTests/Duplicator.cs
@@ -0,0 +1,258 @@
+using Microsoft.Boogie.TestUtil;
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+using NUnit.Framework;
+using System;
+using System.Linq;
+
+
+namespace CoreTests
+{
+ [TestFixture ()]
+ public class DuplicatorTests : BoogieTestBase, IErrorSink {
+ Duplicator d;
+
+ public void Error(IToken tok, string msg) {
+ Assert.Fail(msg);
+ }
+
+ [SetUp]
+ public void Init() {
+ d = new Duplicator();
+ }
+
+ [Test()]
+ public void BVConcatExpr() {
+ var bv1_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 8);
+ var bv2_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(2), 8);
+ var A = new BvConcatExpr(Token.NoToken, bv1_8, bv2_8);
+ var B = d.Visit(A);
+
+ // The duplicator should ensure we get new BVConcatExprs
+ Assert.AreNotSame(A, B);
+ }
+
+ [Test()]
+ public void BvExtractExpr() {
+ var bv2_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(2), 8);
+ var A = new BvExtractExpr(Token.NoToken, bv2_8, 6,0);
+ var B = d.Visit(A);
+
+ // The duplicator should ensure we get new BVExtractExprs
+ Assert.AreNotSame(A, B);
+ }
+
+ [Test()]
+ public void NaryExpr() {
+ var bv1_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 8);
+ var bv2_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(2), 8);
+ var A = NAryExpr.Eq (bv1_8, bv2_8);
+ var B = d.Visit(A);
+
+ Assert.AreNotSame(A, B);
+ }
+
+ [Test()]
+ public void WholeProgram() {
+ var p = new Program();
+ var t = new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.Bool);
+ var gv = new GlobalVariable(Token.NoToken, t);
+ p.AddTopLevelDeclaration(gv);
+ string metaDataString = "This is a test";
+ p.SetMetadata(0, metaDataString);
+
+ // Now try to clone
+ var p2 = (Program) d.Visit(p);
+
+ // Check global is a copy
+ int counter = 0;
+ GlobalVariable gv2 = null;
+ foreach (var g in p2.TopLevelDeclarations)
+ {
+ ++counter;
+ Assert.IsInstanceOf<GlobalVariable>(g);
+ gv2 = g as GlobalVariable;
+ }
+ Assert.AreEqual(1, counter);
+ Assert.AreNotSame(gv, gv2);
+ Assert.AreEqual(metaDataString, p2.GetMetadata<string>(0));
+
+
+ // Check Top level declarations list is duplicated properly
+ var t2 = new TypedIdent(Token.NoToken, "bar", Microsoft.Boogie.Type.Bool);
+ var gv3 = new GlobalVariable(Token.NoToken, t2);
+ p2.AddTopLevelDeclaration(gv3);
+
+ counter = 0;
+ foreach (var g in p2.TopLevelDeclarations) {
+ ++counter;
+ Assert.IsInstanceOf<GlobalVariable>(g);
+ }
+ Assert.AreEqual(2, counter);
+
+ // The original program should still only have one global variable
+ counter = 0;
+ foreach (var g in p.TopLevelDeclarations) {
+ ++counter;
+ Assert.IsInstanceOf<GlobalVariable>(g);
+ Assert.AreSame(g, gv);
+ }
+
+ Assert.AreEqual(1, counter);
+
+ // Change Metadata in p2, this shouldn't affect p
+ string newMetaDataString = "Another test";
+ p2.SetMetadata(0, newMetaDataString);
+
+ Assert.AreNotEqual(p2.GetMetadata<string>(0), p.GetMetadata<string>(0));
+ }
+
+ [Test()]
+ public void GotoTargets() {
+ Program p = TestUtil.ProgramLoader.LoadProgramFrom(@"
+ procedure main()
+ {
+ entry:
+ assume true;
+ goto thing1, thing2;
+
+ thing1:
+ assume true;
+ assume true;
+ goto entry, thing1;
+
+ thing2:
+ assume true;
+ assume true;
+ return;
+ }
+ ");
+
+ var main = p.TopLevelDeclarations.OfType<Implementation>().Where(x => x.Name == "main").First();
+
+ // Access blocks via their labels of gotocmds
+ var oldEntryBlock = ( main.Blocks[1].TransferCmd as GotoCmd ).labelTargets[0];
+ Assert.AreEqual("entry", oldEntryBlock.Label);
+
+ var oldThing1Block = ( main.Blocks[1].TransferCmd as GotoCmd ).labelTargets[1];
+ Assert.AreEqual("thing1", oldThing1Block.Label);
+
+ var oldThing2Block = ( main.Blocks[0].TransferCmd as GotoCmd ).labelTargets[1];
+ Assert.AreEqual("thing2", oldThing2Block.Label);
+
+ // Now duplicate
+ var newProgram = (Program) d.Visit(p);
+
+ // First lets check blocks have been duplicated
+ var newMain= newProgram.TopLevelDeclarations.OfType<Implementation>().Where(x => x.Name == "main").First();
+ var newEntryBlock = newMain.Blocks[0];
+ Assert.AreEqual("entry", newEntryBlock.Label);
+ Assert.AreNotSame(newEntryBlock, oldEntryBlock);
+
+ var newThing1Block = newMain.Blocks[1];
+ Assert.AreEqual("thing1", newThing1Block.Label);
+ Assert.AreNotSame(newThing1Block, oldThing1Block);
+
+ var newThing2Block = newMain.Blocks[2];
+ Assert.AreEqual("thing2", newThing2Block.Label);
+ Assert.AreNotSame(newThing2Block, oldThing2Block);
+
+ // Now let's examine the gotos and make sure they point to the duplicated blocks.
+ var newEntryGotoCmd = newEntryBlock.TransferCmd as GotoCmd;
+ var newthing1GotoCmd = newThing1Block.TransferCmd as GotoCmd;
+
+ Assert.AreNotSame(newEntryGotoCmd.labelTargets[0], oldThing1Block);
+ Assert.AreSame(newEntryGotoCmd.labelTargets[0], newThing1Block);
+ Assert.AreNotSame(newEntryGotoCmd.labelTargets[1], oldThing2Block);
+ Assert.AreSame(newEntryGotoCmd.labelTargets[1], newThing2Block);
+
+ Assert.AreNotSame(newthing1GotoCmd.labelTargets[0], oldEntryBlock);
+ Assert.AreSame(newthing1GotoCmd.labelTargets[0], newEntryBlock);
+ Assert.AreNotSame(newthing1GotoCmd.labelTargets[1], oldThing1Block);
+ Assert.AreSame(newthing1GotoCmd.labelTargets[1], newThing1Block);
+
+ }
+
+ [Test()]
+ public void ImplementationProcedureResolving() {
+ Program p = TestUtil.ProgramLoader.LoadProgramFrom(@"
+ procedure main(a:int) returns (r:int);
+ requires a > 0;
+ ensures r > a;
+
+ implementation main(a:int) returns (r:int)
+ {
+ r:= a + 1;
+ }
+ ");
+
+ // Check resolved
+ var oldMainImpl = p.TopLevelDeclarations.OfType<Implementation>().Where(i => i.Name == "main").First();
+ var oldMainProc = p.TopLevelDeclarations.OfType<Procedure>().Where(i => i.Name == "main").First();
+ Assert.AreSame(oldMainImpl.Proc, oldMainProc);
+
+ // Now duplicate the program
+ var newProgram = (Program) d.Visit(p);
+
+ // Resolving doesn't seem to fix this.
+ var rc = new ResolutionContext(this);
+ newProgram.Resolve(rc);
+
+ // Check resolved
+ var newMainImpl = newProgram.TopLevelDeclarations.OfType<Implementation>().Where(i => i.Name == "main").First();
+ var newMainProc = newProgram.TopLevelDeclarations.OfType<Procedure>().Where(i => i.Name == "main").First();
+ Assert.AreSame(newMainImpl.Proc, newMainProc);
+ }
+
+ [Test()]
+ public void CallCmdResolving() {
+ Program p = TestUtil.ProgramLoader.LoadProgramFrom(@"
+ procedure main()
+ {
+ var x:int;
+ call x := foo();
+ call x := bar();
+ }
+
+ procedure foo() returns(r:int)
+ {
+ r := 0;
+ }
+
+ procedure bar() returns(r:int);
+ ensures r == 0;
+ ");
+
+ // Get hold of the procedures that will be used with the CallCmd
+ var oldFoo = p.TopLevelDeclarations.OfType<Procedure>().Where(i => i.Name == "foo").First();
+ var oldBar = p.TopLevelDeclarations.OfType<Procedure>().Where(i => i.Name == "bar").First();
+
+ // Get the CallCmds to foo and bar
+ var oldCmdsInMain = p.TopLevelDeclarations.OfType<Implementation>().Where(i => i.Name == "main").SelectMany(i => i.Blocks).SelectMany(b => b.Cmds);
+ var oldCallToFoo = oldCmdsInMain.OfType<CallCmd>().Where(c => c.callee == "foo").First();
+ var oldCallToBar = oldCmdsInMain.OfType<CallCmd>().Where(c => c.callee == "bar").First();
+
+ // Check the Calls
+ Assert.AreSame(oldCallToFoo.Proc, oldFoo);
+ Assert.AreSame(oldCallToBar.Proc, oldBar);
+
+ // Now duplicate the program and check that the calls are resolved correctly
+ var newProgram = (Program) d.Visit(p);
+
+ var foo = newProgram.TopLevelDeclarations.OfType<Procedure>().Where(i => i.Name == "foo").First();
+ var bar = newProgram.TopLevelDeclarations.OfType<Procedure>().Where(i => i.Name == "bar").First();
+
+ // Get the call to Foo
+ var cmdsInMain = newProgram.TopLevelDeclarations.OfType<Implementation>().Where(i => i.Name == "main").SelectMany(i => i.Blocks).SelectMany(b => b.Cmds);
+ var callToFoo = cmdsInMain.OfType<CallCmd>().Where(c => c.callee == "foo").First();
+ var callToBar = cmdsInMain.OfType<CallCmd>().Where(c => c.callee == "bar").First();
+
+ // Check the Calls
+ Assert.AreNotSame(callToFoo.Proc, oldFoo);
+ Assert.AreSame(callToFoo.Proc, foo);
+ Assert.AreNotSame(callToBar.Proc, oldBar);
+ Assert.AreSame(callToBar.Proc, bar);
+ }
+ }
+}
+
diff --git a/Source/UnitTests/CoreTests/ExprEquality.cs b/Source/UnitTests/CoreTests/ExprEquality.cs
new file mode 100644
index 00000000..6bc049f5
--- /dev/null
+++ b/Source/UnitTests/CoreTests/ExprEquality.cs
@@ -0,0 +1,179 @@
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+using NUnit.Framework;
+using System.Collections.Generic;
+using System;
+
+namespace CoreTests
+{
+ [TestFixture()]
+ public class ExprEquality {
+
+ [Test()]
+ public void LiteralBool() {
+ var constant = new LiteralExpr(Token.NoToken, false);
+ var constant2 = new LiteralExpr(Token.NoToken, false);
+
+ Assert.AreNotSame(constant, constant2); // These are different references
+
+ Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal"
+ Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+ }
+
+ [Test()]
+ public void LiteralBV() {
+ var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8;
+ var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8;
+
+ Assert.AreNotSame(constant, constant2); // These are different references
+
+ Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal"
+ Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+ }
+
+ [Test()]
+ public void LiteralInt() {
+ var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(18)); // Integer
+ var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(18)); // Integer
+
+ Assert.AreNotSame(constant, constant2); // These are different references
+
+ Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal"
+ Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+ }
+
+ [Test()]
+ public void LiteralReal() {
+ var constant = new LiteralExpr(Token.NoToken, BigDec.FromString("11.7")); // Real
+ var constant2 = new LiteralExpr(Token.NoToken, BigDec.FromString("11.7")); // Real
+
+ Assert.AreNotSame(constant, constant2); // These are different references
+
+ Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal"
+ Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+ }
+
+ [Test()]
+ public void SimpleAdd() {
+ var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(18)); // Integer
+ var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(19)); // Integer
+ var add = Expr.Add(constant, constant2);
+
+ var add2 = Expr.Add(constant, constant2);
+
+ Assert.AreNotSame(constant, constant2); // These are different references
+ Assert.AreNotSame(add, add2); // These are different references
+
+ Assert.IsTrue(add.Equals(add2)); // These are "structurally equal"
+ Assert.AreEqual(add.GetHashCode(), add2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+ }
+
+ [Test()]
+ public void SimpleIdentifierExprs() {
+ var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+ var idVar = new IdentifierExpr(Token.NoToken, variable);
+ var idVar2 = new IdentifierExpr(Token.NoToken, variable);
+
+ Assert.AreNotSame(idVar, idVar2); // These are different references
+
+ Assert.IsTrue(idVar.Equals(idVar2)); // These are "structurally equal"
+ Assert.AreEqual(idVar.GetHashCode(), idVar2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+ }
+
+ [Test()]
+ public void SimpleIdentifierVariables() {
+ var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+ var variable2 = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+ var idVar = new IdentifierExpr(Token.NoToken, variable);
+ var idVar2 = new IdentifierExpr(Token.NoToken, variable2);
+
+ Assert.AreNotSame(idVar, idVar2); // These are different references
+ // These are not "structurally equal" because the Variable references are different (even though they have the same name and type)
+ Assert.IsFalse(idVar.Equals(idVar2));
+ }
+
+ [Test()]
+ public void SimpleBVConcat() {
+ var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+ var id = new IdentifierExpr(Token.NoToken, variable);
+ var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8;
+ var concat = new BvConcatExpr(Token.NoToken, id, constant);
+
+ // Don't trust the Boogie duplicator here. Do it ourselves
+ var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8;
+ // We don't duplicate the variable because that is not an Expr and we require reference equality.
+ var id2 = new IdentifierExpr(Token.NoToken, variable);
+ var concat2 = new BvConcatExpr(Token.NoToken, id2, constant2);
+
+ Assert.AreNotSame(concat, concat2); // These are different references
+
+ Assert.IsTrue(concat.Equals(concat2)); // These are "structurally equal"
+ Assert.AreEqual(concat.GetHashCode(), concat2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+ }
+
+ [Test()]
+ public void SimpleBVExtract() {
+ var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+ var id = new IdentifierExpr(Token.NoToken, variable);
+
+ var extract = new BvExtractExpr(Token.NoToken, id, 5, 0); // 4-bits
+
+ var id2 = new IdentifierExpr(Token.NoToken, variable);
+ var extract2 = new BvExtractExpr(Token.NoToken, id2, 5, 0);
+
+ Assert.AreNotSame(extract, extract2);
+
+ Assert.IsTrue(extract.Equals(extract2));
+ Assert.AreEqual(extract.GetHashCode(), extract2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+ }
+
+ [Test()]
+ public void SimpleForAll() {
+ var boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,"foo",Microsoft.Boogie.Type.Bool));
+ var id = new IdentifierExpr(Token.NoToken, boundVar);
+ var forall = new ForallExpr(Token.NoToken, new List<Variable>() { boundVar }, id);
+
+ var id2 = new IdentifierExpr(Token.NoToken, boundVar);
+ var forall2 = new ForallExpr(Token.NoToken, new List<Variable>() { boundVar }, id2);
+
+ Assert.AreNotSame(forall, forall2); // These are different references
+
+ Assert.IsTrue(forall.Equals(forall2)); // These are "structurally equal"
+ Assert.AreEqual(forall.GetHashCode(), forall2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+ }
+
+
+ [Test()]
+ public void SimpleExists() {
+ var boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,"foo",Microsoft.Boogie.Type.Bool));
+ var id = new IdentifierExpr(Token.NoToken, boundVar);
+ var exists = new ExistsExpr(Token.NoToken, new List<Variable>() { boundVar }, id);
+
+ var id2 = new IdentifierExpr(Token.NoToken, boundVar);
+ var exists2 = new ExistsExpr(Token.NoToken, new List<Variable>() { boundVar }, id2);
+
+ Assert.AreNotSame(exists, exists2); // These are different references
+
+ Assert.IsTrue(exists.Equals(exists2)); // These are "structurally equal"
+ Assert.AreEqual(exists.GetHashCode(), exists2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+ }
+
+ [Test()]
+ public void SimpleLambda() {
+ var boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,"foo",Microsoft.Boogie.Type.Bool));
+ var id = new IdentifierExpr(Token.NoToken, boundVar);
+
+ // This is basically an Identity Map
+ var lambdaExpr = new LambdaExpr(Token.NoToken, new List<TypeVariable>() , new List<Variable>() { boundVar }, null, id);
+
+ var id2 = new IdentifierExpr(Token.NoToken, boundVar);
+ var lambdaExpr2 = new LambdaExpr(Token.NoToken, new List<TypeVariable>() , new List<Variable>() { boundVar }, null, id2);
+
+ Assert.AreNotSame(lambdaExpr, lambdaExpr2); // These are different references
+
+ Assert.IsTrue(lambdaExpr.Equals(lambdaExpr2)); // These are "structurally equal"
+ Assert.AreEqual(lambdaExpr.GetHashCode(), lambdaExpr2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+ }
+ }
+}
+
diff --git a/Source/UnitTests/CoreTests/ExprTypeChecking.cs b/Source/UnitTests/CoreTests/ExprTypeChecking.cs
new file mode 100644
index 00000000..8bd0284a
--- /dev/null
+++ b/Source/UnitTests/CoreTests/ExprTypeChecking.cs
@@ -0,0 +1,77 @@
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+using NUnit.Framework;
+using System;
+using System.Collections.Generic;
+using System.Linq;
+
+namespace CoreTests
+{
+ [TestFixture()]
+ public class ExprTypeChecking : IErrorSink
+ {
+ [Test()]
+ public void FunctionCall()
+ {
+ var fc = CreateFunctionCall("bv8slt", Microsoft.Boogie.Type.Bool, new List<Microsoft.Boogie.Type>() {
+ BasicType.GetBvType(8),
+ BasicType.GetBvType(8)
+ });
+
+ var constantBv = new LiteralExpr(Token.NoToken, BigNum.FromInt(0) , 8);
+ var nary = new NAryExpr(Token.NoToken,fc, new List<Expr>() { constantBv, constantBv} );
+
+ // Get shallow type (this was broken when this test was written)
+ Assert.AreEqual(BasicType.Bool, nary.ShallowType);
+
+ // Deep type check (this was not broken before writing this test)
+ Assert.IsNull(nary.Type);
+
+ var tc = new TypecheckingContext(this);
+ nary.Typecheck(tc);
+
+ Assert.AreEqual(BasicType.Bool, nary.Type);
+ }
+
+ [Test()]
+ public void FunctionCallTypeResolved()
+ {
+ // This test case requires that function calls have been resolved
+ // correctly and that the ShallowType is correct.
+ // It's simpler to let the parser and resolver do all the work here
+ // than try to build all the objects manually.
+ var program = TestUtil.ProgramLoader.LoadProgramFrom(@"
+ function {:bvbuiltin ""bvugt""} bv8ugt(bv8,bv8) returns(bool);
+
+ procedure main(a:bv8)
+ {
+ assert bv8ugt(a, 2bv8);
+ }
+ ", "file.bpl");
+
+ var assertCmd = program.TopLevelDeclarations.OfType<Implementation>().First().Blocks.SelectMany(c => c.Cmds).OfType<AssertCmd>().First();
+ Assert.AreEqual(BasicType.Bool, assertCmd.Expr.ShallowType);
+ }
+
+ public FunctionCall CreateFunctionCall(string Name, Microsoft.Boogie.Type returnType, IList<Microsoft.Boogie.Type> argTypes)
+ {
+ var returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", returnType), false);
+ var vars = new List<Variable>();
+ foreach (var T in argTypes)
+ {
+ vars.Add( new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "",T), true));
+ }
+
+ // Finally build the function and the function call
+ var funcCall = new FunctionCall(new Function(Token.NoToken, Name, vars, returnVar));
+ return funcCall;
+ }
+
+ public void Error(IToken tok, string msg)
+ {
+ Assert.Fail(msg);
+ }
+
+ }
+}
+
diff --git a/Source/UnitTests/CoreTests/Properties/AssemblyInfo.cs b/Source/UnitTests/CoreTests/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..fb965517
--- /dev/null
+++ b/Source/UnitTests/CoreTests/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("CoreTests")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("")]
+[assembly: AssemblyProduct("CoreTests")]
+[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("5c6f8617-e212-4ab7-bce6-5b1a930fa2b8")]
+
+// 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/CoreTests/packages.config b/Source/UnitTests/CoreTests/packages.config
new file mode 100644
index 00000000..d4e241a2
--- /dev/null
+++ b/Source/UnitTests/CoreTests/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
diff --git a/Source/UnitTests/README.md b/Source/UnitTests/README.md
new file mode 100644
index 00000000..5e70bc18
--- /dev/null
+++ b/Source/UnitTests/README.md
@@ -0,0 +1,55 @@
+Unit testing infrastructure
+===========================
+
+Boogie uses [NUnit](http://www.nunit.org/) unit test framework.
+We currently use NUnit 2.6.3, which was the latest stable
+version available at the time of writing.
+
+
+Installing NUnit
+================
+
+NUnit should be installed via [NuGet](https://www.nuget.org/) package manager.
+
+The NuGet client is available as
+
+* An extension to Visual Studio
+* An add-in in Monodevelop
+* A command line utility from the NuGet website
+
+Note Mono ships with an old version of NUnit (2.4.8) which will cause
+compilation issues. To fix this you must install NUnit via NuGet.
+
+
+Running the tests
+=================
+
+Command line
+------------
+
+The ``run-unittests.py`` python script in the root directory of the project can be used to run the unit tests on the command line. This script is a simple wrapper for ``nunit-console.exe``.
+
+```
+$ python run-unittests.py Release
+```
+
+Run the following to see all the available options
+
+```
+$ python run-unittests.py --help
+```
+
+Monodevelop
+-----------
+
+Monodevelop has built in support for running NUnit tests. Goto the "Unit Tests"
+panel and click "Run All".
+
+Visual Studio
+-------------
+
+Visual studio needs the "NUnit Test Adapter for VS2012 and VS2013" add-in to be installed (Tools > Extensions and Updates). Once that is installed you can run unit tests by going
+
+1. Going to the Test Explorer (TEST > Windows > Test Explorer)
+2. Clicking on "Run All" in the Test Explorer.
+
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..b5d620a8
--- /dev/null
+++ b/Source/UnitTests/TestUtil/TestUtil.csproj
@@ -0,0 +1,71 @@
+<?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>{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
diff --git a/Source/UnitTests/run-unittests.py b/Source/UnitTests/run-unittests.py
new file mode 100755
index 00000000..29033943
--- /dev/null
+++ b/Source/UnitTests/run-unittests.py
@@ -0,0 +1,124 @@
+#!/usr/bin/env python
+"""
+This is a simple script to invoke nunit-console.exe
+on Windows or Linux on all UnitTest libraries.
+"""
+import argparse
+import logging
+import os
+import subprocess
+import sys
+
+class ReturnCode:
+ SUCCESS = 0
+ CONFIG_ERROR = 1
+ RUN_ERROR = 2
+
+
+def main(args):
+ parser = argparse.ArgumentParser(description=__doc__)
+ parser.add_argument('BuildType', choices=['Release', 'Debug'],
+ help='Build type of unit test libraries')
+ parser.add_argument('-l','--log-level',
+ choices=['critical', 'error', 'warning', 'info', 'debug'],
+ default='info',
+ dest='log_level',
+ help='Logging level. Default %(default)s')
+ parser.add_argument('--nunit-console-path', default='',
+ help='Path to nunit-console tool. If not set the script will try to guess its location',
+ dest='nunit_console_path'
+ )
+ parser.add_argument('-e', '--nunit-console-extra-args', action='append',
+ help='Pass extra arguments to nunit-console. This can be used multiple times',
+ default=[],
+ dest='nunit_console_extra_args'
+ )
+ parser.add_argument('--no-progress',
+ action='store_true',
+ dest='no_progress',
+ help='Suppress nunit-console progress information')
+
+
+ parsedArgs = parser.parse_args(args)
+ logging.basicConfig(level=getattr(logging, parsedArgs.log_level.upper()))
+ buildType=parsedArgs.BuildType
+
+ logging.info('Build type is {}'.format(buildType))
+
+ if parsedArgs.no_progress:
+ parsedArgs.nunit_console_extra_args.append('-nodots')
+
+ logging.info('Extra arguments to nunit-console "{}"'.format(parsedArgs.nunit_console_extra_args))
+
+ UnitTestDirRoot = os.path.dirname(os.path.abspath(__file__))
+
+ # Find nunit-console.exe
+ if parsedArgs.nunit_console_path == "":
+ # Try to guess where the tool is
+ nunitConsolePath = os.path.join(os.path.join(UnitTestDirRoot,'..'),
+ "packages",
+ "NUnit.Runners.2.6.3",
+ "tools",
+ "nunit-console.exe"
+ )
+ # Mono needs the path to be absolute
+ nunitConsolePath = os.path.abspath(nunitConsolePath)
+ else:
+ nunitConsolePath = parsedArgs.nunit_console_path
+
+ logging.info('Looking for NUnit console at "{}"'.format(nunitConsolePath))
+ if not os.path.exists(nunitConsolePath):
+ logging.error('Could not find NUnit console tool')
+ return ReturnCode.CONFIG_ERROR
+
+ # Find unit test libraries
+ unitTestLibraries = [ ]
+ logging.info('Searching for Unit test libraries in "{}"'.format(UnitTestDirRoot))
+ for (dirpath, dirnames, filenames) in os.walk(UnitTestDirRoot):
+
+ # Search current directory for dll with correct suffix
+ for filename in filenames:
+ if filename.endswith('Tests.dll'):
+ logging.debug('Found "{}" checking build type'.format(filename))
+
+ pathComponents = dirpath.split(os.path.sep)
+ fullPath = os.path.join(dirpath, filename)
+ try:
+ buildTypeIndex = pathComponents.index(buildType)
+ if buildTypeIndex == 0 or pathComponents[buildTypeIndex -1] != 'bin':
+ continue
+
+ logging.info('Using "{}"'.format(fullPath))
+ unitTestLibraries.append(fullPath)
+ except ValueError:
+ pass
+
+ # Run Unit tests
+ if len(unitTestLibraries) == 0:
+ logging.error('No Unit test libraries were found')
+ return ReturnCode.CONFIG_ERROR
+
+ cmd = []
+
+ if os.name == 'posix':
+ cmd.append('mono')
+
+ cmd.extend([nunitConsolePath, '-nologo'])
+
+ if len(parsedArgs.nunit_console_extra_args) > 0:
+ cmd.extend(parsedArgs.nunit_console_extra_args)
+
+ cmd.extend(unitTestLibraries)
+ logging.info('Running "{}"'.format(cmd))
+ exitCode = subprocess.call(cmd)
+ if exitCode != 0:
+ logging.error('FAILED!')
+ return ReturnCode.RUN_ERROR
+ else:
+ logging.info('Succeeded')
+
+ return ReturnCode.SUCCESS
+
+
+if __name__ == '__main__':
+ sys.exit(main(sys.argv[1:]))
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-09 13:46:40 +0000