Add unit test to catch another bug in Boogie where FunctionCall ShallowType

is not correctly set. This is related to the bug fixed in cea703affa29. That
commit fixed the ShallowType when it was set using the constructor that takes
a Function but the parser uses the other constructor which has the same bug.

1 files changed, 21 insertions, 0 deletions

diff --git a/Source/UnitTests/CoreTests/ExprTypeChecking.cs b/Source/UnitTests/CoreTests/ExprTypeChecking.cs
index 02812151..8bd0284a 100644
--- a/Source/UnitTests/CoreTests/ExprTypeChecking.cs
+++ b/Source/UnitTests/CoreTests/ExprTypeChecking.cs
@@ -3,6 +3,7 @@ using Microsoft.Basetypes;
 using NUnit.Framework;
 using System;
 using System.Collections.Generic;
+using System.Linq;
 
 namespace CoreTests
 {
@@ -32,6 +33,26 @@ namespace CoreTests
             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);