From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Test/test1/Arrays.bpl | 452 ++++++++++++++--------------- Test/test1/AssumptionVariables0.bpl | 114 ++++---- Test/test1/AssumptionVariables1.bpl | 12 +- Test/test1/AssumptionVariables1.bpl.expect | 4 +- Test/test1/AttributeTyping.bpl | 74 ++--- Test/test1/EmptyCallArgs.bpl | 42 +-- Test/test1/Family.bpl | 98 +++---- Test/test1/Frame0.bpl | 34 +-- Test/test1/Frame1.bpl | 198 ++++++------- Test/test1/FunBody.bpl | 30 +- Test/test1/IfThenElse0.bpl | 4 +- Test/test1/IntReal.bpl | 100 +++---- Test/test1/Lambda.bpl | 4 +- Test/test1/LogicalExprs.bpl | 16 +- Test/test1/MapsTypeErrors.bpl | 258 ++++++++-------- Test/test1/Orderings.bpl | 20 +- Test/test1/UpdateExprTyping.bpl | 90 +++--- Test/test1/WhereTyping.bpl | 94 +++--- 18 files changed, 822 insertions(+), 822 deletions(-) (limited to 'Test/test1') diff --git a/Test/test1/Arrays.bpl b/Test/test1/Arrays.bpl index cb21e4ed..2013a69c 100644 --- a/Test/test1/Arrays.bpl +++ b/Test/test1/Arrays.bpl @@ -1,226 +1,226 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -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; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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/AssumptionVariables0.bpl b/Test/test1/AssumptionVariables0.bpl index 7046ea59..7ebd3d24 100644 --- a/Test/test1/AssumptionVariables0.bpl +++ b/Test/test1/AssumptionVariables0.bpl @@ -1,57 +1,57 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure Test0() -{ - var {:assumption} a0: bool where a0; // error -} - - -procedure Test1() -{ - var {:assumption} a0: bool; - - a0 := a0 && true; -} - - -procedure Test2() -{ - var {:assumption} a0: bool; - - a0 := true; // error -} - - -procedure Test3() -{ - var {:assumption} a0: bool; - var {:assumption} a1: bool; - - a0 := a1 && true; // error -} - - -procedure Test4() -{ - var {:assumption} a0: bool; - - a0 := a0 && true; - a0 := a0 && true; // error -} - - -procedure Test5() - modifies a0; -{ - a0 := a0 && true; -} - - -var {:assumption} a0: bool; - - -procedure Test6() - modifies a0; -{ - a0 := a0 && true; // error -} +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure Test0() +{ + var {:assumption} a0: bool where a0; // error +} + + +procedure Test1() +{ + var {:assumption} a0: bool; + + a0 := a0 && true; +} + + +procedure Test2() +{ + var {:assumption} a0: bool; + + a0 := true; // error +} + + +procedure Test3() +{ + var {:assumption} a0: bool; + var {:assumption} a1: bool; + + a0 := a1 && true; // error +} + + +procedure Test4() +{ + var {:assumption} a0: bool; + + a0 := a0 && true; + a0 := a0 && true; // error +} + + +procedure Test5() + modifies a0; +{ + a0 := a0 && true; +} + + +var {:assumption} a0: bool; + + +procedure Test6() + modifies a0; +{ + a0 := a0 && true; // error +} diff --git a/Test/test1/AssumptionVariables1.bpl b/Test/test1/AssumptionVariables1.bpl index 3125650c..918a9b63 100644 --- a/Test/test1/AssumptionVariables1.bpl +++ b/Test/test1/AssumptionVariables1.bpl @@ -1,6 +1,6 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure Test0() -{ - var {:assumption} a0: int; // error -} +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure Test0() +{ + var {:assumption} a0: int; // error +} diff --git a/Test/test1/AssumptionVariables1.bpl.expect b/Test/test1/AssumptionVariables1.bpl.expect index 9e894bf9..badc18b3 100644 --- a/Test/test1/AssumptionVariables1.bpl.expect +++ b/Test/test1/AssumptionVariables1.bpl.expect @@ -1,2 +1,2 @@ -AssumptionVariables1.bpl(5,22): Error: assumption variable must be of type 'bool' -1 type checking errors detected in AssumptionVariables1.bpl +AssumptionVariables1.bpl(5,22): Error: assumption variable must be of type 'bool' +1 type checking errors detected in AssumptionVariables1.bpl diff --git a/Test/test1/AttributeTyping.bpl b/Test/test1/AttributeTyping.bpl index bcd98feb..713f464c 100644 --- a/Test/test1/AttributeTyping.bpl +++ b/Test/test1/AttributeTyping.bpl @@ -1,38 +1,38 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - - -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() -{ -} - - +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + + +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/EmptyCallArgs.bpl b/Test/test1/EmptyCallArgs.bpl index 8f5ae31f..3c2aa177 100644 --- a/Test/test1/EmptyCallArgs.bpl +++ b/Test/test1/EmptyCallArgs.bpl @@ -1,22 +1,22 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -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); -} - -procedure CallQ() { - var x:int; - var y:bool; - var z:bool; - - call x := Q(x, y); // type error +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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); +} + +procedure CallQ() { + var x:int; + var y:bool; + var z:bool; + + call x := Q(x, y); // type error } \ No newline at end of file diff --git a/Test/test1/Family.bpl b/Test/test1/Family.bpl index fec96332..0ec5fb20 100644 --- a/Test/test1/Family.bpl +++ b/Test/test1/Family.bpl @@ -1,49 +1,49 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -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; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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 index 6155fc27..a3ef6138 100644 --- a/Test/test1/Frame0.bpl +++ b/Test/test1/Frame0.bpl @@ -1,17 +1,17 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -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; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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 index 2ec70270..5e637660 100644 --- a/Test/test1/Frame1.bpl +++ b/Test/test1/Frame1.bpl @@ -1,99 +1,99 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -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; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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 index fc566681..caaf06f5 100644 --- a/Test/test1/FunBody.bpl +++ b/Test/test1/FunBody.bpl @@ -1,15 +1,15 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -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 - - - +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +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/IfThenElse0.bpl b/Test/test1/IfThenElse0.bpl index 19918827..65ae65f6 100644 --- a/Test/test1/IfThenElse0.bpl +++ b/Test/test1/IfThenElse0.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" procedure foo() { var b:bool, i:int; diff --git a/Test/test1/IntReal.bpl b/Test/test1/IntReal.bpl index 962aadf3..7b3d77e5 100644 --- a/Test/test1/IntReal.bpl +++ b/Test/test1/IntReal.bpl @@ -1,50 +1,50 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -const i: int; -const r: real; - -axiom i == 0; -axiom i >= 0.0; // type error -axiom i <= 0.0e0; // type error -axiom i < 0.0e-0; // type error -axiom i > 0.0e20; // type error - -axiom -i == r; // type error -axiom i + r == 0.0; // type error -axiom i - r == 0.0; // type error -axiom i * r == 0.0; // type error -axiom i div r == 0; // type error -axiom i mod r == 0; // type error - -axiom i / i == 0; // type error -axiom i / i == 0.0; -axiom i / r == 0.0; -axiom r / i == 0.0; -axiom r / r == 0.0; - -axiom i ** r == 0.0; // type error -axiom r ** r == 0.0; - -axiom real(i) == 0.0; -axiom real(i) == i; // type error -axiom int(r) == 0; -axiom int(r) == r; // type error -axiom int(real(i)) == i; -axiom real(int(r)) == r; -axiom int(int(r)) == i; // type error -axiom real(real(i)) == r; // type error - -axiom i == 0; -axiom real(i) >= 0.0; -axiom real(i) <= 0.0e0; -axiom r < 0.0e-0; -axiom r > 0.0e20; - -axiom -r == real(i); -axiom real(i) + r == 0.0; -axiom r - real(0) == 0.0; -axiom r * r == 0.0; -axiom r div 0 == 0; // type error -axiom r mod 0 == 0; // type error - -axiom r ** r == 0.0; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +const i: int; +const r: real; + +axiom i == 0; +axiom i >= 0.0; // type error +axiom i <= 0.0e0; // type error +axiom i < 0.0e-0; // type error +axiom i > 0.0e20; // type error + +axiom -i == r; // type error +axiom i + r == 0.0; // type error +axiom i - r == 0.0; // type error +axiom i * r == 0.0; // type error +axiom i div r == 0; // type error +axiom i mod r == 0; // type error + +axiom i / i == 0; // type error +axiom i / i == 0.0; +axiom i / r == 0.0; +axiom r / i == 0.0; +axiom r / r == 0.0; + +axiom i ** r == 0.0; // type error +axiom r ** r == 0.0; + +axiom real(i) == 0.0; +axiom real(i) == i; // type error +axiom int(r) == 0; +axiom int(r) == r; // type error +axiom int(real(i)) == i; +axiom real(int(r)) == r; +axiom int(int(r)) == i; // type error +axiom real(real(i)) == r; // type error + +axiom i == 0; +axiom real(i) >= 0.0; +axiom real(i) <= 0.0e0; +axiom r < 0.0e-0; +axiom r > 0.0e20; + +axiom -r == real(i); +axiom real(i) + r == 0.0; +axiom r - real(0) == 0.0; +axiom r * r == 0.0; +axiom r div 0 == 0; // type error +axiom r mod 0 == 0; // type error + +axiom r ** r == 0.0; diff --git a/Test/test1/Lambda.bpl b/Test/test1/Lambda.bpl index 016bece7..5136a1e5 100644 --- a/Test/test1/Lambda.bpl +++ b/Test/test1/Lambda.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" procedure foo() { var a: [int,int]int; diff --git a/Test/test1/LogicalExprs.bpl b/Test/test1/LogicalExprs.bpl index 02174a32..a5d3f987 100644 --- a/Test/test1/LogicalExprs.bpl +++ b/Test/test1/LogicalExprs.bpl @@ -1,8 +1,8 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -const P: bool; -const Q: bool; - -axiom (forall x: int :: x < 0); -axiom Q ==> P; -axiom (forall x: int :: x < 0) ==> P; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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 index bedb02ec..4b1bfec6 100644 --- a/Test/test1/MapsTypeErrors.bpl +++ b/Test/test1/MapsTypeErrors.bpl @@ -1,129 +1,129 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -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]; -} +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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 index 4ab28a48..bad7c2ad 100644 --- a/Test/test1/Orderings.bpl +++ b/Test/test1/Orderings.bpl @@ -1,10 +1,10 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -type C; - -const c1:C; -const c2:C extends c1; -const c0:C extends a; // error: parent of wrong type - -const a:int; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +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/UpdateExprTyping.bpl b/Test/test1/UpdateExprTyping.bpl index bf8fd47c..41b88a3c 100644 --- a/Test/test1/UpdateExprTyping.bpl +++ b/Test/test1/UpdateExprTyping.bpl @@ -1,45 +1,45 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -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; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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 index 0884e8ef..b3675f45 100644 --- a/Test/test1/WhereTyping.bpl +++ b/Test/test1/WhereTyping.bpl @@ -1,47 +1,47 @@ -// RUN: %boogie -noVerify "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -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; +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +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; -- cgit v1.2.3