diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-11-17 20:58:26 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-11-17 20:58:26 +0000 |
commit | 8e5671a4763542c767a8bdba4b6ea41a2ad7691f (patch) | |
tree | 2bf38d77e7b39dbfe009239e6c13baab54b80238 /Source/UnitTests/CoreTests | |
parent | c7a2a70a879e2506f6470e0abab2e03b1b60408a (diff) |
Introduce unit tests which use NUnit. NUnit is now a dependency
so developers need to install it via NuGet.
There aren't many tests yet. Just a few for Core and Basetypes but
hopefully more will be added in the future.
More information can be found in Source/UnitTests/README.md
Diffstat (limited to 'Source/UnitTests/CoreTests')
-rw-r--r-- | Source/UnitTests/CoreTests/AbsyMetadata.cs | 101 | ||||
-rw-r--r-- | Source/UnitTests/CoreTests/CoreTests.csproj | 82 | ||||
-rw-r--r-- | Source/UnitTests/CoreTests/Duplicator.cs | 258 | ||||
-rw-r--r-- | Source/UnitTests/CoreTests/ExprEquality.cs | 179 | ||||
-rw-r--r-- | Source/UnitTests/CoreTests/Properties/AssemblyInfo.cs | 36 | ||||
-rw-r--r-- | Source/UnitTests/CoreTests/packages.config | 4 |
6 files changed, 660 insertions, 0 deletions
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 |