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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
using NUnit.Framework;
using System;
using Microsoft.Boogie;
using System.Collections.Generic;
namespace CoreTests
{
[TestFixture()]
public class ExprImmutability : IErrorSink
{
public void Error(IToken tok, string msg)
{
Assert.Fail (msg);
}
[Test(), ExpectedException(typeof(InvalidOperationException))]
public void IdentifierExprName()
{
var id = new IdentifierExpr(Token.NoToken, "foo", BasicType.Bool, /*immutable=*/true);
Assert.IsTrue(id.Immutable);
id.Name = "foo2";
}
[Test(), ExpectedException(typeof(InvalidOperationException))]
public void IdentifierExprDecl()
{
var id = new IdentifierExpr(Token.NoToken, "foo", BasicType.Bool, /*immutable=*/true);
Assert.IsTrue(id.Immutable);
var typedIdent = new TypedIdent(Token.NoToken, "foo2", BasicType.Bool);
id.Decl = new GlobalVariable(Token.NoToken, typedIdent);
}
private NAryExpr GetUnTypedImmutableNAry()
{
var id = new IdentifierExpr(Token.NoToken, "foo", BasicType.Bool, /*immutable=*/true);
Assert.IsTrue(id.Immutable);
Assert.IsTrue(id.Type.IsBool);
var e = new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, BinaryOperator.Opcode.And), new List<Expr>() {
id,
id
}, /*immutable=*/true);
Assert.IsNull(e.Type);
Assert.IsTrue(e.Immutable);
return e;
}
[Test()]
public void ProtectedExprType()
{
var e = GetUnTypedImmutableNAry();
// Now Typecheck
// Even though it's immutable we allow the TypeCheck field to be set if the Expr has never been type checked
var TC = new TypecheckingContext(this);
e.Typecheck(TC);
Assert.IsNotNull(e.Type);
Assert.IsTrue(e.Type.IsBool);
}
[Test(), ExpectedException(typeof(InvalidOperationException))]
public void ProtectedExprChangeTypeFail()
{
var e = GetUnTypedImmutableNAry();
// Now Typecheck
// Even though it's immutable we allow the TypeCheck field to be set if the Expr has never been type checked
var TC = new TypecheckingContext(this);
e.Typecheck(TC);
Assert.IsNotNull(e.Type);
Assert.IsTrue(e.Type.IsBool);
// Trying to modify the Type to a different Type now should fail
e.Type = BasicType.Int;
}
[Test()]
public void ProtectedExprTypeChangeTypeSucceed()
{
var e = GetUnTypedImmutableNAry();
// Now Typecheck
// Even though it's immutable we allow the TypeCheck field to be set if the Expr has never been type checked
var TC = new TypecheckingContext(this);
e.Typecheck(TC);
Assert.IsNotNull(e.Type);
Assert.IsTrue(e.Type.IsBool);
// Trying to assign the same Type should succeed
e.Type = BasicType.Bool;
}
[Test(), ExpectedException(typeof(InvalidOperationException))]
public void ProtectedOldExpr()
{
var e = new OldExpr(Token.NoToken, Expr.True, /*immutable=*/ true);
e.Expr = Expr.False;
}
}
}
|
