summaryrefslogtreecommitdiff
path: root/Source/UnitTests/CoreTests/ExprTypeChecking.cs
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-11-25 18:26:06 +0000
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-11-25 18:26:06 +0000
commit177aad9ff997f38056d2dc352c73b531e5822e22 (patch)
tree5a908ff3b1f20a3e277247e5010e453e2b7ecf61 /Source/UnitTests/CoreTests/ExprTypeChecking.cs
parent072b57b44df4fd1d512cca59fa678c4f16671e31 (diff)
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.
Diffstat (limited to 'Source/UnitTests/CoreTests/ExprTypeChecking.cs')
-rw-r--r--Source/UnitTests/CoreTests/ExprTypeChecking.cs21
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);