From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Wed, 15 Jul 2009 21:03:41 +0000 Subject: Initial set of files. --- Test/test1/Answer | 137 ++++++++++++++++++++++++ Test/test1/Arrays.bpl | 224 +++++++++++++++++++++++++++++++++++++++ Test/test1/AttributeTyping.bpl | 36 +++++++ Test/test1/CallForallResolve.bpl | 23 ++++ Test/test1/EmptyCallArgs.bpl | 31 ++++++ Test/test1/Family.bpl | 47 ++++++++ Test/test1/Frame0.bpl | 15 +++ Test/test1/Frame1.bpl | 97 +++++++++++++++++ Test/test1/FunBody.bpl | 13 +++ Test/test1/LogicalExprs.bpl | 6 ++ Test/test1/MapsTypeErrors.bpl | 127 ++++++++++++++++++++++ Test/test1/Orderings.bpl | 8 ++ Test/test1/Output | 137 ++++++++++++++++++++++++ Test/test1/UpdateExprTyping.bpl | 43 ++++++++ Test/test1/WhereTyping.bpl | 45 ++++++++ Test/test1/runtest.bat | 19 ++++ 16 files changed, 1008 insertions(+) create mode 100644 Test/test1/Answer create mode 100644 Test/test1/Arrays.bpl create mode 100644 Test/test1/AttributeTyping.bpl create mode 100644 Test/test1/CallForallResolve.bpl create mode 100644 Test/test1/EmptyCallArgs.bpl create mode 100644 Test/test1/Family.bpl create mode 100644 Test/test1/Frame0.bpl create mode 100644 Test/test1/Frame1.bpl create mode 100644 Test/test1/FunBody.bpl create mode 100644 Test/test1/LogicalExprs.bpl create mode 100644 Test/test1/MapsTypeErrors.bpl create mode 100644 Test/test1/Orderings.bpl create mode 100644 Test/test1/Output create mode 100644 Test/test1/UpdateExprTyping.bpl create mode 100644 Test/test1/WhereTyping.bpl create mode 100644 Test/test1/runtest.bat (limited to 'Test/test1') 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 [int,a]bool) +Arrays.bpl(177,4): Error: mismatched types in assignment command (cannot assign [int,a]bool to [int,int]bool) +Arrays.bpl(178,4): Error: mismatched types in assignment command (cannot assign [any,any]bool to [int,a]bool) +Arrays.bpl(179,4): Error: mismatched types in assignment command (cannot assign [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: [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]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(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: [ref,Field x]x; + +function IsHeap([ref,Field x]x) returns (bool); + +const alloc: Field bool; +const C.x: Field int; + +axiom (forall h: [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(x:beta) returns (beta); +function g1() returns (beta); + +function {:inline true} f1() returns (int) { 13 } +function {:inline true} f2() returns (int) { true } // wrong type +function {:inline true} f3(x:alpha) returns (alpha) { g0(x) } +function {:inline true} f4(x:alpha) returns (alpha) { g0(5) } // wrong type +function {:inline true} f5() returns (alpha) { g1() } +function {:inline true} f6() 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; + +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(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 = [ref, Field a]a; +const F0: Field int; +const F1: Field bool; +const alloc: Field bool; +var Heap: HeapType; + +function LiberalEqual(a, b) returns (bool); +function StrictEqual(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 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() returns (T); +function Same(T,T) returns (T); +procedure ConsumeAnything(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 [int,a]bool) +Arrays.bpl(177,4): Error: mismatched types in assignment command (cannot assign [int,a]bool to [int,int]bool) +Arrays.bpl(178,4): Error: mismatched types in assignment command (cannot assign [any,any]bool to [int,a]bool) +Arrays.bpl(179,4): Error: mismatched types in assignment command (cannot assign [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: [ref,Field x]x, this: ref) +{ + var i: int, r: ref, y: any; + var K: [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 -- cgit v1.2.3