Added a unit test to catch a bug in Boogie where a NAryExpr.ShallowType

fails when the Function is a FunctionCall

2 files changed, 61 insertions, 4 deletions

diff --git a/Source/UnitTests/CoreTests/CoreTests.csproj b/Source/UnitTests/CoreTests/CoreTests.csproj
index d470ca4c..76f7b985 100644
--- a/Source/UnitTests/CoreTests/CoreTests.csproj
+++ b/Source/UnitTests/CoreTests/CoreTests.csproj
@@ -46,25 +46,26 @@
     <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>

+      <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>

       <Name>Basetypes</Name>

     </ProjectReference>

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

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

+      <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

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

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

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

       <Name>ParserHelper</Name>

     </ProjectReference>

     <ProjectReference Include="..\TestUtil\TestUtil.csproj">

-      <Project>{59118e35-4236-495e-af6e-0d641302ed2c}</Project>

+      <Project>{59118E35-4236-495E-AF6E-0D641302ED2C}</Project>

       <Name>TestUtil</Name>

     </ProjectReference>

   </ItemGroup>

diff --git a/Source/UnitTests/CoreTests/ExprTypeChecking.cs b/Source/UnitTests/CoreTests/ExprTypeChecking.cs
new file mode 100644
index 00000000..02812151
--- /dev/null
+++ b/Source/UnitTests/CoreTests/ExprTypeChecking.cs
@@ -0,0 +1,56 @@
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+using NUnit.Framework;
+using System;
+using System.Collections.Generic;
+
+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);
+        }
+
+        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);
+        }
+
+    }
+}
+