diff options
Diffstat (limited to 'Test/test0')
31 files changed, 1266 insertions, 1255 deletions
diff --git a/Test/test0/Arrays0.bpl b/Test/test0/Arrays0.bpl index 6c208b1e..3f365d8f 100644 --- a/Test/test0/Arrays0.bpl +++ b/Test/test0/Arrays0.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff NoErrors.expect "%t"
-var one: [int]int;
-var two: [int,int]int;
-var three: [int,int,int]int; // three's a crowd
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff NoErrors.expect "%t" +var one: [int]int; +var two: [int,int]int; +var three: [int,int,int]int; // three's a crowd diff --git a/Test/test0/Arrays1.bpl b/Test/test0/Arrays1.bpl index 4e031cb8..0c9f6044 100644 --- a/Test/test0/Arrays1.bpl +++ b/Test/test0/Arrays1.bpl @@ -1,22 +1,22 @@ -// RUN: %boogie -noVerify "%s" | %OutputCheck "%s"
-var Q: [int,int][int]int;
-
-procedure P()
-{
- var q: [int]int;
-
- start:
- // here's how to do it:
- q := Q[5,8];
- q[13] := 21;
-
- // CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
- Q[5,8] := q;
-
- // not like this:
- // CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q
- Q[5,8][13] := 21; // error: the updated array must be an identifier
- return;
-}
-
-// CHECK-L: 2 type checking errors detected in ${CHECKFILE_NAME}
+// RUN: %boogie -noVerify "%s" | %OutputCheck "%s" +var Q: [int,int][int]int; + +procedure P() +{ + var q: [int]int; + + start: + // here's how to do it: + q := Q[5,8]; + q[13] := 21; + + // CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},11): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q + Q[5,8] := q; + + // not like this: + // CHECK-L: ${CHECKFILE_NAME}(${LINE:+1},15): Error: command assigns to a global variable that is not in the enclosing procedure's modifies clause: Q + Q[5,8][13] := 21; // error: the updated array must be an identifier + return; +} + +// CHECK-L: 2 type checking errors detected in ${CHECKFILE_NAME} diff --git a/Test/test0/AssertVerifiedUnder0.bpl b/Test/test0/AssertVerifiedUnder0.bpl new file mode 100644 index 00000000..1b054f68 --- /dev/null +++ b/Test/test0/AssertVerifiedUnder0.bpl @@ -0,0 +1,8 @@ +// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure test0() +{ + assert {:verified_under} true; + assert {:verified_under true, false} true; +} diff --git a/Test/test0/AssertVerifiedUnder0.bpl.expect b/Test/test0/AssertVerifiedUnder0.bpl.expect new file mode 100644 index 00000000..b3d8177d --- /dev/null +++ b/Test/test0/AssertVerifiedUnder0.bpl.expect @@ -0,0 +1,3 @@ +AssertVerifiedUnder0.bpl(6,11): Error: attribute :verified_under accepts only one argument +AssertVerifiedUnder0.bpl(7,11): Error: attribute :verified_under accepts only one argument +2 name resolution errors detected in AssertVerifiedUnder0.bpl diff --git a/Test/test0/AttributeParsing.bpl b/Test/test0/AttributeParsing.bpl index afc0a88d..7372fcc4 100644 --- a/Test/test0/AttributeParsing.bpl +++ b/Test/test0/AttributeParsing.bpl @@ -1,40 +1,40 @@ -// RUN: %boogie -noVerify -print:- -env:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type {:sourcefile "test.ssc"} T;
-
-function {:source "test.scc"} f(int) returns (int);
-
-const {:description "The largest integer value"} unique MAXINT: int;
-
-axiom {:naming "MyFavoriteAxiom"} (forall i: int :: {f(i)} f(i) == i+1);
-
-var {:description "memory"} $Heap: [ref, name]any;
-
-var {:sort_of_like_a_trigger (forall i: int :: true)} Bla: [ref, name]any;
-
-procedure {:use_impl 1} foo(x : int) returns(n : int);
-
-implementation {:id 1} foo(x : int) returns(n : int)
-{
- block1: return;
-}
-
-implementation {:id 2} foo(x : int) returns(n : int)
-{
- block1: return;
-}
-
-type ref, any, name;
-
-
-// allow \" and other backslashes rather liberally:
-
-procedure
- {:myAttribute
- "h\n\"ello\"",
- "again",
- "and\\" a\"gain\"",
- again}
-P();
-
-const again: int;
+// RUN: %boogie -noVerify -print:- -env:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type {:sourcefile "test.ssc"} T; + +function {:source "test.scc"} f(int) returns (int); + +const {:description "The largest integer value"} unique MAXINT: int; + +axiom {:naming "MyFavoriteAxiom"} (forall i: int :: {f(i)} f(i) == i+1); + +var {:description "memory"} $Heap: [ref, name]any; + +var {:sort_of_like_a_trigger (forall i: int :: true)} Bla: [ref, name]any; + +procedure {:use_impl 1} foo(x : int) returns(n : int); + +implementation {:id 1} foo(x : int) returns(n : int) +{ + block1: return; +} + +implementation {:id 2} foo(x : int) returns(n : int) +{ + block1: return; +} + +type ref, any, name; + + +// allow \" and other backslashes rather liberally: + +procedure + {:myAttribute + "h\n\"ello\"", + "again", + "and\\" a\"gain\"", + again} +P(); + +const again: int; diff --git a/Test/test0/AttributeParsingErr.bpl b/Test/test0/AttributeParsingErr.bpl index 438f674d..9498daf1 100644 --- a/Test/test0/AttributeParsingErr.bpl +++ b/Test/test0/AttributeParsingErr.bpl @@ -1,25 +1,25 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type {:sourcefile "test.ssc"} {1} T;
-
-function {:source "test.scc"} {1} f(int) returns (int);
-
-const {:description "The largest integer value"} {1} unique MAXINT: int;
-
-axiom {:naming "MyFavoriteAxiom"} {1} (forall i: int :: {f(i)} f(i) == i+1);
-
-var {:description "memory"} {1} $Heap: [ref, name]any;
-
-var {(forall i: int :: true)} Bla: [ref, name]any;
-
-procedure {1} {:use_impl 1} foo(x : int) returns(n : int);
-
-implementation {1} {:id 1} foo(x : int) returns(n : int)
-{
- block1: return;
-}
-
-implementation {:id 2} {1} foo(x : int) returns(n : int)
-{
- block1: return;
-}
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type {:sourcefile "test.ssc"} {1} T; + +function {:source "test.scc"} {1} f(int) returns (int); + +const {:description "The largest integer value"} {1} unique MAXINT: int; + +axiom {:naming "MyFavoriteAxiom"} {1} (forall i: int :: {f(i)} f(i) == i+1); + +var {:description "memory"} {1} $Heap: [ref, name]any; + +var {(forall i: int :: true)} Bla: [ref, name]any; + +procedure {1} {:use_impl 1} foo(x : int) returns(n : int); + +implementation {1} {:id 1} foo(x : int) returns(n : int) +{ + block1: return; +} + +implementation {:id 2} {1} foo(x : int) returns(n : int) +{ + block1: return; +} diff --git a/Test/test0/AttributeResolution.bpl b/Test/test0/AttributeResolution.bpl index e5094932..17d79727 100644 --- a/Test/test0/AttributeResolution.bpl +++ b/Test/test0/AttributeResolution.bpl @@ -1,40 +1,40 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type {:sourcefile foo} T;
-
-function {:source bar} f(int) returns (int);
-
-const {:description baz} unique MAXINT: int;
-
-axiom {:naming qux} (forall i: int :: {f(ij)} f(i) == i+1);
-
-var {:description mux} $Heap: [ref, int]bool;
-
-var {:sort_of_like_a_trigger fux} Bla: [ref, int]bool;
-
-procedure {:use_impl bzzt} foo(x : int) returns(n : int);
-
-implementation {:id blt} foo(x : int) returns(n : int)
-{
- block1: return;
-}
-
-// ------ and here are various correct things
-
-
-
-const {:Correct hux0 + F(hux1)} hux0: int;
-
-function {:Correct F(hux0) + hux1} F(int) returns (int);
-
-axiom {:Correct F(hux0 + hux1)} true;
-
-var {:Correct hux0*hux1} hux1: int;
-
-procedure {:Correct hux0 - hux1} P();
-
-implementation {:Correct hux0 + hux1} {:AlsoCorrect "hello"} P()
-{
-}
-
-type ref;
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type {:sourcefile foo} T; + +function {:source bar} f(int) returns (int); + +const {:description baz} unique MAXINT: int; + +axiom {:naming qux} (forall i: int :: {f(ij)} f(i) == i+1); + +var {:description mux} $Heap: [ref, int]bool; + +var {:sort_of_like_a_trigger fux} Bla: [ref, int]bool; + +procedure {:use_impl bzzt} foo(x : int) returns(n : int); + +implementation {:id blt} foo(x : int) returns(n : int) +{ + block1: return; +} + +// ------ and here are various correct things + + + +const {:Correct hux0 + F(hux1)} hux0: int; + +function {:Correct F(hux0) + hux1} F(int) returns (int); + +axiom {:Correct F(hux0 + hux1)} true; + +var {:Correct hux0*hux1} hux1: int; + +procedure {:Correct hux0 - hux1} P(); + +implementation {:Correct hux0 + hux1} {:AlsoCorrect "hello"} P() +{ +} + +type ref; diff --git a/Test/test0/BadLabels0.bpl b/Test/test0/BadLabels0.bpl index b3f6f896..6b02a2d1 100644 --- a/Test/test0/BadLabels0.bpl +++ b/Test/test0/BadLabels0.bpl @@ -1,15 +1,15 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure Dup(y: int)
-{
- X:
- X: // error: duplicate label
- while (y < 100)
- {
- Y:
- }
- while (y < 1000)
- {
- Y: // error: duplicate label (labels must be unique in entire procedure body)
- }
-}
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure Dup(y: int) +{ + X: + X: // error: duplicate label + while (y < 100) + { + Y: + } + while (y < 1000) + { + Y: // error: duplicate label (labels must be unique in entire procedure body) + } +} diff --git a/Test/test0/BadLabels1.bpl b/Test/test0/BadLabels1.bpl index d0b4e396..dca59b57 100644 --- a/Test/test0/BadLabels1.bpl +++ b/Test/test0/BadLabels1.bpl @@ -1,83 +1,83 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure P0()
-{
- // these labels don't exist at all
- goto X; // error: undefined label
- goto Y; // error: undefined label
-}
-
-procedure P1(y: int)
-{
- goto X;
- while (y < 100)
- {
- X:
- }
-
- Q:
- if (y == 102) {
- A:
- goto Q;
- } else if (y == 104) {
- B:
- } else {
- C:
- goto K;
- }
-
- while (y < 1000)
- {
- K:
- goto A;
- if (y mod 2 == 0) {
- goto L;
- M:
- }
- goto K, L;
- L:
- if (*) {
- goto M;
- }
- }
- goto B;
-}
-
-
-procedure Break(n: int)
-{
- break; // error: break not inside a loop
- if (*) {
- break; // error: label-less break not inside a loop
- }
-
- A:
- if (*) {
- break A; // this is fine, since the break statement uses a label
- }
-
- B:
- assert 2 <= n;
- while (*) {
- break B; // error: B does not label a loop
- break;
- C: while (*) { assert n < 100; }
- break A; // error: A does not label a loop
- break C; // error: A does not label an enclosing loop
- F: break F; // error: F does not label an enclosing loop
- }
-
- D:
- while (*) {
- E:
- while (*) {
- if (*) {
- break;
- } else if (*) {
- if (*) { break E; }
- } else {
- break D;
- }
- }
- }
-}
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure P0() +{ + // these labels don't exist at all + goto X; // error: undefined label + goto Y; // error: undefined label +} + +procedure P1(y: int) +{ + goto X; + while (y < 100) + { + X: + } + + Q: + if (y == 102) { + A: + goto Q; + } else if (y == 104) { + B: + } else { + C: + goto K; + } + + while (y < 1000) + { + K: + goto A; + if (y mod 2 == 0) { + goto L; + M: + } + goto K, L; + L: + if (*) { + goto M; + } + } + goto B; +} + + +procedure Break(n: int) +{ + break; // error: break not inside a loop + if (*) { + break; // error: label-less break not inside a loop + } + + A: + if (*) { + break A; // this is fine, since the break statement uses a label + } + + B: + assert 2 <= n; + while (*) { + break B; // error: B does not label a loop + break; + C: while (*) { assert n < 100; } + break A; // error: A does not label a loop + break C; // error: A does not label an enclosing loop + F: break F; // error: F does not label an enclosing loop + } + + D: + while (*) { + E: + while (*) { + if (*) { + break; + } else if (*) { + if (*) { break E; } + } else { + break D; + } + } + } +} diff --git a/Test/test0/BadQuantifier.bpl b/Test/test0/BadQuantifier.bpl index db704a6e..9b020642 100644 --- a/Test/test0/BadQuantifier.bpl +++ b/Test/test0/BadQuantifier.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-function f(int) returns (bool);
-axiom (forall int x :: f(x) <== x >= 0);
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function f(int) returns (bool); +axiom (forall int x :: f(x) <== x >= 0); diff --git a/Test/test0/EmptyCallArgs.bpl b/Test/test0/EmptyCallArgs.bpl index 54b374d7..062dbcdf 100644 --- a/Test/test0/EmptyCallArgs.bpl +++ b/Test/test0/EmptyCallArgs.bpl @@ -1,22 +1,22 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff NoErrors.expect "%t"
-type C;
-
-procedure P(x:int, y:bool) returns (z:C);
-procedure Q<a>(x:int, y:a) returns (z:a);
-
-procedure CallP() {
- var x:int;
- var y:bool;
- var z:C;
-
- call z := P(x, y);
-}
-
-procedure CallQ() {
- var x:int;
- var y:bool;
- var z:bool;
-
- call z := Q(x, y);
-}
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff NoErrors.expect "%t" +type C; + +procedure P(x:int, y:bool) returns (z:C); +procedure Q<a>(x:int, y:a) returns (z:a); + +procedure CallP() { + var x:int; + var y:bool; + var z:C; + + call z := P(x, y); +} + +procedure CallQ() { + var x:int; + var y:bool; + var z:bool; + + call z := Q(x, y); +} diff --git a/Test/test0/LargeLiterals0.bpl b/Test/test0/LargeLiterals0.bpl index af9c02b4..2db94141 100644 --- a/Test/test0/LargeLiterals0.bpl +++ b/Test/test0/LargeLiterals0.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff NoErrors.expect "%t"
-// Test to parse large integer literals
-
-axiom 1234567890987654321 == 1234567890987654321;
-
-function f(int) returns (int);
-
-axiom f(1234567890987654321) == 0;
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff NoErrors.expect "%t" +// Test to parse large integer literals + +axiom 1234567890987654321 == 1234567890987654321; + +function f(int) returns (int); + +axiom f(1234567890987654321) == 0; diff --git a/Test/test0/LineParse.bpl b/Test/test0/LineParse.bpl index 76149ff6..8de34149 100644 --- a/Test/test0/LineParse.bpl +++ b/Test/test0/LineParse.bpl @@ -1,14 +1,14 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-#line
-#line
-#line 0
-#line 0
-
-#dontknow what this is No, I don't well, it's an error is what it is
-
-#define ASSERT(x) {if (!(x)) { crash(); }} // error: A B C . txt(12,0)
-
-// this is line 5; an error occurs on line 6:
- #line 10 // this is not even scanned like a pragma, because the # is not in column 0
-
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +#line +#line +#line 0 +#line 0 + +#dontknow what this is No, I don't well, it's an error is what it is + +#define ASSERT(x) {if (!(x)) { crash(); }} // error: A B C . txt(12,0) + +// this is line 5; an error occurs on line 6: + #line 10 // this is not even scanned like a pragma, because the # is not in column 0 + diff --git a/Test/test0/LineResolve.bpl b/Test/test0/LineResolve.bpl index 39bf9983..cca5c4a5 100644 --- a/Test/test0/LineResolve.bpl +++ b/Test/test0/LineResolve.bpl @@ -1,45 +1,45 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure P() {
-var x: int;
-x :=
-
- a+ // error: LineResolve.bpl(5,1)
-
- b+ // error: LineResolve.bpl(7,2)
-#line 12
-c+ // error: LineResolve.bpl(12,0)
- d+ // error: LineResolve.bpl(13,10)
-#line 12
-e+ // error: LineResolve.bpl(12,0)
-#line 2
-f+ // error: LineResolve.bpl(2,0)
-#line 1000
-#line 900
-g+ // error: LineResolve.bpl(900,0)
-
-#line 10 Abc.txt
-
- h+ // error: Abc.txt(11,3)
-
-i+ // error: Abc.txt(13,0)
-#line 98
-
-j+ // error: Abc.txt(99,0)
-
-#line 103 c:\Users\leino\Documents\Programs\MyClass.ssc
-
-k+ // error: c:\Users\leino\Documents\Programs\MyClass.ssc(104,0)
-
-#line -58
-
-#line 12 A B C . txt
-l+ // error: A B C . txt(12,0)
-
-0;
-}
-
-#line 100 LineResolve.bpl
-procedure ResolutionTest() {
- x := 0; // error: undeclared identifier (once upon a time, this used to crash Boogie)
-}
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure P() { +var x: int; +x := + + a+ // error: LineResolve.bpl(5,1) + + b+ // error: LineResolve.bpl(7,2) +#line 12 +c+ // error: LineResolve.bpl(12,0) + d+ // error: LineResolve.bpl(13,10) +#line 12 +e+ // error: LineResolve.bpl(12,0) +#line 2 +f+ // error: LineResolve.bpl(2,0) +#line 1000 +#line 900 +g+ // error: LineResolve.bpl(900,0) + +#line 10 Abc.txt + + h+ // error: Abc.txt(11,3) + +i+ // error: Abc.txt(13,0) +#line 98 + +j+ // error: Abc.txt(99,0) + +#line 103 c:\Users\leino\Documents\Programs\MyClass.ssc + +k+ // error: c:\Users\leino\Documents\Programs\MyClass.ssc(104,0) + +#line -58 + +#line 12 A B C . txt +l+ // error: A B C . txt(12,0) + +0; +} + +#line 100 LineResolve.bpl +procedure ResolutionTest() { + x := 0; // error: undeclared identifier (once upon a time, this used to crash Boogie) +} diff --git a/Test/test0/MapsResolutionErrors.bpl b/Test/test0/MapsResolutionErrors.bpl index 4cd5ff19..204cb7b0 100644 --- a/Test/test0/MapsResolutionErrors.bpl +++ b/Test/test0/MapsResolutionErrors.bpl @@ -1,30 +1,30 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-var m: []int;
-var p: <a>[]a;
-
-type C _;
-var bad: <a,b>[]C a; // error: b is not used
-
-function F<a>(a, int) returns (bool) { true }
-
-type Set _;
-function EmptySet<a>() returns (Set a);
-function G<a>(a, int) returns (Set a) { EmptySet() }
-
-function H<a>(int) returns (Set a);
-
-function {:inline true} K<a>(int) returns (Set a)
-{ EmptySet() }
-
-
-procedure P<a>(x: int, y: bool) returns (z: int, w: bool); // error: "a" is not used
-
-procedure Q<a>(x: int, y: bool) returns (z: int, w: a);
-procedure R<a>(x: int, y: bool) returns (z: int, w: Set a);
-procedure S<a>(x: a, y: bool) returns (z: int, w: Set a);
-
-
-function K2<a>(int) returns (Set a) // now ok
-{ EmptySet() }
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +var m: []int; +var p: <a>[]a; + +type C _; +var bad: <a,b>[]C a; // error: b is not used + +function F<a>(a, int) returns (bool) { true } + +type Set _; +function EmptySet<a>() returns (Set a); +function G<a>(a, int) returns (Set a) { EmptySet() } + +function H<a>(int) returns (Set a); + +function {:inline true} K<a>(int) returns (Set a) +{ EmptySet() } + + +procedure P<a>(x: int, y: bool) returns (z: int, w: bool); // error: "a" is not used + +procedure Q<a>(x: int, y: bool) returns (z: int, w: a); +procedure R<a>(x: int, y: bool) returns (z: int, w: Set a); +procedure S<a>(x: a, y: bool) returns (z: int, w: Set a); + + +function K2<a>(int) returns (Set a) // now ok +{ EmptySet() } diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl index b3677621..5d9f2aaa 100644 --- a/Test/test0/ModifiedBag.bpl +++ b/Test/test0/ModifiedBag.bpl @@ -1,373 +1,373 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff NoErrors.expect "%t"
-// ----------- BEGIN PRELUDE
-
-
-type elements;
-
-type name;
-
-const $CALL: name;
-
-const $REQ: name;
-
-const $ENS: name;
-
-const $PACK: name;
-
-const $UNPACK: name;
-
-const $HEAD: name;
-
-const $THROW: name;
-
-var $RefHeap: [ref, name]ref;
-
-var $IntHeap: [ref, name]int;
-
-var $RealHeap: [ref, name]real;
-
-var $BoolHeap: [ref, name]bool;
-
-var $ArrayHeap: [ref, name]elements;
-
-const $allocated: name;
-
-const $elements: name;
-
-function $ArrayLength(ref) returns (int);
-
-function $RefArrayGet(elements, int) returns (ref);
-
-function $RefArraySet(elements, int, ref) returns (elements);
-
-function $IntArrayGet(elements, int) returns (value: int);
-
-function $IntArraySet(elements, int, int) returns (elements);
-
-function $RealArrayGet(elements, int) returns (value: real);
-
-function $RealArraySet(elements, int, real) returns (elements);
-
-function $BoolArrayGet(elements, int) returns (value: bool);
-
-function $BoolArraySet(elements, int, bool) returns (elements);
-
-function $ArrayArrayGet(elements, int) returns (value: elements);
-
-function $ArrayArraySet(elements, int, elements) returns (elements);
-
-axiom (forall A: elements, i: int, x: ref :: $RefArrayGet($RefArraySet(A, i, x), i) == x);
-
-axiom (forall A: elements, i: int, j: int, x: ref :: i != j ==> $RefArrayGet($RefArraySet(A, i, x), j) == $RefArrayGet(A, j));
-
-axiom (forall A: elements, i: int, x: int :: $IntArrayGet($IntArraySet(A, i, x), i) == x);
-
-axiom (forall A: elements, i: int, j: int, x: int :: i != j ==> $IntArrayGet($IntArraySet(A, i, x), j) == $IntArrayGet(A, j));
-
-axiom (forall A: elements, i: int, x: real :: $RealArrayGet($RealArraySet(A, i, x), i) == x);
-
-axiom (forall A: elements, i: int, j: int, x: real :: i != j ==> $RealArrayGet($RealArraySet(A, i, x), j) == $RealArrayGet(A, j));
-
-axiom (forall A: elements, i: int, x: bool :: $BoolArrayGet($BoolArraySet(A, i, x), i) == x);
-
-axiom (forall A: elements, i: int, j: int, x: bool :: i != j ==> $BoolArrayGet($BoolArraySet(A, i, x), j) == $BoolArrayGet(A, j));
-
-axiom (forall A: elements, i: int, x: elements :: $ArrayArrayGet($ArrayArraySet(A, i, x), i) == x);
-
-axiom (forall A: elements, i: int, j: int, x: elements :: i != j ==> $ArrayArrayGet($ArrayArraySet(A, i, x), j) == $ArrayArrayGet(A, j));
-
-axiom (forall a: ref :: 0 <= $ArrayLength(a));
-
-function $typeof(ref) returns (name);
-
-function $BoolIs(bool, name) returns (bool);
-
-function $RealIs(real, name) returns (bool);
-
-function $IntIs(int, name) returns (bool);
-
-const System.Int16: name;
-
-const System.Int32: name;
-
-const System.Int64: name;
-
-const System.Int16.MinValue: int;
-
-const System.Int16.MaxValue: int;
-
-const System.Int32.MinValue: int;
-
-const System.Int32.MaxValue: int;
-
-const System.Int64.MinValue: int;
-
-const System.Int64.MaxValue: int;
-
-axiom System.Int64.MinValue < System.Int32.MinValue;
-
-axiom System.Int32.MinValue < System.Int16.MinValue;
-
-axiom System.Int16.MinValue < System.Int16.MaxValue;
-
-axiom System.Int16.MaxValue < System.Int32.MaxValue;
-
-axiom System.Int32.MaxValue < System.Int64.MaxValue;
-
-axiom (forall i: int :: $IntIs(i, System.Int16) <==> System.Int16.MinValue <= i && i <= System.Int16.MaxValue);
-
-axiom (forall i: int :: $IntIs(i, System.Int32) <==> System.Int32.MinValue <= i && i <= System.Int32.MaxValue);
-
-axiom (forall i: int :: $IntIs(i, System.Int64) <==> System.Int64.MinValue <= i && i <= System.Int64.MaxValue);
-
-function $RefIs(ref, name) returns (bool);
-
-axiom (forall o: ref, T: name :: $RefIs(o, T) <==> o == null || $typeof(o) <: T);
-
-axiom (forall o: ref, T: name :: $RefIs(o, $NotNull(T)) <==> o != null && $RefIs(o, T));
-
-axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $IntArray(T)) && a != null ==> $IntIs($IntArrayGet($ArrayHeap[a, $elements], i), T));
-
-axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $RealArray(T)) && a != null ==> $RealIs($RealArrayGet($ArrayHeap[a, $elements], i), T));
-
-axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $BoolArray(T)) && a != null ==> $BoolIs($BoolArrayGet($ArrayHeap[a, $elements], i), T));
-
-axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $RefArray(T)) && a != null ==> $RefIs($RefArrayGet($ArrayHeap[a, $elements], i), T));
-
-function $NotNull(name) returns (name);
-
-function $IntArray(name) returns (name);
-
-function $BoolArray(name) returns (name);
-
-function $RealArray(name) returns (name);
-
-function $RefArray(name) returns (name);
-// ----------- END PRELUDE
-const Bag.a: name;
-
-const Bag.n: name;
-
-const Bag: name;
-
-
-
-
-
-procedure Bag..ctor$(this: ref, initialElements$in: ref);
-
-
-
-
-
-
-procedure System.Object..ctor(this: ref);
-
-
-
-procedure System.Array.CopyTo$System.Array$System.Int32(this: ref, array$in: ref, index$in: int);
-
-
-
-procedure Bag..ctor$$System.Int32$System.Int32(this: ref, initialElements$in: ref, start$in: int, howMany$in: int);
- requires 0 <= howMany$in;
- requires start$in + howMany$in <= $ArrayLength(initialElements$in);
- modifies $IntHeap, $RefHeap;
-
-
-
-implementation Bag..ctor$$System.Int32$System.Int32(this: ref, initialElements$in: ref, start$in: int, howMany$in: int)
-{
- var initialElements: ref, start: int, howMany: int, stack0i: int, stack0o: ref, stack1i: int, stack2i: int;
-
- entry:
- assume $RefIs(this, $NotNull(Bag));
- initialElements := initialElements$in;
- assume $RefIs(initialElements, $NotNull($IntArray(System.Int32)));
- start := start$in;
- assume $IntIs(start, System.Int32);
- howMany := howMany$in;
- assume $IntIs(howMany, System.Int32);
- goto block165;
-
- block165:
- call System.Object..ctor(this);
- $IntHeap[this, Bag.n] := howMany;
- stack0i := howMany;
- havoc stack0o;
- assume $BoolHeap[stack0o, $allocated] == true && $ArrayLength(stack0o) == stack0i;
- $RefHeap[this, Bag.a] := stack0o;
- stack0o := $RefHeap[this, Bag.a];
- stack1i := 0;
- stack2i := start + howMany;
- call System.Array.Copy$System.Array$System.Int32$System.Array$System.Int32$System.Int32(initialElements, start, stack0o, stack1i, stack2i);
- assert this != null;
- assert 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);
- return;
-}
-
-
-
-procedure System.Array.Copy$System.Array$System.Int32$System.Array$System.Int32$System.Int32(sourceArray$in: ref, sourceIndex$in: int, destinationArray$in: ref, destinationIndex$in: int, length$in: int);
-
-
-
-procedure Bag.Add$System.Int32(this: ref, x$in: int);
- modifies $ArrayHeap, $IntHeap;
-
-
-
-implementation Bag.Add$System.Int32(this: ref, x$in: int)
-{
- var x: int, stack0i: int, stack1o: ref, stack1i: int, stack0b: bool, stack0o: ref, stack2i: int, b: ref;
-
- entry:
- assume $RefIs(this, $NotNull(Bag));
- x := x$in;
- assume $IntIs(x, System.Int32);
- assert this != null;
- assume 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);
- goto block205;
-
- block205:
- stack0i := $IntHeap[this, Bag.n];
- stack1o := $RefHeap[this, Bag.a];
- stack1i := $ArrayLength(stack1o);
- stack1i := stack1i;
- stack0b := stack0i != stack1i;
- goto trueblock208, falseblock206;
-
- trueblock208:
- assume stack0b == true;
-assume false;
-// goto block208;
-return;
-
- falseblock206:
- assume stack0b == false;
- goto block206;
-
- block206:
-// assert label-([$PACK@0:3:4425:0], $IntHeap[this, Bag.n] <= 2 * $ArrayLength($RefHeap[this, Bag.a]));
- stack0i := 2;
- stack1o := $RefHeap[this, Bag.a];
- stack1i := $ArrayLength(stack1o);
- stack1i := stack1i;
- stack0i := stack0i * stack1i;
- stack0i := stack0i;
- assert $IntHeap[this, Bag.n] <= stack0i;
-// havoc b;
-// assume $BoolHeap[b, $allocated] == true && $ArrayLength(b) == stack0i;
-// assert label-([$PACK@0:3:4427:0], $IntHeap[this, Bag.n] <= $ArrayLength(b));
-// stack0o := $RefHeap[this, Bag.a];
-// stack1i := 0;
-// call [$CALL@0:7:39:0] System.Array.CopyTo$System.Array$System.Int32(stack0o, b, stack1i);
-// $RefHeap[this, Bag.a] := b;
-// assert label-([$PACK@0:3:4428:0], $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]));
-// goto block208;
- return;
-
- block208:
- stack0o := $RefHeap[this, Bag.a];
- stack1i := $IntHeap[this, Bag.n];
- $ArrayHeap[stack0o, $elements] := $IntArraySet($ArrayHeap[stack0o, $elements], stack1i, x);
- stack0o := this;
- stack1o := stack0o;
- stack1i := $IntHeap[stack1o, Bag.n];
- stack2i := 1;
- stack1i := stack1i + stack2i;
- $IntHeap[stack0o, Bag.n] := stack1i;
- assert this != null;
- assert 0 <= $IntHeap[this, Bag.n];
- assert $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);
- return;
-
-}
-
-
-
-procedure Bag.ExtractMin(this: ref) returns ($result: int);
- modifies $IntHeap, $ArrayHeap;
-
-
-
-implementation Bag.ExtractMin(this: ref) returns ($result: int)
-{
- var m: int, mindex: int, i: int, stack0i: int, stack0b: bool, stack0o: ref, stack1o: ref, stack1i: int, stack2i: int, CS$00000003$00000000: int;
-
- entry:
- assume $RefIs(this, $NotNull(Bag));
- assert this != null;
- assume 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);
- goto block282;
-
- block282:
- m := 2147483647;
- mindex := 0;
- i := 1;
- goto block286;
-
- block285:
- stack0i := 1;
- stack0i := i + stack0i;
- i := stack0i;
- goto block286;
-
- block286:
- stack0i := $IntHeap[this, Bag.n];
- stack0b := i <= stack0i;
- goto trueblock283, falseblock287;
-
- trueblock283:
- assume stack0b == true;
- goto block283;
-
- falseblock287:
- assume stack0b == false;
- goto block287;
-
- block283:
- stack0o := $RefHeap[this, Bag.a];
- stack0i := $IntArrayGet($ArrayHeap[stack0o, $elements], i);
- stack0b := stack0i >= m;
- goto trueblock285, falseblock284;
-
- block287:
- stack0o := this;
- stack1o := stack0o;
- stack1i := $IntHeap[stack1o, Bag.n];
- stack2i := 1;
- stack1i := stack1i - stack2i;
- $IntHeap[stack0o, Bag.n] := stack1i;
- stack0o := $RefHeap[this, Bag.a];
- stack1o := $RefHeap[this, Bag.a];
- stack2i := $IntHeap[this, Bag.n];
- stack1i := $IntArrayGet($ArrayHeap[stack1o, $elements], stack2i);
- $ArrayHeap[stack0o, $elements] := $IntArraySet($ArrayHeap[stack0o, $elements], mindex, stack1i);
- CS$00000003$00000000 := m;
- goto block289;
-
- trueblock285:
- assume stack0b == true;
- goto block285;
-
- falseblock284:
- assume stack0b == false;
- goto block284;
-
- block284:
- mindex := i;
- stack0o := $RefHeap[this, Bag.a];
- m := $IntArrayGet($ArrayHeap[stack0o, $elements], i);
- goto block285;
-
- block289:
- $result := CS$00000003$00000000;
- assert this != null;
- assert 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);
- return;
-}
-
-type ref;
-const null : ref;
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff NoErrors.expect "%t" +// ----------- BEGIN PRELUDE + + +type elements; + +type name; + +const $CALL: name; + +const $REQ: name; + +const $ENS: name; + +const $PACK: name; + +const $UNPACK: name; + +const $HEAD: name; + +const $THROW: name; + +var $RefHeap: [ref, name]ref; + +var $IntHeap: [ref, name]int; + +var $RealHeap: [ref, name]real; + +var $BoolHeap: [ref, name]bool; + +var $ArrayHeap: [ref, name]elements; + +const $allocated: name; + +const $elements: name; + +function $ArrayLength(ref) returns (int); + +function $RefArrayGet(elements, int) returns (ref); + +function $RefArraySet(elements, int, ref) returns (elements); + +function $IntArrayGet(elements, int) returns (value: int); + +function $IntArraySet(elements, int, int) returns (elements); + +function $RealArrayGet(elements, int) returns (value: real); + +function $RealArraySet(elements, int, real) returns (elements); + +function $BoolArrayGet(elements, int) returns (value: bool); + +function $BoolArraySet(elements, int, bool) returns (elements); + +function $ArrayArrayGet(elements, int) returns (value: elements); + +function $ArrayArraySet(elements, int, elements) returns (elements); + +axiom (forall A: elements, i: int, x: ref :: $RefArrayGet($RefArraySet(A, i, x), i) == x); + +axiom (forall A: elements, i: int, j: int, x: ref :: i != j ==> $RefArrayGet($RefArraySet(A, i, x), j) == $RefArrayGet(A, j)); + +axiom (forall A: elements, i: int, x: int :: $IntArrayGet($IntArraySet(A, i, x), i) == x); + +axiom (forall A: elements, i: int, j: int, x: int :: i != j ==> $IntArrayGet($IntArraySet(A, i, x), j) == $IntArrayGet(A, j)); + +axiom (forall A: elements, i: int, x: real :: $RealArrayGet($RealArraySet(A, i, x), i) == x); + +axiom (forall A: elements, i: int, j: int, x: real :: i != j ==> $RealArrayGet($RealArraySet(A, i, x), j) == $RealArrayGet(A, j)); + +axiom (forall A: elements, i: int, x: bool :: $BoolArrayGet($BoolArraySet(A, i, x), i) == x); + +axiom (forall A: elements, i: int, j: int, x: bool :: i != j ==> $BoolArrayGet($BoolArraySet(A, i, x), j) == $BoolArrayGet(A, j)); + +axiom (forall A: elements, i: int, x: elements :: $ArrayArrayGet($ArrayArraySet(A, i, x), i) == x); + +axiom (forall A: elements, i: int, j: int, x: elements :: i != j ==> $ArrayArrayGet($ArrayArraySet(A, i, x), j) == $ArrayArrayGet(A, j)); + +axiom (forall a: ref :: 0 <= $ArrayLength(a)); + +function $typeof(ref) returns (name); + +function $BoolIs(bool, name) returns (bool); + +function $RealIs(real, name) returns (bool); + +function $IntIs(int, name) returns (bool); + +const System.Int16: name; + +const System.Int32: name; + +const System.Int64: name; + +const System.Int16.MinValue: int; + +const System.Int16.MaxValue: int; + +const System.Int32.MinValue: int; + +const System.Int32.MaxValue: int; + +const System.Int64.MinValue: int; + +const System.Int64.MaxValue: int; + +axiom System.Int64.MinValue < System.Int32.MinValue; + +axiom System.Int32.MinValue < System.Int16.MinValue; + +axiom System.Int16.MinValue < System.Int16.MaxValue; + +axiom System.Int16.MaxValue < System.Int32.MaxValue; + +axiom System.Int32.MaxValue < System.Int64.MaxValue; + +axiom (forall i: int :: $IntIs(i, System.Int16) <==> System.Int16.MinValue <= i && i <= System.Int16.MaxValue); + +axiom (forall i: int :: $IntIs(i, System.Int32) <==> System.Int32.MinValue <= i && i <= System.Int32.MaxValue); + +axiom (forall i: int :: $IntIs(i, System.Int64) <==> System.Int64.MinValue <= i && i <= System.Int64.MaxValue); + +function $RefIs(ref, name) returns (bool); + +axiom (forall o: ref, T: name :: $RefIs(o, T) <==> o == null || $typeof(o) <: T); + +axiom (forall o: ref, T: name :: $RefIs(o, $NotNull(T)) <==> o != null && $RefIs(o, T)); + +axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $IntArray(T)) && a != null ==> $IntIs($IntArrayGet($ArrayHeap[a, $elements], i), T)); + +axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $RealArray(T)) && a != null ==> $RealIs($RealArrayGet($ArrayHeap[a, $elements], i), T)); + +axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $BoolArray(T)) && a != null ==> $BoolIs($BoolArrayGet($ArrayHeap[a, $elements], i), T)); + +axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $RefArray(T)) && a != null ==> $RefIs($RefArrayGet($ArrayHeap[a, $elements], i), T)); + +function $NotNull(name) returns (name); + +function $IntArray(name) returns (name); + +function $BoolArray(name) returns (name); + +function $RealArray(name) returns (name); + +function $RefArray(name) returns (name); +// ----------- END PRELUDE +const Bag.a: name; + +const Bag.n: name; + +const Bag: name; + + + + + +procedure Bag..ctor$(this: ref, initialElements$in: ref); + + + + + + +procedure System.Object..ctor(this: ref); + + + +procedure System.Array.CopyTo$System.Array$System.Int32(this: ref, array$in: ref, index$in: int); + + + +procedure Bag..ctor$$System.Int32$System.Int32(this: ref, initialElements$in: ref, start$in: int, howMany$in: int); + requires 0 <= howMany$in; + requires start$in + howMany$in <= $ArrayLength(initialElements$in); + modifies $IntHeap, $RefHeap; + + + +implementation Bag..ctor$$System.Int32$System.Int32(this: ref, initialElements$in: ref, start$in: int, howMany$in: int) +{ + var initialElements: ref, start: int, howMany: int, stack0i: int, stack0o: ref, stack1i: int, stack2i: int; + + entry: + assume $RefIs(this, $NotNull(Bag)); + initialElements := initialElements$in; + assume $RefIs(initialElements, $NotNull($IntArray(System.Int32))); + start := start$in; + assume $IntIs(start, System.Int32); + howMany := howMany$in; + assume $IntIs(howMany, System.Int32); + goto block165; + + block165: + call System.Object..ctor(this); + $IntHeap[this, Bag.n] := howMany; + stack0i := howMany; + havoc stack0o; + assume $BoolHeap[stack0o, $allocated] == true && $ArrayLength(stack0o) == stack0i; + $RefHeap[this, Bag.a] := stack0o; + stack0o := $RefHeap[this, Bag.a]; + stack1i := 0; + stack2i := start + howMany; + call System.Array.Copy$System.Array$System.Int32$System.Array$System.Int32$System.Int32(initialElements, start, stack0o, stack1i, stack2i); + assert this != null; + assert 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]); + return; +} + + + +procedure System.Array.Copy$System.Array$System.Int32$System.Array$System.Int32$System.Int32(sourceArray$in: ref, sourceIndex$in: int, destinationArray$in: ref, destinationIndex$in: int, length$in: int); + + + +procedure Bag.Add$System.Int32(this: ref, x$in: int); + modifies $ArrayHeap, $IntHeap; + + + +implementation Bag.Add$System.Int32(this: ref, x$in: int) +{ + var x: int, stack0i: int, stack1o: ref, stack1i: int, stack0b: bool, stack0o: ref, stack2i: int, b: ref; + + entry: + assume $RefIs(this, $NotNull(Bag)); + x := x$in; + assume $IntIs(x, System.Int32); + assert this != null; + assume 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]); + goto block205; + + block205: + stack0i := $IntHeap[this, Bag.n]; + stack1o := $RefHeap[this, Bag.a]; + stack1i := $ArrayLength(stack1o); + stack1i := stack1i; + stack0b := stack0i != stack1i; + goto trueblock208, falseblock206; + + trueblock208: + assume stack0b == true; +assume false; +// goto block208; +return; + + falseblock206: + assume stack0b == false; + goto block206; + + block206: +// assert label-([$PACK@0:3:4425:0], $IntHeap[this, Bag.n] <= 2 * $ArrayLength($RefHeap[this, Bag.a])); + stack0i := 2; + stack1o := $RefHeap[this, Bag.a]; + stack1i := $ArrayLength(stack1o); + stack1i := stack1i; + stack0i := stack0i * stack1i; + stack0i := stack0i; + assert $IntHeap[this, Bag.n] <= stack0i; +// havoc b; +// assume $BoolHeap[b, $allocated] == true && $ArrayLength(b) == stack0i; +// assert label-([$PACK@0:3:4427:0], $IntHeap[this, Bag.n] <= $ArrayLength(b)); +// stack0o := $RefHeap[this, Bag.a]; +// stack1i := 0; +// call [$CALL@0:7:39:0] System.Array.CopyTo$System.Array$System.Int32(stack0o, b, stack1i); +// $RefHeap[this, Bag.a] := b; +// assert label-([$PACK@0:3:4428:0], $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a])); +// goto block208; + return; + + block208: + stack0o := $RefHeap[this, Bag.a]; + stack1i := $IntHeap[this, Bag.n]; + $ArrayHeap[stack0o, $elements] := $IntArraySet($ArrayHeap[stack0o, $elements], stack1i, x); + stack0o := this; + stack1o := stack0o; + stack1i := $IntHeap[stack1o, Bag.n]; + stack2i := 1; + stack1i := stack1i + stack2i; + $IntHeap[stack0o, Bag.n] := stack1i; + assert this != null; + assert 0 <= $IntHeap[this, Bag.n]; + assert $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]); + return; + +} + + + +procedure Bag.ExtractMin(this: ref) returns ($result: int); + modifies $IntHeap, $ArrayHeap; + + + +implementation Bag.ExtractMin(this: ref) returns ($result: int) +{ + var m: int, mindex: int, i: int, stack0i: int, stack0b: bool, stack0o: ref, stack1o: ref, stack1i: int, stack2i: int, CS$00000003$00000000: int; + + entry: + assume $RefIs(this, $NotNull(Bag)); + assert this != null; + assume 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]); + goto block282; + + block282: + m := 2147483647; + mindex := 0; + i := 1; + goto block286; + + block285: + stack0i := 1; + stack0i := i + stack0i; + i := stack0i; + goto block286; + + block286: + stack0i := $IntHeap[this, Bag.n]; + stack0b := i <= stack0i; + goto trueblock283, falseblock287; + + trueblock283: + assume stack0b == true; + goto block283; + + falseblock287: + assume stack0b == false; + goto block287; + + block283: + stack0o := $RefHeap[this, Bag.a]; + stack0i := $IntArrayGet($ArrayHeap[stack0o, $elements], i); + stack0b := stack0i >= m; + goto trueblock285, falseblock284; + + block287: + stack0o := this; + stack1o := stack0o; + stack1i := $IntHeap[stack1o, Bag.n]; + stack2i := 1; + stack1i := stack1i - stack2i; + $IntHeap[stack0o, Bag.n] := stack1i; + stack0o := $RefHeap[this, Bag.a]; + stack1o := $RefHeap[this, Bag.a]; + stack2i := $IntHeap[this, Bag.n]; + stack1i := $IntArrayGet($ArrayHeap[stack1o, $elements], stack2i); + $ArrayHeap[stack0o, $elements] := $IntArraySet($ArrayHeap[stack0o, $elements], mindex, stack1i); + CS$00000003$00000000 := m; + goto block289; + + trueblock285: + assume stack0b == true; + goto block285; + + falseblock284: + assume stack0b == false; + goto block284; + + block284: + mindex := i; + stack0o := $RefHeap[this, Bag.a]; + m := $IntArrayGet($ArrayHeap[stack0o, $elements], i); + goto block285; + + block289: + $result := CS$00000003$00000000; + assert this != null; + assert 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]); + return; +} + +type ref; +const null : ref; diff --git a/Test/test0/Orderings.bpl b/Test/test0/Orderings.bpl index 0d55ed27..1cf900b6 100644 --- a/Test/test0/Orderings.bpl +++ b/Test/test0/Orderings.bpl @@ -1,22 +1,22 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-type C;
-
-const c:int extends a;
-const d:int extends a complete;
-const e:int extends unique a, b;
-const f:int extends complete;
-
-const a:int;
-const b:int;
-
-const g:int extends x; // error: undeclared parent
-
-const c0:C;
-const c1:C extends c0, c0; // error: parent mentioned twice
-const c2:C extends c2; // error: constant as its own parent
-
-const h:int extends y; // error: variable cannot be parent
-
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +type C; + +const c:int extends a; +const d:int extends a complete; +const e:int extends unique a, b; +const f:int extends complete; + +const a:int; +const b:int; + +const g:int extends x; // error: undeclared parent + +const c0:C; +const c1:C extends c0, c0; // error: parent mentioned twice +const c2:C extends c2; // error: constant as its own parent + +const h:int extends y; // error: variable cannot be parent + var y:int;
\ No newline at end of file diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl index c79eff80..faa6bfd1 100644 --- a/Test/test0/PrettyPrint.bpl +++ b/Test/test0/PrettyPrint.bpl @@ -1,67 +1,67 @@ -// RUN: %boogie -pretty:0 -noVerify -printInstrumented "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const x: int;
-const y: int;
-const z: int;
-const r: real;
-const s: real;
-const t: real;
-const P: bool;
-const Q: bool;
-const R: bool;
-
-axiom x * (y + z) == x + (y * z);
-axiom (x * y) + z == (x + y) * z;
-
-axiom x * y * z == (x * (y * z));
-axiom (x * y) * (z * x) == (x * y) * z;
-
-axiom x div y div z == (x div (y div z));
-axiom (x div y) div (z div x) == (x div y) div z;
-
-axiom x + y mod z == ((y mod z) + x);
-axiom (x + y) mod z == (x mod z) + (y mod z);
-
-axiom x / y / z == (x / (y / z));
-axiom (x / y) / (z / x) == (x / y) / z;
-axiom x / s / z == (x / (s / z));
-axiom (x / s) / (z / x) == (x / s) / z;
-axiom r / s / t == (r / (s / t));
-axiom (r / s) / (t / r) == (r / s) / t;
-
-axiom ((r * s) / t) == r * s / t;
-axiom ((r / s) * t) == (r / s) * t;
-
-axiom (r * s) ** t == (r ** t) * (s ** t);
-axiom r ** (s + t) == r ** s * r ** t;
-
-axiom int(real(x)) == x;
-axiom r >= 0.0 ==> real(int(r)) <= r;
-axiom int(0e-3 - 0.02) == 0;
-axiom int(0e2 - 3.5e1) == -35;
-axiom int(27e-1) == 2;
-
-axiom x - y - z == (x - (y - z));
-axiom (x - y) - (z - x) == (x - y) - z;
-
-axiom x + y - z - x + y == 0;
-axiom ((((x + y) - z) - x) + y) == (x + (y - (z - (x + y))));
-
-axiom P ==> Q ==> R <==> (P ==> (Q ==> R));
-axiom ((P ==> Q) ==> (R ==> P)) == ((P ==> Q) ==> R);
-
-axiom P <==> Q <==> R;
-axiom P ==> Q <==> Q ==> R <==> R ==> P;
-
-axiom (P && Q) || (Q && R);
-axiom (P || Q) && (Q || R);
-axiom (P || Q) || (Q || R);
-axiom (P && Q) && (Q && R);
-
-// -------------- quantifier key-value decorations
-
-function f(int) returns (int);
-
-axiom (forall x: int :: {:xname "hello"}
- { :weight 5} {f(x+x)} {:ValueFunc f(x+1) } {f(x)*f(x)} {:nopats f(x+x+x)}
- f(f(x)) < 200);
+// RUN: %boogie -pretty:0 -noVerify -printInstrumented "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +const x: int; +const y: int; +const z: int; +const r: real; +const s: real; +const t: real; +const P: bool; +const Q: bool; +const R: bool; + +axiom x * (y + z) == x + (y * z); +axiom (x * y) + z == (x + y) * z; + +axiom x * y * z == (x * (y * z)); +axiom (x * y) * (z * x) == (x * y) * z; + +axiom x div y div z == (x div (y div z)); +axiom (x div y) div (z div x) == (x div y) div z; + +axiom x + y mod z == ((y mod z) + x); +axiom (x + y) mod z == (x mod z) + (y mod z); + +axiom x / y / z == (x / (y / z)); +axiom (x / y) / (z / x) == (x / y) / z; +axiom x / s / z == (x / (s / z)); +axiom (x / s) / (z / x) == (x / s) / z; +axiom r / s / t == (r / (s / t)); +axiom (r / s) / (t / r) == (r / s) / t; + +axiom ((r * s) / t) == r * s / t; +axiom ((r / s) * t) == (r / s) * t; + +axiom (r * s) ** t == (r ** t) * (s ** t); +axiom r ** (s + t) == r ** s * r ** t; + +axiom int(real(x)) == x; +axiom r >= 0.0 ==> real(int(r)) <= r; +axiom int(0e-3 - 0.02) == 0; +axiom int(0e2 - 3.5e1) == -35; +axiom int(27e-1) == 2; + +axiom x - y - z == (x - (y - z)); +axiom (x - y) - (z - x) == (x - y) - z; + +axiom x + y - z - x + y == 0; +axiom ((((x + y) - z) - x) + y) == (x + (y - (z - (x + y)))); + +axiom P ==> Q ==> R <==> (P ==> (Q ==> R)); +axiom ((P ==> Q) ==> (R ==> P)) == ((P ==> Q) ==> R); + +axiom P <==> Q <==> R; +axiom P ==> Q <==> Q ==> R <==> R ==> P; + +axiom (P && Q) || (Q && R); +axiom (P || Q) && (Q || R); +axiom (P || Q) || (Q || R); +axiom (P && Q) && (Q && R); + +// -------------- quantifier key-value decorations + +function f(int) returns (int); + +axiom (forall x: int :: {:xname "hello"} + { :weight 5} {f(x+x)} {:ValueFunc f(x+1) } {f(x)*f(x)} {:nopats f(x+x+x)} + f(f(x)) < 200); diff --git a/Test/test0/Prog0.bpl b/Test/test0/Prog0.bpl index d9e467ec..51383660 100644 --- a/Test/test0/Prog0.bpl +++ b/Test/test0/Prog0.bpl @@ -1,53 +1,53 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff NoErrors.expect "%t"
-// BoogiePL Examples
-
-type elements;
-
-var x:int; var y:real; var z:ref; // Variables
-var x.3:bool; var $ar:ref; // Names can have glyphs
-
-const a, b, c:int; // Consts
-
-function f (int, int) returns (int); // Function with arity 2
-function g ( int , int) returns (int); // Function with arity 2
-function h(int,int) returns (int); // Function with arity 2
-
-function m (int) returns (int); // Function with arity 1
-function k(int) returns (int); // Function with arity 1
-
-
-axiom
- (forall x : int :: f(g(h(a,b),c),x) > 100) ;
-
-procedure p (x:int, y:ref) returns (z:int, w:[int,ref]ref, q:int);
-
-
-procedure q(x:int, y:ref) returns (z:int) // Procedure with output params
- requires x > 0; // as many req/ens/mod you want
- ensures z > 3;
- ensures old(x) == 1; // old only in ensures..
- modifies z,y,$ar;
-{
- var t, s: int;
- var r: [int,ref]ref;
-
- start: // one label per block
- t := x;
- s := t;
- z := x + t;
- call s, r,z := p(t,r[3,null]); // procedure call with mutiple returns
- goto continue, end ; // as many labels as you like
-
- continue:
- return; // ends control flow
-
- end:
- goto start;
-}
-
-procedure s(e: elements) { L: return; }
-procedure r (x:int, y:ref) returns (z:int);
-
-type ref;
-const null : ref;
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff NoErrors.expect "%t" +// BoogiePL Examples + +type elements; + +var x:int; var y:real; var z:ref; // Variables +var x.3:bool; var $ar:ref; // Names can have glyphs + +const a, b, c:int; // Consts + +function f (int, int) returns (int); // Function with arity 2 +function g ( int , int) returns (int); // Function with arity 2 +function h(int,int) returns (int); // Function with arity 2 + +function m (int) returns (int); // Function with arity 1 +function k(int) returns (int); // Function with arity 1 + + +axiom + (forall x : int :: f(g(h(a,b),c),x) > 100) ; + +procedure p (x:int, y:ref) returns (z:int, w:[int,ref]ref, q:int); + + +procedure q(x:int, y:ref) returns (z:int) // Procedure with output params + requires x > 0; // as many req/ens/mod you want + ensures z > 3; + ensures old(x) == 1; // old only in ensures.. + modifies z,y,$ar; +{ + var t, s: int; + var r: [int,ref]ref; + + start: // one label per block + t := x; + s := t; + z := x + t; + call s, r,z := p(t,r[3,null]); // procedure call with mutiple returns + goto continue, end ; // as many labels as you like + + continue: + return; // ends control flow + + end: + goto start; +} + +procedure s(e: elements) { L: return; } +procedure r (x:int, y:ref) returns (z:int); + +type ref; +const null : ref; diff --git a/Test/test0/Quoting.bpl b/Test/test0/Quoting.bpl index bf1f268e..db8ccf92 100644 --- a/Test/test0/Quoting.bpl +++ b/Test/test0/Quoting.bpl @@ -1,18 +1,18 @@ -// RUN: %boogie -noVerify -print:- -env:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function \true() returns(bool);
-
-type \procedure;
-procedure \old(\any : \procedure) returns(\var : \procedure)
-{
- var \modifies : \procedure;
- \modifies := \any;
- \var := \modifies;
-}
-
-procedure qux(a : \procedure)
-{
- var \var : \procedure; var x : bool;
- call \var := \old(a);
- x := \true();
-}
+// RUN: %boogie -noVerify -print:- -env:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +function \true() returns(bool); + +type \procedure; +procedure \old(\any : \procedure) returns(\var : \procedure) +{ + var \modifies : \procedure; + \modifies := \any; + \var := \modifies; +} + +procedure qux(a : \procedure) +{ + var \var : \procedure; var x : bool; + call \var := \old(a); + x := \true(); +} diff --git a/Test/test0/SeparateVerification0.bpl b/Test/test0/SeparateVerification0.bpl index a5c3962a..93324437 100644 --- a/Test/test0/SeparateVerification0.bpl +++ b/Test/test0/SeparateVerification0.bpl @@ -1,27 +1,27 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// RUN: %boogie -noVerify "%s" "%s" > "%t"
-// RUN: %diff NoErrors.expect "%t"
-// RUN: %boogie -noVerify "%s" "%s" SeparateVerification1.bpl > "%t"
-// RUN: %diff NoErrors.expect "%t"
-// need to include this file twice for it to include all necessary declarations
-
-#if FILE_0
-const x: int;
-#else
-const y: int;
-#endif
-
-#if FILE_1
-axiom x == 12;
-procedure Q();
-#else
-axiom y == 7;
-#endif
-
-// duplicates of :extern's are fine (Boogie keeps the non-:extern or chooses arbitrarily among the :extern's)
-type {:extern} T;
-const {:extern} C: int;
-function {:extern} F(): int;
-var {:extern} n: int;
-procedure {:extern} P(inconsistentParameterButThatIsOkayBecauseTheExternIsIgnored: int);
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// RUN: %boogie -noVerify "%s" "%s" > "%t" +// RUN: %diff NoErrors.expect "%t" +// RUN: %boogie -noVerify "%s" "%s" SeparateVerification1.bpl > "%t" +// RUN: %diff NoErrors.expect "%t" +// need to include this file twice for it to include all necessary declarations + +#if FILE_0 +const x: int; +#else +const y: int; +#endif + +#if FILE_1 +axiom x == 12; +procedure Q(); +#else +axiom y == 7; +#endif + +// duplicates of :extern's are fine (Boogie keeps the non-:extern or chooses arbitrarily among the :extern's) +type {:extern} T; +const {:extern} C: int; +function {:extern} F(): int; +var {:extern} n: int; +procedure {:extern} P(inconsistentParameterButThatIsOkayBecauseTheExternIsIgnored: int); diff --git a/Test/test0/SeparateVerification1.bpl b/Test/test0/SeparateVerification1.bpl index 5956828f..d06aa043 100644 --- a/Test/test0/SeparateVerification1.bpl +++ b/Test/test0/SeparateVerification1.bpl @@ -1,21 +1,21 @@ -// RUN: %boogie -noVerify "%s" SeparateVerification0.bpl > "%t"
-// RUN: %diff "%s.expect" "%t"
-// to be used with SeparateVerification0.bpl
-
-// x and y are declared in SeparateVerification0.bpl
-axiom x + y <= 100;
-
-// these are declared as :extern as SeparateVerification0.bpl
-type T;
-const C: int;
-function F(): int;
-var n: int;
-procedure P();
-procedure {:extern} Q(x: int);
-
-procedure Main() {
- call P(); // note, calling the parameter-less non-extern P (an extern and a non-extern
- // declaration of the same name are usually mostly identical declarations,
- // but Boogie allows them to be different, because it ignores the extern ones)
- call Q(); // ditto
-}
+// RUN: %boogie -noVerify "%s" SeparateVerification0.bpl > "%t" +// RUN: %diff "%s.expect" "%t" +// to be used with SeparateVerification0.bpl + +// x and y are declared in SeparateVerification0.bpl +axiom x + y <= 100; + +// these are declared as :extern as SeparateVerification0.bpl +type T; +const C: int; +function F(): int; +var n: int; +procedure P(); +procedure {:extern} Q(x: int); + +procedure Main() { + call P(); // note, calling the parameter-less non-extern P (an extern and a non-extern + // declaration of the same name are usually mostly identical declarations, + // but Boogie allows them to be different, because it ignores the extern ones) + call Q(); // ditto +} diff --git a/Test/test0/Triggers0.bpl b/Test/test0/Triggers0.bpl index 0113b992..34e89727 100644 --- a/Test/test0/Triggers0.bpl +++ b/Test/test0/Triggers0.bpl @@ -1,17 +1,17 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Trigger errors
-
-function f(int, int) returns (int);
-function P(int, int) returns (bool);
-
-// -------------- tests specific to pattern exclusions
-
-axiom (forall x: int ::
- {:nopats f(x,10) }
- { : nopats f(x,10) }
- f(x,10) == 3);
-
-axiom (forall x: int ::
- {:nopats f(x,10), f(x,x) } // error: a pattern exclusion can only mention one expression
- f(x,10) == 3);
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// Trigger errors + +function f(int, int) returns (int); +function P(int, int) returns (bool); + +// -------------- tests specific to pattern exclusions + +axiom (forall x: int :: + {:nopats f(x,10) } + { : nopats f(x,10) } + f(x,10) == 3); + +axiom (forall x: int :: + {:nopats f(x,10), f(x,x) } // error: a pattern exclusion can only mention one expression + f(x,10) == 3); diff --git a/Test/test0/Triggers1.bpl b/Test/test0/Triggers1.bpl index 12d734be..7ab1c191 100644 --- a/Test/test0/Triggers1.bpl +++ b/Test/test0/Triggers1.bpl @@ -1,129 +1,129 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Trigger errors
-
-function f(int, int) returns (int);
-function P(int, int) returns (bool);
-
-axiom (forall x: int ::
- { f(x,10) && f(x,9) } // error: && not allowed
- f(x,10) == 3);
-
-axiom (forall x: int ::
- { ((((f(x,10) || f(x,9))))) } // error: || not allowed
- f(x,10) == 3);
-
-axiom (forall x: int ::
- { !f(x,10) } // error: ! not allowed
- f(x,10) == 3);
-
-axiom (forall x: int ::
- { (!f(x,10)) } // error: ! not allowed
- f(x,10) == 3);
-
-axiom (forall x: int ::
- { P(x,10) ==> P(20,x) } // error: ==> not allowed
- f(x,10) == 3);
-
-axiom (forall x: int ::
- { P(x,10) <==> P(20,x) } // error: <==> not allowed
- f(x,10) == 3);
-
-
-axiom (forall x: int ::
- { f(x,10) == 3 } // error: == not allowed
- f(x,10) == 3);
-
-axiom (forall x: int ::
- { f(x,10) < 3 } // error: < not allowed
- f(x,10) == 3);
-
-
-axiom (forall x: int ::
- { f(x,10) + f(x,x) != 3 } // yes, != is allowed
- f(x,10) == 3);
-
-axiom (forall b: bool ::
- { (forall y: int :: b) } // error: quantifiers not allowed
- b);
-
-// -------------- tests of free variables
-
-const g: int;
-
-axiom (forall x: int ::
- { false, 6 } // error: does not mention "x"
- x < x + 1);
-
-axiom (forall x: int ::
- { false, x+1, 6 } // allowed
- x < x + 1);
-
-axiom (forall x: int, y: int ::
- { x+1 } // error: does not mention "y"
- { y+1 } // error: does not mention "x"
- x < y + 1);
-
-axiom (forall x: int ::
- { g+x != 65 } // allowed
- x < x + 1);
-
-axiom (forall x: int ::
- { x } // "x" by itself is not a good trigger
- x < x + 1);
-
-//axiom (forall x: any :: // PR: removed for the time being
-// { cast(x,int) } // can't fool me, still not allowed
-// x == x );
-
-// --- multiple triggers
-
-axiom (forall x: int, y: int, z: int ::
- { x+y+z } // good
- { x+y, y+z } // also good
- { f(f(x,y),y) } // error: does not mention z
- x == x );
-
-// --- multi-triggers
-
-axiom (forall x: int, y: int, z: int ::
- { f(x,x), f(y,y), f(z,z) } // good
- f(x,y) < f(y,z) );
-
-// --- pattern exclusion
-
-axiom (forall x: int, y: int ::
- {:nopats x } // error: "x" by itself is not allowed here either
- {:nopats g } // error: "g" by itself is not allowed here either
- x < y);
-
-axiom (forall x: int, y: int ::
- {:nopats f(g,g) } // but it is okay not to mention the bound variables (in a pattern exclusion)
- x < y);
-
-// --- merging of nested quantifiers (disabled unless both have no triggers)
-
-axiom (forall x:int :: (forall y:int :: { f(x,y) } f(x,y) > 0)); // OK, but no merging - outer quantifier has no trigger
-axiom (forall x:int :: (forall y:int :: { f(x,x) } f(x,x) > 0)); // error
-axiom (forall x:int :: (forall y:int :: { f(y,y) } f(y,y) > 0)); // OK - no merging
-
-// three levels
-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y) } f(y,y) > 0))); // error - z not mentioned
-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,z) } f(y,y) > 0))); // OK - only outer two quantifiers are merged
-//axiom (forall x:int :: (forall y:int :: (forall z:int :: f(y,y) > 0))); // OK - all three are merged
-axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y), f(y,z) } f(y,y) > 0))); // OK - but not a trigger for outer x,y (which get merged)
-
-// --- no free variables
-
-var h0: int;
-var h1: [ref,ref]int;
-
-axiom (forall o: ref, f: ref :: h1[o,f] // error: cannot mention free variable "h1"
- < h0); // error: cannot mention free variable "h0"
-
-const c0: int;
-const c1: [ref,ref]int;
-
-axiom (forall o: ref, f: ref :: c1[o,f] < c0);
-
-type ref;
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// Trigger errors + +function f(int, int) returns (int); +function P(int, int) returns (bool); + +axiom (forall x: int :: + { f(x,10) && f(x,9) } // error: && not allowed + f(x,10) == 3); + +axiom (forall x: int :: + { ((((f(x,10) || f(x,9))))) } // error: || not allowed + f(x,10) == 3); + +axiom (forall x: int :: + { !f(x,10) } // error: ! not allowed + f(x,10) == 3); + +axiom (forall x: int :: + { (!f(x,10)) } // error: ! not allowed + f(x,10) == 3); + +axiom (forall x: int :: + { P(x,10) ==> P(20,x) } // error: ==> not allowed + f(x,10) == 3); + +axiom (forall x: int :: + { P(x,10) <==> P(20,x) } // error: <==> not allowed + f(x,10) == 3); + + +axiom (forall x: int :: + { f(x,10) == 3 } // error: == not allowed + f(x,10) == 3); + +axiom (forall x: int :: + { f(x,10) < 3 } // error: < not allowed + f(x,10) == 3); + + +axiom (forall x: int :: + { f(x,10) + f(x,x) != 3 } // yes, != is allowed + f(x,10) == 3); + +axiom (forall b: bool :: + { (forall y: int :: b) } // error: quantifiers not allowed + b); + +// -------------- tests of free variables + +const g: int; + +axiom (forall x: int :: + { false, 6 } // error: does not mention "x" + x < x + 1); + +axiom (forall x: int :: + { false, x+1, 6 } // allowed + x < x + 1); + +axiom (forall x: int, y: int :: + { x+1 } // error: does not mention "y" + { y+1 } // error: does not mention "x" + x < y + 1); + +axiom (forall x: int :: + { g+x != 65 } // allowed + x < x + 1); + +axiom (forall x: int :: + { x } // "x" by itself is not a good trigger + x < x + 1); + +//axiom (forall x: any :: // PR: removed for the time being +// { cast(x,int) } // can't fool me, still not allowed +// x == x ); + +// --- multiple triggers + +axiom (forall x: int, y: int, z: int :: + { x+y+z } // good + { x+y, y+z } // also good + { f(f(x,y),y) } // error: does not mention z + x == x ); + +// --- multi-triggers + +axiom (forall x: int, y: int, z: int :: + { f(x,x), f(y,y), f(z,z) } // good + f(x,y) < f(y,z) ); + +// --- pattern exclusion + +axiom (forall x: int, y: int :: + {:nopats x } // error: "x" by itself is not allowed here either + {:nopats g } // error: "g" by itself is not allowed here either + x < y); + +axiom (forall x: int, y: int :: + {:nopats f(g,g) } // but it is okay not to mention the bound variables (in a pattern exclusion) + x < y); + +// --- merging of nested quantifiers (disabled unless both have no triggers) + +axiom (forall x:int :: (forall y:int :: { f(x,y) } f(x,y) > 0)); // OK, but no merging - outer quantifier has no trigger +axiom (forall x:int :: (forall y:int :: { f(x,x) } f(x,x) > 0)); // error +axiom (forall x:int :: (forall y:int :: { f(y,y) } f(y,y) > 0)); // OK - no merging + +// three levels +axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y) } f(y,y) > 0))); // error - z not mentioned +axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,z) } f(y,y) > 0))); // OK - only outer two quantifiers are merged +//axiom (forall x:int :: (forall y:int :: (forall z:int :: f(y,y) > 0))); // OK - all three are merged +axiom (forall x:int :: (forall y:int :: (forall z:int :: { f(x,y), f(y,z) } f(y,y) > 0))); // OK - but not a trigger for outer x,y (which get merged) + +// --- no free variables + +var h0: int; +var h1: [ref,ref]int; + +axiom (forall o: ref, f: ref :: h1[o,f] // error: cannot mention free variable "h1" + < h0); // error: cannot mention free variable "h0" + +const c0: int; +const c1: [ref,ref]int; + +axiom (forall o: ref, f: ref :: c1[o,f] < c0); + +type ref; diff --git a/Test/test0/Types0.bpl b/Test/test0/Types0.bpl index 62385acf..d606951b 100644 --- a/Test/test0/Types0.bpl +++ b/Test/test0/Types0.bpl @@ -1,10 +1,10 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type T, U;
-type V;
-
-function f([U,V]T, int) returns (U);
-function g(x: [U,V]T, y: int) returns (z: U);
-function h([U,V]T: int, y: int) returns (z: U); // parse error
-function k(T: int, y: int) returns (U: [any]int);
-function l(x) returns (int); // resolve error
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type T, U; +type V; + +function f([U,V]T, int) returns (U); +function g(x: [U,V]T, y: int) returns (z: U); +function h([U,V]T: int, y: int) returns (z: U); // parse error +function k(T: int, y: int) returns (U: [any]int); +function l(x) returns (int); // resolve error diff --git a/Test/test0/Types1.bpl b/Test/test0/Types1.bpl index 75bb6178..2580fe40 100644 --- a/Test/test0/Types1.bpl +++ b/Test/test0/Types1.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type T, U;
-type V;
-
-function h(T) returns (int);
-function k(x:T) returns (int);
-function l(x) returns (int); // resolve error
-function m(x, x) returns (bool); // resolve error
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type T, U; +type V; + +function h(T) returns (int); +function k(x:T) returns (int); +function l(x) returns (int); // resolve error +function m(x, x) returns (bool); // resolve error diff --git a/Test/test0/WhereParsing.bpl b/Test/test0/WhereParsing.bpl index e75a1c81..e6a0ab4e 100644 --- a/Test/test0/WhereParsing.bpl +++ b/Test/test0/WhereParsing.bpl @@ -1,36 +1,36 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const x: int;
-
-function R(int) returns (bool);
-function Even(int) returns (bool);
-
-var y: int where R(y);
-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 where xx > 0) // error: where not allowed in implementation decl
- returns (yy: int where yy < 0) // error: where not allowed in implementation decl
-{
- var a: int where a == b; // b is not allowed to be mentioned here, but this test is only
- var b: int; // for parsing, so no complaint will be issued
-
- start:
- a := xx;
- call b := P(a);
- yy := b;
- return;
-}
-
-procedure {:myProcAttr} Attr(x: int, {:myParamAttr x, y} y: bool) returns (z: int, {:retAttr x} w: bool)
-{
-}
-
-procedure BadAttrs(x: int);
-implementation BadAttrs({:myParamAttr} x: int) // error: attributes not allowed in implementation decl
-{
-}
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +const x: int; + +function R(int) returns (bool); +function Even(int) returns (bool); + +var y: int where R(y); +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 where xx > 0) // error: where not allowed in implementation decl + returns (yy: int where yy < 0) // error: where not allowed in implementation decl +{ + var a: int where a == b; // b is not allowed to be mentioned here, but this test is only + var b: int; // for parsing, so no complaint will be issued + + start: + a := xx; + call b := P(a); + yy := b; + return; +} + +procedure {:myProcAttr} Attr(x: int, {:myParamAttr x, y} y: bool) returns (z: int, {:retAttr x} w: bool) +{ +} + +procedure BadAttrs(x: int); +implementation BadAttrs({:myParamAttr} x: int) // error: attributes not allowed in implementation decl +{ +} diff --git a/Test/test0/WhereParsing0.bpl b/Test/test0/WhereParsing0.bpl index da26bc5e..9e9579df 100644 --- a/Test/test0/WhereParsing0.bpl +++ b/Test/test0/WhereParsing0.bpl @@ -1,34 +1,34 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const x: int;
-
-function R(int) returns (bool);
-function Even(int) returns (bool);
-
-var y: int where R(y);
-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;
-
-procedure Q(x: int where x > 0) returns (y: int where y < 0)
- requires x < 100;
- modifies g;
- ensures (forall t: int where Even(t) :: -100 < y + t) || // error: where not allowed in quant
- (exists t: int where Even(t) :: -100 < y + t); // error: where not allowed in quant
-{
- var a: int;
- var b: int;
-
- start:
- a := x;
- call b := P(a);
- y := b;
- return;
-}
-
-axiom (forall yu: bool, {:myAttr} x: int :: x < 100);
-axiom (forall {:myAttr} x: int :: x < 100);
-axiom (forall <T> {:myAttr} x: T :: x == x);
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +const x: int; + +function R(int) returns (bool); +function Even(int) returns (bool); + +var y: int where R(y); +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; + +procedure Q(x: int where x > 0) returns (y: int where y < 0) + requires x < 100; + modifies g; + ensures (forall t: int where Even(t) :: -100 < y + t) || // error: where not allowed in quant + (exists t: int where Even(t) :: -100 < y + t); // error: where not allowed in quant +{ + var a: int; + var b: int; + + start: + a := x; + call b := P(a); + y := b; + return; +} + +axiom (forall yu: bool, {:myAttr} x: int :: x < 100); +axiom (forall {:myAttr} x: int :: x < 100); +axiom (forall <T> {:myAttr} x: T :: x == x); diff --git a/Test/test0/WhereParsing1.bpl b/Test/test0/WhereParsing1.bpl index b65f7ce9..2e9d4b37 100644 --- a/Test/test0/WhereParsing1.bpl +++ b/Test/test0/WhereParsing1.bpl @@ -1,17 +1,17 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const x: int;
-
-function R(int) returns (bool);
-function Even(int) returns (bool);
-
-var y: int where R(y);
-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;
-
-function f(a: int, b: int where b < 0) // error: where not allowed among function parameters
- returns (bool);
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +const x: int; + +function R(int) returns (bool); +function Even(int) returns (bool); + +var y: int where R(y); +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; + +function f(a: int, b: int where b < 0) // error: where not allowed among function parameters + returns (bool); diff --git a/Test/test0/WhereParsing2.bpl b/Test/test0/WhereParsing2.bpl index e7a0bd62..192b1720 100644 --- a/Test/test0/WhereParsing2.bpl +++ b/Test/test0/WhereParsing2.bpl @@ -1,4 +1,4 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const x: int where x < 0; // error: where clauses not allowed on constants
-
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +const x: int where x < 0; // error: where clauses not allowed on constants + diff --git a/Test/test0/WhereResolution.bpl b/Test/test0/WhereResolution.bpl index fac91dc8..9083d1fa 100644 --- a/Test/test0/WhereResolution.bpl +++ b/Test/test0/WhereResolution.bpl @@ -1,64 +1,64 @@ -// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type double;
-
-function R(int) returns (bool);
-function K(double, bool) returns (bool);
-
-var y: int where R(y);
-var g: int where h ==> g == 12;
-var h: bool where g < 100;
-var k: double where K(k, h);
-
-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 where a == 10;
- var b: int where a == b && b < g;
-
- start:
- a := xx;
- call b := P(a);
- yy := b;
- return;
-}
-
-procedure Q(w: int where x < w || x > alpha/*error: out-parameter alpha is not in scope*/, x: int where x + w > 0)
- returns (v: bool where v,
- y: int where x + y + z < 0,
- z: int where g == 12,
- alpha: ref where old(alpha) != null, // error: cannot use old in where clause
- beta: ref where (forall r: ref :: r == beta ==> beta == null))
- requires x < 100;
- modifies g;
- ensures -100 < y;
-{
- var a: int;
- var b: int;
-
- start:
- a := x;
- call b := P(a);
- y := b;
- return;
-}
-
-const SomeConstant: ref;
-
-procedure Cnst(n: ref where n != SomeConstant) returns (SomeConstant: int)
-{
- var m: ref where m != SomeConstant;
- var k: int where k != SomeConstant;
- var r: ref where (forall abc: ref :: abc == SomeConstant);
- var b: bool;
- start:
- b := (forall l: ref :: l == SomeConstant);
- return;
-}
-
-type ref;
-const null : ref;
+// RUN: %boogie -noVerify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type double; + +function R(int) returns (bool); +function K(double, bool) returns (bool); + +var y: int where R(y); +var g: int where h ==> g == 12; +var h: bool where g < 100; +var k: double where K(k, h); + +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 where a == 10; + var b: int where a == b && b < g; + + start: + a := xx; + call b := P(a); + yy := b; + return; +} + +procedure Q(w: int where x < w || x > alpha/*error: out-parameter alpha is not in scope*/, x: int where x + w > 0) + returns (v: bool where v, + y: int where x + y + z < 0, + z: int where g == 12, + alpha: ref where old(alpha) != null, // error: cannot use old in where clause + beta: ref where (forall r: ref :: r == beta ==> beta == null)) + requires x < 100; + modifies g; + ensures -100 < y; +{ + var a: int; + var b: int; + + start: + a := x; + call b := P(a); + y := b; + return; +} + +const SomeConstant: ref; + +procedure Cnst(n: ref where n != SomeConstant) returns (SomeConstant: int) +{ + var m: ref where m != SomeConstant; + var k: int where k != SomeConstant; + var r: ref where (forall abc: ref :: abc == SomeConstant); + var b: bool; + start: + b := (forall l: ref :: l == SomeConstant); + return; +} + +type ref; +const null : ref; |