Initial set of files.

16 files changed, 1008 insertions, 0 deletions

diff --git a/Test/test1/Answer b/Test/test1/Answer
new file mode 100644
index 00000000..b0f4aac3
--- /dev/null
+++ b/Test/test1/Answer
@@ -0,0 +1,137 @@
+Frame0.bpl(10,11): Error: undeclared identifier: a

+Frame0.bpl(12,11): Error: undeclared identifier: b

+2 name resolution errors detected in Frame0.bpl

+Frame1.bpl(16,7): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

+Frame1.bpl(17,6): Error: command assigns to an immutable variable: a

+Frame1.bpl(22,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

+Frame1.bpl(23,4): Error: command assigns to an immutable variable: a

+Frame1.bpl(27,12): Error: command assigns to an immutable variable: hh

+Frame1.bpl(28,12): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(30,7): Error: command assigns to an immutable variable: hh

+Frame1.bpl(31,7): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(33,4): Error: command assigns to an immutable variable: hh

+Frame1.bpl(34,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(55,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g0

+Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g0

+Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

+Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(84,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x

+Frame1.bpl(89,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x (named y in implementation)

+16 type checking errors detected in Frame1.bpl

+

+Boogie program verifier finished with 0 verified, 0 errors

+Arrays.bpl(15,14): Error: wrong number of arguments in map select: 2 instead of 1

+Arrays.bpl(16,14): Error: wrong number of arguments in map select: 1 instead of 2

+Arrays.bpl(20,7): Error: wrong number of arguments in map assignment: 2 instead of 1

+Arrays.bpl(21,7): Error: wrong number of arguments in map assignment: 1 instead of 2

+Arrays.bpl(41,13): Error: invalid type for argument 0 in map select: bool (expected: int)

+Arrays.bpl(42,16): Error: invalid argument types (bool and int) to binary operator ==

+Arrays.bpl(43,13): Error: invalid type for argument 0 in map select: int (expected: bool)

+Arrays.bpl(43,15): Error: invalid type for argument 1 in map select: int (expected: ref)

+Arrays.bpl(44,15): Error: invalid type for argument 1 in map select: bool (expected: ref)

+Arrays.bpl(44,23): Error: invalid type for argument 0 in map select: ref (expected: bool)

+Arrays.bpl(45,13): Error: invalid type for argument 0 in map select: ref (expected: bool)

+Arrays.bpl(45,18): Error: invalid type for argument 1 in map select: int (expected: ref)

+Arrays.bpl(45,2): Error: preconditions must be of type bool

+Arrays.bpl(46,13): Error: invalid type for argument 0 in map select: int (expected: bool)

+Arrays.bpl(46,15): Error: invalid type for argument 1 in map select: int (expected: ref)

+Arrays.bpl(50,6): Error: invalid type for argument 0 in map assignment: bool (expected: int)

+Arrays.bpl(51,6): Error: invalid type for argument 0 in map assignment: int (expected: bool)

+Arrays.bpl(51,8): Error: invalid type for argument 1 in map assignment: int (expected: ref)

+Arrays.bpl(51,5): Error: mismatched types in assignment command (cannot assign ref to int)

+Arrays.bpl(52,7): Error: invalid type for argument 0 in map assignment: bool (expected: int)

+Arrays.bpl(52,5): Error: mismatched types in assignment command (cannot assign int to bool)

+Arrays.bpl(53,12): Error: invalid type for argument 1 in map assignment: bool (expected: ref)

+Arrays.bpl(113,11): Error: invalid type for argument 0 in map select: name (expected: [int,int]bool)

+Arrays.bpl(114,4): Error: mismatched types in assignment command (cannot assign [int,int]bool to [[int,int]bool,[name]name]int)

+Arrays.bpl(115,4): Error: mismatched types in assignment command (cannot assign name to [int,int]bool)

+Arrays.bpl(116,5): Error: mismatched types in assignment command (cannot assign name to bool)

+Arrays.bpl(117,8): Error: invalid type for argument 1 in map assignment: name (expected: [name]name)

+Arrays.bpl(118,4): Error: mismatched types in assignment command (cannot assign [int,int][int]int to [[int,int]bool,[name]name]int)

+Arrays.bpl(123,10): Error: wrong number of arguments in map select: 1 instead of 2

+Arrays.bpl(124,14): Error: wrong number of arguments in map select: 1 instead of 2

+Arrays.bpl(125,6): Error: invalid type for argument 0 in map assignment: bool (expected: int)

+Arrays.bpl(126,4): Error: mismatched types in assignment command (cannot assign [int,int][int]int to [int,int][name]int)

+Arrays.bpl(127,4): Error: mismatched types in assignment command (cannot assign [int,int][name]int to [int,int][int]int)

+Arrays.bpl(130,21): Error: wrong number of arguments in map select: 2 instead of 1

+Arrays.bpl(131,5): Error: wrong number of arguments in map assignment: 2 instead of 1

+Arrays.bpl(132,13): Error: wrong number of arguments in map select: 2 instead of 1

+Arrays.bpl(133,17): Error: wrong number of arguments in map select: 1 instead of 2

+Arrays.bpl(134,14): Error: wrong number of arguments in map select: 2 instead of 1

+Arrays.bpl(166,12): Error: invalid type for argument 0 in application of Sf: [int,int]bool (expected: any)

+Arrays.bpl(176,4): Error: mismatched types in assignment command (cannot assign [int,int]bool to <a>[int,a]bool)

+Arrays.bpl(177,4): Error: mismatched types in assignment command (cannot assign <a>[int,a]bool to [int,int]bool)

+Arrays.bpl(178,4): Error: mismatched types in assignment command (cannot assign [any,any]bool to <a>[int,a]bool)

+Arrays.bpl(179,4): Error: mismatched types in assignment command (cannot assign <a>[int,a]bool to [any,any]bool)

+Arrays.bpl(180,4): Error: mismatched types in assignment command (cannot assign [ref]bool to [any]bool)

+Arrays.bpl(191,18): Error: invalid type for argument 0 in map select: any (expected: int)

+Arrays.bpl(198,11): Error: invalid type for argument 0 in map assignment: any (expected: int)

+Arrays.bpl(214,24): Error: invalid type for argument 0 in call to IntMethod: int (expected: any)

+Arrays.bpl(214,9): Error: invalid type for out-parameter 0 in call to IntMethod: any (expected: int)

+Arrays.bpl(215,4): Error: mismatched types in assignment command (cannot assign int to any)

+Arrays.bpl(216,4): Error: mismatched types in assignment command (cannot assign any to int)

+Arrays.bpl(218,24): Error: invalid type for argument 0 in call to AnyMethod: any (expected: int)

+Arrays.bpl(218,9): Error: invalid type for out-parameter 0 in call to AnyMethod: int (expected: any)

+52 type checking errors detected in Arrays.bpl

+WhereTyping.bpl(25,34): Error: invalid argument types (double and int) to binary operator +

+WhereTyping.bpl(26,12): Error: where clauses must be of type bool

+WhereTyping.bpl(36,22): Error: invalid argument types (name and int) to binary operator !=

+WhereTyping.bpl(41,30): Error: invalid argument types (name and int) to binary operator ==

+4 type checking errors detected in WhereTyping.bpl

+Family.bpl(30,4): Error: mismatched types in assignment command (cannot assign int to bool)

+Family.bpl(31,8): Error: mismatched types in assignment command (cannot assign bool to int)

+Family.bpl(33,8): Error: mismatched types in assignment command (cannot assign int to y)

+Family.bpl(34,15): Error: invalid type for argument 1 in map assignment: any (expected: Field x)

+Family.bpl(35,15): Error: invalid type for argument 1 in map assignment: any (expected: Field x)

+Family.bpl(37,8): Error: mismatched types in assignment command (cannot assign bool to any)

+Family.bpl(38,8): Error: mismatched types in assignment command (cannot assign Field any to any)

+Family.bpl(39,8): Error: mismatched types in assignment command (cannot assign Field y to any)

+8 type checking errors detected in Family.bpl

+AttributeTyping.bpl(3,23): Error: ++ operands need to be bitvectors (got int, int)

+AttributeTyping.bpl(5,29): Error: invalid type for argument 0 in application of F0: bool (expected: int)

+AttributeTyping.bpl(7,26): Error: invalid type for argument 0 in application of F0: bool (expected: int)

+AttributeTyping.bpl(9,21): Error: invalid argument types (int and int) to binary operator &&

+AttributeTyping.bpl(11,22): Error: invalid argument type (int) to unary operator !

+AttributeTyping.bpl(13,32): Error: invalid argument types (int and int) to binary operator ==>

+6 type checking errors detected in AttributeTyping.bpl

+UpdateExprTyping.bpl(3,11): Error: invalid argument types ([int]bool and [int]ref) to binary operator ==

+UpdateExprTyping.bpl(4,11): Error: invalid argument types ([int]bool and [bool]bool) to binary operator ==

+UpdateExprTyping.bpl(7,16): Error: invalid type for argument 0 in map store: bool (expected: int)

+UpdateExprTyping.bpl(8,21): Error: right-hand side in map store with wrong type: int (expected: bool)

+UpdateExprTyping.bpl(9,11): Error: invalid argument types ([int]bool and [int]ref) to binary operator ==

+UpdateExprTyping.bpl(15,18): Error: invalid type for argument 0 in map store: ref (expected: int)

+UpdateExprTyping.bpl(16,20): Error: invalid type for argument 1 in map store: bool (expected: ref)

+UpdateExprTyping.bpl(17,28): Error: right-hand side in map store with wrong type: ref (expected: bool)

+UpdateExprTyping.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to any)

+UpdateExprTyping.bpl(36,28): Error: right-hand side in map store with wrong type: ref (expected: any)

+UpdateExprTyping.bpl(38,27): Error: right-hand side in map store with wrong type: ref (expected: int)

+UpdateExprTyping.bpl(39,27): Error: right-hand side in map store with wrong type: int (expected: ref)

+12 type checking errors detected in UpdateExprTyping.bpl

+CallForallResolve.bpl(15,2): Error: call forall is allowed only on procedures with no modifies clause: Q

+1 type checking errors detected in CallForallResolve.bpl

+MapsTypeErrors.bpl(26,6): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: m

+MapsTypeErrors.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to []int)

+MapsTypeErrors.bpl(33,3): Error: mismatched types in assignment command (cannot assign []int to int)

+MapsTypeErrors.bpl(39,3): Error: mismatched types in assignment command (cannot assign bool to int)

+MapsTypeErrors.bpl(67,14): Error: invalid argument types (Field int and Field bool) to binary operator ==

+MapsTypeErrors.bpl(70,27): Error: invalid type for argument 1 in application of StrictEqual: Field bool (expected: a)

+MapsTypeErrors.bpl(75,33): Error: invalid type for argument 1 in application of StrictEqual: Field int (expected: a)

+MapsTypeErrors.bpl(77,31): Error: invalid type for argument 1 in application of IntEqual: Field alpha (expected: Field int)

+MapsTypeErrors.bpl(90,8): Error: extract operand must be a bitvector of at least 32 bits (got bv31)

+MapsTypeErrors.bpl(91,8): Error: extract operand must be a bitvector of at least 32 bits (got int)

+MapsTypeErrors.bpl(95,2): Error: mismatched types in assignment command (cannot assign bv33 to bv32)

+MapsTypeErrors.bpl(104,2): Error: mismatched types in assignment command (cannot assign bv20 to bv32)

+MapsTypeErrors.bpl(110,56): Error: invalid type for argument 1 in application of Same: bv18 (expected: T)

+MapsTypeErrors.bpl(120,4): Error: mismatched types in assignment command (cannot assign [?, ?]? to [int,int]bool)

+MapsTypeErrors.bpl(122,4): Error: mismatched types in assignment command (cannot assign [?, ?]? to HeapType)

+15 type checking errors detected in MapsTypeErrors.bpl

+Orderings.bpl(6,19): Error: parent of constant has incompatible type (int instead of C)

+1 type checking errors detected in Orderings.bpl

+EmptyCallArgs.bpl(15,17): Error: invalid type for argument 0 in call to P: int (expected: bool)

+EmptyCallArgs.bpl(26,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)

+EmptyCallArgs.bpl(28,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)

+3 type checking errors detected in EmptyCallArgs.bpl

+FunBody.bpl(6,45): Error: function body with invalid type: bool (expected: int)

+FunBody.bpl(8,61): Error: function body with invalid type: int (expected: alpha)

+FunBody.bpl(10,58): Error: function body with invalid type: int (expected: alpha)

+3 type checking errors detected in FunBody.bpl

diff --git a/Test/test1/Arrays.bpl b/Test/test1/Arrays.bpl
new file mode 100644
index 00000000..85ee783b
--- /dev/null
+++ b/Test/test1/Arrays.bpl
@@ -0,0 +1,224 @@
+var one: [int]int;

+var two: [int, int]int;

+

+procedure Good0(x: int, y: int)

+  requires one[x] == two[x,y];

+  modifies one, two;

+{

+  start:

+    one[x] := two[x,y];

+    two[x,y] := one[x];

+    return;

+}

+

+procedure Bad0(x: int, y: int)

+  requires one[x,y] == 7;

+  requires two[x] == 8;

+  modifies one, two;

+{

+  start:

+    one[x,y] := 10;

+    two[x] := 11;

+    return;

+}

+

+var A: [int]bool;

+var B: [bool, ref]int;

+

+procedure Good1(x: int, b: bool, o: ref)

+  requires A[x] && B[b,o] == 18;

+  modifies A, B;

+{

+  start:

+    A[x] := true;

+    B[b,o] := 19;

+    A[100] := false;

+    B[false,null] := 70;

+    return;

+}

+

+procedure Bad1(x: int, b: bool, o: ref)

+  requires A[b];

+  requires A[x] == 7;

+  requires B[x,x] < 12;

+  requires B[b,b] == B[o,o];

+  requires B[null,5];

+  requires B[7,7] == A[7];

+  modifies A, B;

+{

+  start:

+    A[b] := true;

+    B[3,14] := null;

+    A[A[x]] := 9;

+    B[false,false] := 70;

+    return;

+}

+

+var M: [ [int,int]bool, [name]name ]int;

+var Q: [int,int][int]int;

+var R: [int][int,int]int;

+

+procedure Good2(k: [int,int]bool, l: [name]name) returns (n: int)

+  modifies M, Q, R;

+{

+  var m: [ [int,int]bool, [name]name ]int;

+  var p: [int,int]bool;

+  var q: [int]int;

+  var qq: [int,int][int]int;

+  var r: [int,int]int;

+

+  start:

+    n := M[k,l];

+    m := M;

+    p := k;

+    p[5,8] := true;

+    m[p,l] := 13;

+    M := m;

+    goto next;

+

+  next:

+    qq := Q;

+    q := Q[13,21];

+    n := n + Q[34,55][89];

+    R[1] := R[2];

+    n := n + R[1][2,3];

+    Q[144,233] := q;

+    goto deepUpdate;

+

+  deepUpdate:

+    // To effectively do:

+    //     Q[5,8][13] := 21;

+    // do:

+    q := Q[5,8];

+    q[13] := 21;

+    Q[5,8] := q;

+    return;

+}

+

+const Sven: name;

+const Mia: name;

+const Tryggve: name;

+const Gunnel: name;

+

+procedure Bad2(k: [int,int]bool, l: [name]name) returns (n: int)

+  modifies M, Q, R;

+{

+  var m: [ [int,int]bool, [name]name ]int;

+  var p: [int,int]bool;

+  var q: [int]int;

+  var qq: [int,int][int]int;

+  var qqx: [int,int][name]int;

+

+  start:

+    n := M[Sven,l];

+    m := p;

+    p := l[Mia];

+    p[5,8] := Tryggve;

+    m[p,Gunnel] := 13;

+    M := qq;

+    goto next;

+

+  next:

+    qq := Q;  // okay

+    q := Q[13];

+    n := n - Q[89][34,55];

+    Q[true,233] := q;

+    qqx := qq;

+    Q := qqx;

+    qqx := qqx;  // okay

+    Q := Q;  // okay

+    n := n + Q[34,55][144,169];

+    R[1,2] := 0;

+    R[1] := R[2,3];

+    n := n + R[1][2];

+    n := n + R[1,2];

+    return;

+}

+

+type MyType;

+var S0: bool;

+var S1: [ref]bool;

+var S2: [ref,int]bool;

+var S3: [[ref,int]bool,MyType]MyType;

+var S4: <a>[int,a]bool;

+var S5: [int,int]bool;

+var S6: [any,any]bool;

+var S7: [int,any]any;

+var S8: [any]bool;

+

+function Sf(any) returns (bool);

+

+procedure SubtypesGood(a: any)

+  modifies S0;

+{

+  var t: MyType;

+  var b: bool;

+

+  start:

+    S0 := S1[null];  // bool := bool

+    S0 := S2[null,0];  // bool := bool

+    t := S3[S2,t];

+    goto next;

+  next:

+    b := S4[4,a];

+    b := S4[5,null];  // any := ref

+    b := S4[6,S4];  // any := [int,any]bool

+    b := Sf(S5);

+    return;

+}

+

+procedure SubtypesBad()

+  modifies S4,S5,S6;

+  modifies S8;

+{

+  start:

+    S4 := S4;

+    S4 := S5;  // no

+    S5 := S4;  // no

+    S4 := S6;  // no

+    S6 := S4;  // no

+    S8 := S1;  // no

+    return;

+}

+

+// ----------------------------------------------------

+

+var ArrayA: [int]bool;

+var ArrayB: <a>[a]bool;

+

+procedure ArrayP(x: int, y: any)

+  requires ArrayA[x];

+  requires ArrayA[y];  // error

+  requires ArrayB[x];

+  requires ArrayB[y];

+  modifies ArrayA, ArrayB;

+{

+  start:

+    ArrayA[x] := true;

+    ArrayA[y] := true;  // error

+    ArrayB[x] := true;

+    ArrayB[y] := true;

+    return;

+}

+

+// ----------------------------------------------------

+

+procedure IntMethod(p: any) returns (r: int);

+procedure AnyMethod(p: int) returns (r: any);

+

+procedure IntMethodCaller()

+{

+  var x: any, y: int;

+  entry:

+    call x := AnyMethod(y);  // types are exact

+    call x := IntMethod(y);  // error: type mismatch for out-parameter

+    x := y;

+    y := x;  // error: cannot assign any to int

+    call y := IntMethod(x);  // types are exact

+    call y := AnyMethod(x);  // type error on both in-parameter and out-parameter

+    return;

+}

+

+

+type ref, any, name;

+const null : ref;

diff --git a/Test/test1/AttributeTyping.bpl b/Test/test1/AttributeTyping.bpl
new file mode 100644
index 00000000..204ac2ac
--- /dev/null
+++ b/Test/test1/AttributeTyping.bpl
@@ -0,0 +1,36 @@
+

+

+const {:Incorrect pux0 ++ F0(pux1)} pux0: int;

+

+function {:Incorrect F0(pux0 < 0) + pux1} F0(int) returns (int);

+

+axiom {:Incorrect F0(pux0 == pux1)} true;

+

+var {:Incorrect pux0 && pux1} pux1: int;

+

+procedure {:Incorrect !(pux0 - pux1)} P();

+

+implementation {:Incorrect pux0 ==> pux1} P()

+{

+}

+

+// ------  and here are various correct things

+

+

+

+const {:Correct hux0 + F1(hux1)} hux0: int;

+

+function {:Correct F1(hux0) + hux1} F1(int) returns (int);

+

+axiom {:Correct F1(hux0 + hux1)} true;

+

+var {:Correct hux0*hux1} hux1: int;

+

+procedure {:Correct hux0 - hux1} H();

+

+implementation {:Correct hux0 + hux1} {:AlsoCorrect "hello"} H()

+{

+}

+

+

+type any;
\ No newline at end of file
diff --git a/Test/test1/CallForallResolve.bpl b/Test/test1/CallForallResolve.bpl
new file mode 100644
index 00000000..374db174
--- /dev/null
+++ b/Test/test1/CallForallResolve.bpl
@@ -0,0 +1,23 @@
+procedure P(x: int) returns (y: int);

+

+procedure CallP()

+{

+  call forall P(5);  // P is allowed here, even if it has out parameters

+}

+

+var global: bool;

+

+procedure Q(x: int);

+  modifies global;

+

+procedure CallQ()

+{

+  call forall Q(5);  // error: P is not allowed here, because it has a modifies clause

+}

+

+procedure R(x: int);

+

+procedure CallR()

+{

+  call forall R(5);  // no problem that R has no body, though

+}

diff --git a/Test/test1/EmptyCallArgs.bpl b/Test/test1/EmptyCallArgs.bpl
new file mode 100644
index 00000000..18d837a9
--- /dev/null
+++ b/Test/test1/EmptyCallArgs.bpl
@@ -0,0 +1,31 @@
+type C;

+

+procedure P(x:int, y:bool) returns (z:C);

+procedure Q<a>(x:int, y:a) returns (z:a);

+

+procedure CallP() {

+  var x:int;

+  var y:bool;

+  var z:C;

+

+  call z := P(x, y);

+  call * := P(x, y);

+  call z := P(*, y);

+  call z := P(x, *);

+  call * := P(*, x);   // type error

+  call * := P(x, *);

+  call z := P(*, *);

+  call * := P(*, *);

+}

+

+procedure CallQ() {

+  var x:int;

+  var y:bool;

+  var z:bool;

+

+  call x := Q(x, y);   // type error

+  call * := Q(x, y);

+  call x := Q(*, y);   // type error

+  call x := Q(x, *);

+  call * := Q(*, y);

+}
\ No newline at end of file
diff --git a/Test/test1/Family.bpl b/Test/test1/Family.bpl
new file mode 100644
index 00000000..1c650d3d
--- /dev/null
+++ b/Test/test1/Family.bpl
@@ -0,0 +1,47 @@
+type T;

+

+var Heap: <x>[ref,Field x]x;

+

+function IsHeap(<x>[ref,Field x]x) returns (bool);

+

+const alloc: Field bool;

+const C.x: Field int;

+

+axiom (forall h: <x>[ref,Field x]x, f: Field ref, o: ref :: IsHeap(h) && o != null ==> h[h[o,f], alloc]);

+

+procedure P(this: ref) returns (r: int)

+  modifies Heap;

+{

+  start:

+    r := Heap[this, C.x];

+    Heap[this, C.x] := r;

+    return;

+}

+

+// -----------------

+

+procedure R(this: ref)

+  modifies Heap;

+{

+  var field: any, refField: Field ref, yField: Field y, anyField: Field any;

+  var b: bool, a: any;

+

+  start:

+    b := Heap[this, C.x];     // type error

+    Heap[this, C.x] := true;  // type error

+    Heap[this, refField] := this;

+    Heap[this, yField] := 2;  // type error

+    Heap[this, field] := a;   // type error

+    Heap[this, field] := b;   // type error

+    Heap[this, anyField] := a;

+    Heap[this, anyField] := b;

+    Heap[this, anyField] := anyField;

+    Heap[this, anyField] := yField;

+    Heap[this, anyField] := field;

+    return;

+}

+

+type Field a;

+type y;

+type ref, any;

+const null : ref;

diff --git a/Test/test1/Frame0.bpl b/Test/test1/Frame0.bpl
new file mode 100644
index 00000000..02a5af46
--- /dev/null
+++ b/Test/test1/Frame0.bpl
@@ -0,0 +1,15 @@
+var g0: int;

+var g1: int;

+

+var h0: [ref, name]any;

+var h1: [ref, name]any;

+

+const X: name;

+

+procedure P(a: ref, hh: [ref, name]any) returns (b: int, hout: [ref, name]any);

+  modifies a;  // in-parameters are not mutable

+  modifies h1, g0;

+  modifies b;  // out-parameters are not allowed explicitly in modifies clause

+

+

+type ref, name, any;

diff --git a/Test/test1/Frame1.bpl b/Test/test1/Frame1.bpl
new file mode 100644
index 00000000..469f43ba
--- /dev/null
+++ b/Test/test1/Frame1.bpl
@@ -0,0 +1,97 @@
+var g0: int;

+var g1: int;

+

+var h0: [ref, name]int;

+var h1: [ref, name]int;

+

+const X: name;

+

+procedure P(a: ref, hh: [ref, name]int) returns (b: int, hout: [ref, name]any);

+  modifies h1, g0;

+

+implementation P(a: ref, hh: [ref, name]int)

+               returns (b: int, hout: [ref, name]any) {

+  start:

+    g0 := 5;

+    g1 := 6;  // error: g1 is not in modifies clause

+    a := null;  // error: in-parameters are not mutable 

+    b := 12;

+    goto next;

+  next:

+    havoc g0;

+    havoc g1;  // error: g1 is not in modifies clause

+    havoc a;  // error: in-parameters are not mutable

+    havoc b;

+    goto more;

+  more:

+    hh[a,X] := 101;  // error: in-parameter (hh) is not mutable

+    h0[a,X] := 102;  // error: h0 is not in modifies clause

+    h1[a,X] := 103;

+    hh := h0;  // error: in-parameter is not mutable

+    h0 := h1;  // error: h0 is not in modifies clause

+    h1 := hh;

+    havoc hh;  // error: in-parameter is not mutable

+    havoc h0;  // error: h0 is not in modifies clause

+    havoc h1;

+    return;

+}

+

+procedure PX();

+  modifies h1, g0;

+

+procedure PY()

+  modifies h1, g0;

+{

+  start:

+    call PX();

+    call PY();

+    return;

+}

+

+procedure PZ()

+  modifies h1;

+{

+  start:

+    call PX();  // error: PX has larger frame than PZ

+    return;

+}

+

+procedure Q() returns (x: int, y: int, h: [ref, name]int)

+{

+  start:

+    return;

+}

+

+procedure QCallerBad()

+{

+  start:

+    call g0, g1, h0 := Q();

+    return;

+}

+

+procedure QCallerGood()

+  modifies g0, h0;

+{

+  var t: int;

+

+  start:

+    call t, g0, h0 := Q();

+    return;

+}

+

+procedure MismatchedTypes(x: int);

+

+implementation MismatchedTypes(x: bool)  // error

+{

+  start:

+    return;

+}

+implementation MismatchedTypes(y: bool)  // error (this time with a different name for the formal)

+{

+  start:

+    return;

+}

+

+

+type ref, name, any;

+const null : ref;

diff --git a/Test/test1/FunBody.bpl b/Test/test1/FunBody.bpl
new file mode 100644
index 00000000..867942ff
--- /dev/null
+++ b/Test/test1/FunBody.bpl
@@ -0,0 +1,13 @@
+

+function g0<beta>(x:beta) returns (beta);

+function g1<beta>() returns (beta);

+

+function {:inline true} f1() returns (int) { 13 }

+function {:inline true} f2() returns (int) { true }                  // wrong type

+function {:inline true} f3<alpha>(x:alpha) returns (alpha) { g0(x) }

+function {:inline true} f4<alpha>(x:alpha) returns (alpha) { g0(5) } // wrong type

+function {:inline true} f5<alpha>() returns (alpha) { g1() }

+function {:inline true} f6<alpha>() returns (alpha) { g1():int }     // wrong type

+

+

+

diff --git a/Test/test1/LogicalExprs.bpl b/Test/test1/LogicalExprs.bpl
new file mode 100644
index 00000000..028d18f4
--- /dev/null
+++ b/Test/test1/LogicalExprs.bpl
@@ -0,0 +1,6 @@
+const P: bool;

+const Q: bool;

+

+axiom (forall x: int :: x < 0);

+axiom Q ==> P;

+axiom (forall x: int :: x < 0) ==> P;

diff --git a/Test/test1/MapsTypeErrors.bpl b/Test/test1/MapsTypeErrors.bpl
new file mode 100644
index 00000000..0e68440d
--- /dev/null
+++ b/Test/test1/MapsTypeErrors.bpl
@@ -0,0 +1,127 @@
+var m: []int;

+var p: <a>[]a;

+

+type ref;

+const null: ref;

+

+procedure P()

+  requires m[] == 5;

+  modifies m;

+  modifies p;

+  ensures m[] == 30;

+  ensures p[] + p[] == 24;

+  ensures p[] == null;

+{

+  m[] := 12;

+  p[] := 12;

+  p[] := true;

+  assert p[] == m[];

+  assert p[];

+  m := m[:= 30];

+  p := p[:=null];

+}

+

+procedure A()

+{

+  m[] := 12;  // error: illegal assignment, because m is not in modifies clause

+}

+

+procedure B()

+  modifies m;

+{

+  m := m[];  // type error

+  m[] := m;  // type error

+}

+

+procedure C()

+  modifies m;

+{

+  m[] := true;  // type error

+}

+

+// -----

+

+procedure Genrc<T>(x: int) returns (t: T);

+

+procedure Caller() returns (b: bool)

+{

+  var y: ref;

+  call y := Genrc(5);

+  b := y == null;

+}

+

+// ----

+

+type Field a;

+type HeapType = <a>[ref, Field a]a;

+const F0: Field int;

+const F1: Field bool;

+const alloc: Field bool;

+var Heap: HeapType;

+

+function LiberalEqual<a,b>(a, b) returns (bool);

+function StrictEqual<a>(a,a) returns (bool);

+function IntEqual(Field int,Field int) returns (bool);

+

+procedure FrameCondition(this: ref)

+  requires F0 == F1;  // error

+  requires LiberalEqual(F0, F1);

+  requires StrictEqual(F0, F0);

+  requires StrictEqual(F0, F1);  // error

+  modifies Heap;

+  ensures (forall<alpha> o: ref, f: Field alpha ::

+    Heap[o,f] == old(Heap)[o,f] ||

+    !old(Heap)[o,alloc] ||

+    (o == this && StrictEqual(f, F0)) ||  // error: f and F0 don't have the same type

+    (o == this && LiberalEqual(f, f)) ||

+    (o == this && IntEqual(F0, f))  // error: f and F0 don't have the same type

+    );

+{

+}

+

+// ---- bitvector inference ----

+

+function Gimmie<T>() returns (T);

+function Same<T>(T,T) returns (T);

+procedure ConsumeAnything<T>(t: T);

+

+procedure Bvs(x: bv31, y: int) returns (a: bv32)

+{

+  a := x[50 : 18];  // error

+  a := y[50 : 18];  // error

+

+  a := Gimmie();  // fine, this can be made to have at least 32 bits

+  a := Gimmie()[50 : 18];  // fine, result is always 32 bits and Gimmie() can be made to have at least 50 bits

+  a := Gimmie()[50 : 17];  // error, result is 33 bits (but there's nothing wrong with Gimmie())

+

+  a := Gimmie() ++ Gimmie() ++ Gimmie();

+  a := Gimmie() ++ Gimmie()[20:0];

+  a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie() ++ Gimmie()[27:0];

+  a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie() ++ Gimmie()[22:0];

+  a := 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie()[22:0] ++ Gimmie();

+  a := Gimmie() ++ 0bv0 ++ Gimmie()[6:6] ++ Gimmie()[17:12] ++ Gimmie() ++ Gimmie()[22:0];

+  a := Same(Gimmie(), Gimmie());

+  a := Same(Gimmie()[20:0], Gimmie());  // error, have only bv20, need bv32

+

+  a := Same(Gimmie() ++ Gimmie()[20:0], 0bv32);

+  a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie());

+  a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie() ++ Gimmie());

+  a := Same(Gimmie() ++ Gimmie()[20:0], Gimmie()[40:30] ++ Gimmie());

+  call ConsumeAnything(Same(Gimmie() ++ Gimmie()[20:0], 0bv18));  // error, can't make things smaller

+}

+

+// ---- maps again ----

+

+procedure Mmm() returns (a: [int,int]bool, b: HeapType, c: int)

+{

+  if (Gimmie()[null] == Gimmie()) {

+    a := Same(Gimmie()[Gimmie(), Gimmie() := Gimmie()], Gimmie());

+    b := Same(Gimmie()[Gimmie(), Gimmie() := Gimmie()], Gimmie());

+    a := Same(Gimmie()[Gimmie(), Gimmie() := 4], Gimmie());  // error

+    b := Same(Gimmie()[Gimmie(), Gimmie() := 5], Gimmie());

+    b := Same(Gimmie()[Gimmie(), 6 := Gimmie()], Gimmie());  // error

+  }

+  c := Gimmie()[Gimmie() := 10][null];

+  c := Gimmie()[Gimmie() := Gimmie()][null];

+  c := Gimmie()[Gimmie() := false][null];

+}

diff --git a/Test/test1/Orderings.bpl b/Test/test1/Orderings.bpl
new file mode 100644
index 00000000..be0502fa
--- /dev/null
+++ b/Test/test1/Orderings.bpl
@@ -0,0 +1,8 @@
+

+type C;

+

+const c1:C;

+const c2:C extends c1;

+const c0:C extends a;         // error: parent of wrong type

+

+const a:int;

diff --git a/Test/test1/Output b/Test/test1/Output
new file mode 100644
index 00000000..b0f4aac3
--- /dev/null
+++ b/Test/test1/Output
@@ -0,0 +1,137 @@
+Frame0.bpl(10,11): Error: undeclared identifier: a

+Frame0.bpl(12,11): Error: undeclared identifier: b

+2 name resolution errors detected in Frame0.bpl

+Frame1.bpl(16,7): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

+Frame1.bpl(17,6): Error: command assigns to an immutable variable: a

+Frame1.bpl(22,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

+Frame1.bpl(23,4): Error: command assigns to an immutable variable: a

+Frame1.bpl(27,12): Error: command assigns to an immutable variable: hh

+Frame1.bpl(28,12): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(30,7): Error: command assigns to an immutable variable: hh

+Frame1.bpl(31,7): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(33,4): Error: command assigns to an immutable variable: hh

+Frame1.bpl(34,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(55,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g0

+Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g0

+Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: g1

+Frame1.bpl(68,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: h0

+Frame1.bpl(84,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x

+Frame1.bpl(89,15): Error: mismatched type of in-parameter in implementation MismatchedTypes: x (named y in implementation)

+16 type checking errors detected in Frame1.bpl

+

+Boogie program verifier finished with 0 verified, 0 errors

+Arrays.bpl(15,14): Error: wrong number of arguments in map select: 2 instead of 1

+Arrays.bpl(16,14): Error: wrong number of arguments in map select: 1 instead of 2

+Arrays.bpl(20,7): Error: wrong number of arguments in map assignment: 2 instead of 1

+Arrays.bpl(21,7): Error: wrong number of arguments in map assignment: 1 instead of 2

+Arrays.bpl(41,13): Error: invalid type for argument 0 in map select: bool (expected: int)

+Arrays.bpl(42,16): Error: invalid argument types (bool and int) to binary operator ==

+Arrays.bpl(43,13): Error: invalid type for argument 0 in map select: int (expected: bool)

+Arrays.bpl(43,15): Error: invalid type for argument 1 in map select: int (expected: ref)

+Arrays.bpl(44,15): Error: invalid type for argument 1 in map select: bool (expected: ref)

+Arrays.bpl(44,23): Error: invalid type for argument 0 in map select: ref (expected: bool)

+Arrays.bpl(45,13): Error: invalid type for argument 0 in map select: ref (expected: bool)

+Arrays.bpl(45,18): Error: invalid type for argument 1 in map select: int (expected: ref)

+Arrays.bpl(45,2): Error: preconditions must be of type bool

+Arrays.bpl(46,13): Error: invalid type for argument 0 in map select: int (expected: bool)

+Arrays.bpl(46,15): Error: invalid type for argument 1 in map select: int (expected: ref)

+Arrays.bpl(50,6): Error: invalid type for argument 0 in map assignment: bool (expected: int)

+Arrays.bpl(51,6): Error: invalid type for argument 0 in map assignment: int (expected: bool)

+Arrays.bpl(51,8): Error: invalid type for argument 1 in map assignment: int (expected: ref)

+Arrays.bpl(51,5): Error: mismatched types in assignment command (cannot assign ref to int)

+Arrays.bpl(52,7): Error: invalid type for argument 0 in map assignment: bool (expected: int)

+Arrays.bpl(52,5): Error: mismatched types in assignment command (cannot assign int to bool)

+Arrays.bpl(53,12): Error: invalid type for argument 1 in map assignment: bool (expected: ref)

+Arrays.bpl(113,11): Error: invalid type for argument 0 in map select: name (expected: [int,int]bool)

+Arrays.bpl(114,4): Error: mismatched types in assignment command (cannot assign [int,int]bool to [[int,int]bool,[name]name]int)

+Arrays.bpl(115,4): Error: mismatched types in assignment command (cannot assign name to [int,int]bool)

+Arrays.bpl(116,5): Error: mismatched types in assignment command (cannot assign name to bool)

+Arrays.bpl(117,8): Error: invalid type for argument 1 in map assignment: name (expected: [name]name)

+Arrays.bpl(118,4): Error: mismatched types in assignment command (cannot assign [int,int][int]int to [[int,int]bool,[name]name]int)

+Arrays.bpl(123,10): Error: wrong number of arguments in map select: 1 instead of 2

+Arrays.bpl(124,14): Error: wrong number of arguments in map select: 1 instead of 2

+Arrays.bpl(125,6): Error: invalid type for argument 0 in map assignment: bool (expected: int)

+Arrays.bpl(126,4): Error: mismatched types in assignment command (cannot assign [int,int][int]int to [int,int][name]int)

+Arrays.bpl(127,4): Error: mismatched types in assignment command (cannot assign [int,int][name]int to [int,int][int]int)

+Arrays.bpl(130,21): Error: wrong number of arguments in map select: 2 instead of 1

+Arrays.bpl(131,5): Error: wrong number of arguments in map assignment: 2 instead of 1

+Arrays.bpl(132,13): Error: wrong number of arguments in map select: 2 instead of 1

+Arrays.bpl(133,17): Error: wrong number of arguments in map select: 1 instead of 2

+Arrays.bpl(134,14): Error: wrong number of arguments in map select: 2 instead of 1

+Arrays.bpl(166,12): Error: invalid type for argument 0 in application of Sf: [int,int]bool (expected: any)

+Arrays.bpl(176,4): Error: mismatched types in assignment command (cannot assign [int,int]bool to <a>[int,a]bool)

+Arrays.bpl(177,4): Error: mismatched types in assignment command (cannot assign <a>[int,a]bool to [int,int]bool)

+Arrays.bpl(178,4): Error: mismatched types in assignment command (cannot assign [any,any]bool to <a>[int,a]bool)

+Arrays.bpl(179,4): Error: mismatched types in assignment command (cannot assign <a>[int,a]bool to [any,any]bool)

+Arrays.bpl(180,4): Error: mismatched types in assignment command (cannot assign [ref]bool to [any]bool)

+Arrays.bpl(191,18): Error: invalid type for argument 0 in map select: any (expected: int)

+Arrays.bpl(198,11): Error: invalid type for argument 0 in map assignment: any (expected: int)

+Arrays.bpl(214,24): Error: invalid type for argument 0 in call to IntMethod: int (expected: any)

+Arrays.bpl(214,9): Error: invalid type for out-parameter 0 in call to IntMethod: any (expected: int)

+Arrays.bpl(215,4): Error: mismatched types in assignment command (cannot assign int to any)

+Arrays.bpl(216,4): Error: mismatched types in assignment command (cannot assign any to int)

+Arrays.bpl(218,24): Error: invalid type for argument 0 in call to AnyMethod: any (expected: int)

+Arrays.bpl(218,9): Error: invalid type for out-parameter 0 in call to AnyMethod: int (expected: any)

+52 type checking errors detected in Arrays.bpl

+WhereTyping.bpl(25,34): Error: invalid argument types (double and int) to binary operator +

+WhereTyping.bpl(26,12): Error: where clauses must be of type bool

+WhereTyping.bpl(36,22): Error: invalid argument types (name and int) to binary operator !=

+WhereTyping.bpl(41,30): Error: invalid argument types (name and int) to binary operator ==

+4 type checking errors detected in WhereTyping.bpl

+Family.bpl(30,4): Error: mismatched types in assignment command (cannot assign int to bool)

+Family.bpl(31,8): Error: mismatched types in assignment command (cannot assign bool to int)

+Family.bpl(33,8): Error: mismatched types in assignment command (cannot assign int to y)

+Family.bpl(34,15): Error: invalid type for argument 1 in map assignment: any (expected: Field x)

+Family.bpl(35,15): Error: invalid type for argument 1 in map assignment: any (expected: Field x)

+Family.bpl(37,8): Error: mismatched types in assignment command (cannot assign bool to any)

+Family.bpl(38,8): Error: mismatched types in assignment command (cannot assign Field any to any)

+Family.bpl(39,8): Error: mismatched types in assignment command (cannot assign Field y to any)

+8 type checking errors detected in Family.bpl

+AttributeTyping.bpl(3,23): Error: ++ operands need to be bitvectors (got int, int)

+AttributeTyping.bpl(5,29): Error: invalid type for argument 0 in application of F0: bool (expected: int)

+AttributeTyping.bpl(7,26): Error: invalid type for argument 0 in application of F0: bool (expected: int)

+AttributeTyping.bpl(9,21): Error: invalid argument types (int and int) to binary operator &&

+AttributeTyping.bpl(11,22): Error: invalid argument type (int) to unary operator !

+AttributeTyping.bpl(13,32): Error: invalid argument types (int and int) to binary operator ==>

+6 type checking errors detected in AttributeTyping.bpl

+UpdateExprTyping.bpl(3,11): Error: invalid argument types ([int]bool and [int]ref) to binary operator ==

+UpdateExprTyping.bpl(4,11): Error: invalid argument types ([int]bool and [bool]bool) to binary operator ==

+UpdateExprTyping.bpl(7,16): Error: invalid type for argument 0 in map store: bool (expected: int)

+UpdateExprTyping.bpl(8,21): Error: right-hand side in map store with wrong type: int (expected: bool)

+UpdateExprTyping.bpl(9,11): Error: invalid argument types ([int]bool and [int]ref) to binary operator ==

+UpdateExprTyping.bpl(15,18): Error: invalid type for argument 0 in map store: ref (expected: int)

+UpdateExprTyping.bpl(16,20): Error: invalid type for argument 1 in map store: bool (expected: ref)

+UpdateExprTyping.bpl(17,28): Error: right-hand side in map store with wrong type: ref (expected: bool)

+UpdateExprTyping.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to any)

+UpdateExprTyping.bpl(36,28): Error: right-hand side in map store with wrong type: ref (expected: any)

+UpdateExprTyping.bpl(38,27): Error: right-hand side in map store with wrong type: ref (expected: int)

+UpdateExprTyping.bpl(39,27): Error: right-hand side in map store with wrong type: int (expected: ref)

+12 type checking errors detected in UpdateExprTyping.bpl

+CallForallResolve.bpl(15,2): Error: call forall is allowed only on procedures with no modifies clause: Q

+1 type checking errors detected in CallForallResolve.bpl

+MapsTypeErrors.bpl(26,6): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: m

+MapsTypeErrors.bpl(32,2): Error: mismatched types in assignment command (cannot assign int to []int)

+MapsTypeErrors.bpl(33,3): Error: mismatched types in assignment command (cannot assign []int to int)

+MapsTypeErrors.bpl(39,3): Error: mismatched types in assignment command (cannot assign bool to int)

+MapsTypeErrors.bpl(67,14): Error: invalid argument types (Field int and Field bool) to binary operator ==

+MapsTypeErrors.bpl(70,27): Error: invalid type for argument 1 in application of StrictEqual: Field bool (expected: a)

+MapsTypeErrors.bpl(75,33): Error: invalid type for argument 1 in application of StrictEqual: Field int (expected: a)

+MapsTypeErrors.bpl(77,31): Error: invalid type for argument 1 in application of IntEqual: Field alpha (expected: Field int)

+MapsTypeErrors.bpl(90,8): Error: extract operand must be a bitvector of at least 32 bits (got bv31)

+MapsTypeErrors.bpl(91,8): Error: extract operand must be a bitvector of at least 32 bits (got int)

+MapsTypeErrors.bpl(95,2): Error: mismatched types in assignment command (cannot assign bv33 to bv32)

+MapsTypeErrors.bpl(104,2): Error: mismatched types in assignment command (cannot assign bv20 to bv32)

+MapsTypeErrors.bpl(110,56): Error: invalid type for argument 1 in application of Same: bv18 (expected: T)

+MapsTypeErrors.bpl(120,4): Error: mismatched types in assignment command (cannot assign [?, ?]? to [int,int]bool)

+MapsTypeErrors.bpl(122,4): Error: mismatched types in assignment command (cannot assign [?, ?]? to HeapType)

+15 type checking errors detected in MapsTypeErrors.bpl

+Orderings.bpl(6,19): Error: parent of constant has incompatible type (int instead of C)

+1 type checking errors detected in Orderings.bpl

+EmptyCallArgs.bpl(15,17): Error: invalid type for argument 0 in call to P: int (expected: bool)

+EmptyCallArgs.bpl(26,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)

+EmptyCallArgs.bpl(28,7): Error: invalid type for out-parameter 0 in call to Q: int (expected: bool)

+3 type checking errors detected in EmptyCallArgs.bpl

+FunBody.bpl(6,45): Error: function body with invalid type: bool (expected: int)

+FunBody.bpl(8,61): Error: function body with invalid type: int (expected: alpha)

+FunBody.bpl(10,58): Error: function body with invalid type: int (expected: alpha)

+3 type checking errors detected in FunBody.bpl

diff --git a/Test/test1/UpdateExprTyping.bpl b/Test/test1/UpdateExprTyping.bpl
new file mode 100644
index 00000000..e495cb51
--- /dev/null
+++ b/Test/test1/UpdateExprTyping.bpl
@@ -0,0 +1,43 @@
+procedure P(a: [int]bool, b: [int]ref, c: [bool]bool)

+{

+  assert a == b;  // type error

+  assert a == c;  // type error

+

+  assert a == a[5 := true];

+  assert a == a[true := true];  // type error

+  assert a == a[5 := 5]; // type error in RHS

+  assert a == b[5 := null];  // type error

+}

+

+procedure Q(aa: [int,ref]bool)

+{

+  assert aa[5,null := true] != aa[2,null := false];

+  assert aa == aa[null,null := true];  // type error, index 0

+  assert aa == aa[5,true := true];  // type error, index 1

+  assert aa == aa[5,null := null];  // type error, RHS

+}

+

+type Field a;

+const unique IntField: Field int;

+const unique RefField: Field ref;

+const unique SomeField: Field any;

+

+procedure R(H: <x>[ref,Field x]x, this: ref)

+{

+  var i: int, r: ref, y: any;

+  var K: <wz>[ref,Field wz]wz;

+

+  i := H[this, IntField];

+  r := H[this, RefField];

+  y := H[this, IntField];       // type error, wrong LHS

+  y := H[this, SomeField];

+

+  K := H[this, IntField := i][this, RefField := r][this, SomeField := y];

+  K := H[this, SomeField := r]; // type error, wrong RHS

+

+  K := K[this, IntField := r];  // RHS has wrong type (ref, expecting int)

+  K := K[this, RefField := i];  // RHS has wrong type (int, expecting ref)

+}

+

+type ref, any;

+const null : ref;

diff --git a/Test/test1/WhereTyping.bpl b/Test/test1/WhereTyping.bpl
new file mode 100644
index 00000000..dba628ee
--- /dev/null
+++ b/Test/test1/WhereTyping.bpl
@@ -0,0 +1,45 @@
+var g: int where g == 12;

+

+procedure P(x: int where x > 0) returns (y: int where y < 0);

+  requires x < 100;

+  modifies g;

+  ensures -100 < y;

+

+implementation P(xx: int) returns (yy: int)

+{

+  var a: int;

+  var b: int;

+

+  start:

+    a := xx;

+    call b := P(a);

+    yy := b;

+    return;

+}

+

+type double;

+function F(double) returns (double);

+function G(double) returns (bool);

+

+procedure Q(omega: double where omega == F(omega),

+            psi: double where psi + 1 == 0,  // error: psi doesn't have right type for +

+            pi: double where F(pi),          // error: F has wrong return type

+            sigma: double where G(sigma));

+

+

+const SomeConstant: name;

+function fgh(int) returns (int);

+

+procedure Cnst(n: name where n <: SomeConstant /*this SomeConstant refers to the const*/) returns (SomeConstant: int)

+{

+  var k: int where k != SomeConstant;  // fine, since SomeConstants refers to the out parameter

+  var m: name where m != SomeConstant;  // error: types don't match up

+  var r: ref where (forall abc: int :: abc == SomeConstant);

+  var b: bool;

+  start:

+    b := (forall x: int :: fgh(x) < SomeConstant);

+    b := (forall l: name :: l == SomeConstant);  // error: SomeConstant here refers to the out parameter

+    return;

+}

+

+type ref, name;

diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat
new file mode 100644
index 00000000..c6881263
--- /dev/null
+++ b/Test/test1/runtest.bat
@@ -0,0 +1,19 @@
+@echo off

+setlocal

+

+set BGEXE=..\..\Binaries\Boogie.exe

+rem set BGEXE=mono ..\..\Binaries\Boogie.exe

+

+%BGEXE% %* /noVerify Frame0.bpl

+%BGEXE% %* /noVerify Frame1.bpl

+%BGEXE% %* /noVerify LogicalExprs.bpl

+%BGEXE% %* /noVerify Arrays.bpl

+%BGEXE% %* /noVerify WhereTyping.bpl

+%BGEXE% %* /noVerify Family.bpl

+%BGEXE% %* /noVerify AttributeTyping.bpl

+%BGEXE% %* /noVerify UpdateExprTyping.bpl

+%BGEXE% %* /noVerify CallForallResolve.bpl

+%BGEXE% %* /noVerify MapsTypeErrors.bpl

+%BGEXE% %* /noVerify Orderings.bpl

+%BGEXE% %* /noVerify EmptyCallArgs.bpl

+%BGEXE% %* /noVerify FunBody.bpl