diff options
22 files changed, 1269 insertions, 1 deletions
@@ -10,6 +10,8 @@ Source/*/bin Source/*/obj
Source/Provers/*/bin
Source/Provers/*/obj
+Source/packages/*
+Source/UnitTests/TestResult.xml
Binaries/ITaskManager.dll
Binaries/ITaskManager.pdb
Binaries/Microsoft.SpecSharp.Runtime.dll
@@ -3,6 +3,7 @@ syntax: regexp ^Source/_ReSharper\.Boogie$
^Source/.*\.(user|suo|cache|vs10x)$
^Source/Core/(Parser|Scanner).cs.old$
+^Source/packages/.*$
^Binaries/.*\.(dll|pdb|exe|manifest|config)$
^.*(bin|obj)/([^/]*/)?(Debug|Release|Checked|Debug All|DEBUG ALL)/.*$
Test/.*/Output
@@ -16,3 +17,4 @@ backup.diff *.exe.mdb
*.pidb
*.userprefs
+TestResult.xml
diff --git a/Source/.nuget/packages.config b/Source/.nuget/packages.config new file mode 100644 index 00000000..f0b15e98 --- /dev/null +++ b/Source/.nuget/packages.config @@ -0,0 +1,4 @@ +<?xml version="1.0" encoding="utf-8"?>
+<packages>
+ <package id="NUnit.Runners" version="2.6.3" />
+</packages>
\ No newline at end of file diff --git a/Source/Boogie.sln b/Source/Boogie.sln index ff116c50..aabaed90 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -1,7 +1,7 @@
Microsoft Visual Studio Solution File, Format Version 12.00
# Visual Studio 2013
-VisualStudioVersion = 12.0.21005.1
+VisualStudioVersion = 12.0.31101.0
MinimumVisualStudioVersion = 10.0.40219.1
Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758C1E3-824A-439F-AA2F-0BA1143E8C8D}"
EndProject
@@ -44,6 +44,19 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BVD", "BVD\BVD.csproj", "{8 EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "Concurrency\Concurrency.csproj", "{D07B8E38-E172-47F4-AD02-0373014A46D3}"
EndProject
+Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "UnitTests", "UnitTests", "{0C77D814-EC94-45D7-9F9B-213C425D0F15}"
+EndProject
+Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = ".nuget", ".nuget", "{83CAF6FB-75EB-422D-B341-D61E07A0FAEB}"
+ ProjectSection(SolutionItems) = preProject
+ .nuget\packages.config = .nuget\packages.config
+ EndProjectSection
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CoreTests", "UnitTests\CoreTests\CoreTests.csproj", "{961B3BCA-2067-43B2-8E43-23C4293F21B9}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TestUtil", "UnitTests\TestUtil\TestUtil.csproj", "{59118E35-4236-495E-AF6E-0D641302ED2C}"
+EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BasetypesTests", "UnitTests\BasetypesTests\BasetypesTests.csproj", "{D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}"
+EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Checked|.NET = Checked|.NET
@@ -552,11 +565,86 @@ Global {D07B8E38-E172-47F4-AD02-0373014A46D3}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
{D07B8E38-E172-47F4-AD02-0373014A46D3}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
{D07B8E38-E172-47F4-AD02-0373014A46D3}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Checked|.NET.ActiveCfg = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Checked|x86.ActiveCfg = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Release|.NET.ActiveCfg = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Release|Any CPU.Build.0 = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.Release|x86.ActiveCfg = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Checked|.NET.ActiveCfg = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Checked|x86.ActiveCfg = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Release|.NET.ActiveCfg = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Release|Any CPU.Build.0 = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.Release|x86.ActiveCfg = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {59118E35-4236-495E-AF6E-0D641302ED2C}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Checked|.NET.ActiveCfg = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Checked|Any CPU.ActiveCfg = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Checked|Any CPU.Build.0 = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Checked|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Checked|Mixed Platforms.Build.0 = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Checked|x86.ActiveCfg = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Release|.NET.ActiveCfg = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Release|Any CPU.Build.0 = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.Release|x86.ActiveCfg = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}.z3apidebug|x86.ActiveCfg = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
EndGlobalSection
GlobalSection(NestedProjects) = preSolution
{9B163AA3-36BC-4AFB-88AB-79BC9E97E401} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
+ {961B3BCA-2067-43B2-8E43-23C4293F21B9} = {0C77D814-EC94-45D7-9F9B-213C425D0F15}
+ {59118E35-4236-495E-AF6E-0D641302ED2C} = {0C77D814-EC94-45D7-9F9B-213C425D0F15}
+ {D00C3F22-1EDA-4781-8F0E-81991E9CB0D9} = {0C77D814-EC94-45D7-9F9B-213C425D0F15}
EndGlobalSection
EndGlobal
diff --git a/Source/UnitTests/BasetypesTests/BasetypesTests.csproj b/Source/UnitTests/BasetypesTests/BasetypesTests.csproj new file mode 100644 index 00000000..483c12c7 --- /dev/null +++ b/Source/UnitTests/BasetypesTests/BasetypesTests.csproj @@ -0,0 +1,69 @@ +<?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>{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..1bad6134 --- /dev/null +++ b/Source/UnitTests/CoreTests/CoreTests.csproj @@ -0,0 +1,82 @@ +<?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>{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" />
+ </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/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..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 diff --git a/Source/UnitTests/run-unittests.py b/Source/UnitTests/run-unittests.py new file mode 100644 index 00000000..be906edd --- /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:]))
|