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
|
using Microsoft.Boogie;
using Microsoft.Basetypes;
using NUnit.Framework;
using System;
using System.Collections.Generic;
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);
}
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);
}
}
}
|
