1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
using Microsoft.Boogie;
using Microsoft.Basetypes;
using NUnit.Framework;
using System;
using System.Collections.Generic;
using System.Linq;
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);
}
[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);
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);
}
}
}
|
