From 177aad9ff997f38056d2dc352c73b531e5822e22 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Nov 2014 18:26:06 +0000 Subject: 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. --- Source/UnitTests/CoreTests/ExprTypeChecking.cs | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'Source/UnitTests/CoreTests') 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().First().Blocks.SelectMany(c => c.Cmds).OfType().First(); + Assert.AreEqual(BasicType.Bool, assertCmd.Expr.ShallowType); + } + public FunctionCall CreateFunctionCall(string Name, Microsoft.Boogie.Type returnType, IList argTypes) { var returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", returnType), false); -- cgit v1.2.3