summaryrefslogtreecommitdiff
path: root/Test/test1/Arrays.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test1/Arrays.bpl')
-rw-r--r--Test/test1/Arrays.bpl452
1 files changed, 226 insertions, 226 deletions
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: <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;
+// 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: <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;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 02:43:23 +0000