diff options
| -rw-r--r-- | Source/UnitTests/CoreTests/ExprTypeChecking.cs | 21 |
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); |