summaryrefslogtreecommitdiff
path: root/Test/aitest0
diff options
context:
space:
mode:
authorGravatar Checkmate50 <dgeisler50@gmail.com>2016-06-06 23:14:18 -0600
committerGravatar Checkmate50 <dgeisler50@gmail.com>2016-06-06 23:14:18 -0600
commitd652155ae013f36a1ee17653a8e458baad2d9c2c (patch)
tree067d600fe3cd1723afc11682935f0123a1eab653 /Test/aitest0
parentd7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff)
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Test/aitest0')
-rw-r--r--Test/aitest0/Intervals.bpl683
-rw-r--r--Test/aitest0/Intervals.bpl.expect2
-rw-r--r--Test/aitest0/Issue25.bpl14
-rw-r--r--Test/aitest0/Issue25.bpl.expect8
-rw-r--r--Test/aitest0/constants.bpl142
5 files changed, 443 insertions, 406 deletions
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index 565b6823..8d40b81d 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -1,334 +1,349 @@
-// RUN: %boogie -infer:j "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const N: int;
-axiom 0 <= N;
-
-procedure P(K: int)
- requires 0 <= K;
-{
- var b: bool, x, k: int;
-
- if (!b) {
- b := !b;
- }
- x := if b then 13 else 10;
- k := K;
- while (k != 0) {
- x := x + k;
- k := k - 1;
- }
- assert 13 <= x;
-}
-
-procedure Thresholds0()
-{
- var i: int;
- i := 0;
- while (i < 200)
- {
- i := i + 1;
- }
- assert i == 200;
-}
-
-procedure Thresholds1()
-{
- var i: int;
- i := 0;
- while (i <= 199)
- {
- i := i + 1;
- }
- assert i == 200;
-}
-
-procedure Thresholds2()
-{
- var i: int;
- i := 100;
- while (0 < i)
- {
- i := i - 1;
- }
- assert i == 0;
-}
-
-procedure Thresholds3()
-{
- var i: int;
- i := 0;
- while (i < 200)
- {
- i := i + 1;
- }
- assert i == 199; // error
-}
-
-procedure Thresholds4()
-{
- var i: int;
- i := 0;
- while (i + 3 < 203)
- {
- i := i + 1;
- }
- assert i * 2 == 400; // error: this would hold in an execution, but /infer:j is too weak to infer invariant i<=200
-}
-
-procedure UnaryNegation0() returns (x: int) // this was once buggy
-{
- x := -1;
- loop_head:
- x := x;
- goto loop_head, after_loop;
- after_loop:
- assert x == -1;
-}
-procedure UnaryNegation1() returns (x: int) // this was once buggy
-{
- x := -1;
- loop_head:
- x := x;
- goto loop_head, after_loop;
- after_loop:
- assert x == 1; // error
-}
-
-// --------------------------- test {:identity} annotation --------------------
-
-function {:identity} MyId(x: int): int;
-function MyStealthyId(x: int): int; // this one messes up the abstract interpretation
-function {:identity false} {:identity}/*the last attribute rules*/ MyPolyId<T>(x: T): T;
-function {:identity /*this is a lie*/} MyBogusId(x: int): int { -x }
-function {:identity /*ignored, since the function takes more than one argument*/} MultipleArgs(x: int, y: int): int;
-function {:identity /*ignored, since the return type is not equal to the argument type*/} BoolToInt(b: bool): int;
-function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId0<T>(x: T): int;
-function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId1<T>(x: int): T;
-function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId2<T,U>(x: T): U;
-
-
-procedure Id0(n: int)
-{
- var i: int;
- i := 0;
- while (i < n)
- {
- i := i + 1;
- }
- assert 0 <= i;
-}
-
-procedure Id1(n: int)
-{
- var i: int;
- i := MyId(0);
- while (i < n)
- {
- i := i + MyId(1);
- }
- assert 0 <= i;
-}
-
-procedure Id2(n: int)
-{
- var i: int;
- i := MyStealthyId(0);
- while (i < n)
- {
- i := i + 1;
- }
- assert 0 <= i; // error: abstract interpreter does not figure this one out
-}
-
-procedure Id3(n: int)
-{
- var i: int;
- i := 0;
- while (i < n)
- {
- i := i + MyStealthyId(1);
- }
- assert 0 <= i; // error: abstract interpreter does not figure this one out
-}
-
-procedure Id4(n: int)
-{
- var i: int;
- i := MyPolyId(0);
- while (i < n)
- {
- i := i + MyPolyId(1);
- }
- assert 0 <= i;
-}
-
-procedure Id5(n: int)
-{
- var i: int;
- var b: bool;
- i, b := 0, false;
- while (i < n)
- {
- i, b := i + 1, false;
- }
- assert !b;
-}
-
-procedure Id6(n: int)
-{
- var i: int;
- var b: bool;
- i, b := 0, MyPolyId(false);
- while (i < n)
- {
- i, b := i + 1, false;
- }
- assert !b;
-}
-
-procedure Id7(n: int)
-{
- var i, k, y, z: int;
- i, k := 0, 0;
- while (i < n)
- {
- i := i + 1;
- y, z := MyBogusId(5), -5;
- k := k + z;
- if (*) {
- assert y == z; // fine
- }
- }
- assert 0 <= k; // error: this does not hold -- k may very well be negative
-}
-
-procedure Id8(n: int)
-{
- var i, k: int;
- i, k := 0, 0;
- while (i < n)
- {
- i := i + 1;
- k := k + MyBogusId(5);
- }
- assert 0 <= k; // since we lied about MyBogusId being an {:identity} function, the abstract interpreter gives us this bogus invariant
-}
-
-procedure Id9(n: int)
- requires 0 < n;
-{
- var i, k: int;
- i, k := 0, 0;
- while (i < n)
- invariant i <= n && -k == 5*i;
- {
- i := i + 1;
- k := k + MyBogusId(5);
- }
- assert -k == 5*n;
- assert false; // this just shows the effect of MyBogusId even more; there is no complaint about this assert
-}
-
-procedure Id10(n: int)
-{
- var i: int;
- i := 0;
- while (i < n)
- {
- i := i + MultipleArgs(19, 23);
- }
- assert 0 <= i; // error: no information is known about i
-}
-
-procedure Id11(n: int)
-{
- var i, k: int;
- i, k := 0, 0;
- while (i < n)
- {
- i := i + 1;
- k := k + BoolToInt(false); // this should not be treated as an identity function, since it goes from one type to another
- }
- assert 0 <= k; // error: no information is known about k
-}
-
-procedure Id12(n: int)
-{
- var i: int;
- i := 0;
- while (i < n)
- {
- i := i + SometimesId0(false);
- }
- assert 0 <= i; // error: no information is known about i
-}
-
-procedure Id13(n: int)
-{
- var i: int;
- i := 0;
- while (i < n)
- {
- i := i + SometimesId0(1);
- }
- assert 0 <= i;
-}
-
-procedure Id14(n: int)
-{
- var i: int;
- i := 0;
- while (i < n)
- {
- i := i + SometimesId0(-1);
- }
- assert 0 <= i; // error: this does not hold
-}
-
-procedure Id15(n: int)
-{
- var i: int;
- i := 0;
- while (i < n)
- {
- i := i + SometimesId1(1);
- }
- assert 0 <= i; // fine: SometimesId1 claims to be an identity and the use of it is int->int
-}
-
-procedure Id16(n: int)
-{
- var i: int;
- i := 0;
- while (i < n)
- {
- i := i + SometimesId2(false);
- }
- assert 0 <= i; // error: no information is known about i
-}
-
-procedure Id17(n: int)
-{
- var i: int;
- i := 0;
- while (i < n)
- {
- i := i + SometimesId2(1);
- }
- assert 0 <= i; // fine: SometimesId2 claims to be an identity and the use of it is int->int
-}
-
-// real numbers
-
-procedure W0(N: real)
-{
- var i, bf0: real;
- i := 0.0;
- while (i < N) {
- bf0 := N - i;
- i := i + 1.0;
- // check termination:
- assert 0.0 <= bf0;
- assert N - i <= bf0 - 1.0;
- }
-}
+// RUN: %boogie -infer:j "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+const N: int;
+axiom 0 <= N;
+
+procedure P(K: int)
+ requires 0 <= K;
+{
+ var b: bool, x, k: int;
+
+ if (!b) {
+ b := !b;
+ }
+ x := if b then 13 else 10;
+ k := K;
+ while (k != 0) {
+ x := x + k;
+ k := k - 1;
+ }
+ assert 13 <= x;
+}
+
+procedure Thresholds0()
+{
+ var i: int;
+ i := 0;
+ while (i < 200)
+ {
+ i := i + 1;
+ }
+ assert i == 200;
+}
+
+procedure Thresholds1()
+{
+ var i: int;
+ i := 0;
+ while (i <= 199)
+ {
+ i := i + 1;
+ }
+ assert i == 200;
+}
+
+procedure Thresholds2()
+{
+ var i: int;
+ i := 100;
+ while (0 < i)
+ {
+ i := i - 1;
+ }
+ assert i == 0;
+}
+
+procedure Thresholds3()
+{
+ var i: int;
+ i := 0;
+ while (i < 200)
+ {
+ i := i + 1;
+ }
+ assert i == 199; // error
+}
+
+procedure Thresholds4()
+{
+ var i: int;
+ i := 0;
+ while (i + 3 < 203)
+ {
+ i := i + 1;
+ }
+ assert i * 2 == 400; // error: this would hold in an execution, but /infer:j is too weak to infer invariant i<=200
+}
+
+procedure UnaryNegation0() returns (x: int) // this was once buggy
+{
+ x := -1;
+ loop_head:
+ x := x;
+ goto loop_head, after_loop;
+ after_loop:
+ assert x == -1;
+}
+procedure UnaryNegation1() returns (x: int) // this was once buggy
+{
+ x := -1;
+ loop_head:
+ x := x;
+ goto loop_head, after_loop;
+ after_loop:
+ assert x == 1; // error
+}
+
+// --------------------------- test {:identity} annotation --------------------
+
+function {:identity} MyId(x: int): int;
+function MyStealthyId(x: int): int; // this one messes up the abstract interpretation
+function {:identity false} {:identity}/*the last attribute rules*/ MyPolyId<T>(x: T): T;
+function {:identity /*this is a lie*/} MyBogusId(x: int): int { -x }
+function {:identity /*ignored, since the function takes more than one argument*/} MultipleArgs(x: int, y: int): int;
+function {:identity /*ignored, since the return type is not equal to the argument type*/} BoolToInt(b: bool): int;
+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId0<T>(x: T): int;
+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId1<T>(x: int): T;
+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId2<T,U>(x: T): U;
+
+
+procedure Id0(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + 1;
+ }
+ assert 0 <= i;
+}
+
+procedure Id1(n: int)
+{
+ var i: int;
+ i := MyId(0);
+ while (i < n)
+ {
+ i := i + MyId(1);
+ }
+ assert 0 <= i;
+}
+
+procedure Id2(n: int)
+{
+ var i: int;
+ i := MyStealthyId(0);
+ while (i < n)
+ {
+ i := i + 1;
+ }
+ assert 0 <= i; // error: abstract interpreter does not figure this one out
+}
+
+procedure Id3(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + MyStealthyId(1);
+ }
+ assert 0 <= i; // error: abstract interpreter does not figure this one out
+}
+
+procedure Id4(n: int)
+{
+ var i: int;
+ i := MyPolyId(0);
+ while (i < n)
+ {
+ i := i + MyPolyId(1);
+ }
+ assert 0 <= i;
+}
+
+procedure Id5(n: int)
+{
+ var i: int;
+ var b: bool;
+ i, b := 0, false;
+ while (i < n)
+ {
+ i, b := i + 1, false;
+ }
+ assert !b;
+}
+
+procedure Id6(n: int)
+{
+ var i: int;
+ var b: bool;
+ i, b := 0, MyPolyId(false);
+ while (i < n)
+ {
+ i, b := i + 1, false;
+ }
+ assert !b;
+}
+
+procedure Id7(n: int)
+{
+ var i, k, y, z: int;
+ i, k := 0, 0;
+ while (i < n)
+ {
+ i := i + 1;
+ y, z := MyBogusId(5), -5;
+ k := k + z;
+ if (*) {
+ assert y == z; // fine
+ }
+ }
+ assert 0 <= k; // error: this does not hold -- k may very well be negative
+}
+
+procedure Id8(n: int)
+{
+ var i, k: int;
+ i, k := 0, 0;
+ while (i < n)
+ {
+ i := i + 1;
+ k := k + MyBogusId(5);
+ }
+ assert 0 <= k; // since we lied about MyBogusId being an {:identity} function, the abstract interpreter gives us this bogus invariant
+}
+
+procedure Id9(n: int)
+ requires 0 < n;
+{
+ var i, k: int;
+ i, k := 0, 0;
+ while (i < n)
+ invariant i <= n && -k == 5*i;
+ {
+ i := i + 1;
+ k := k + MyBogusId(5);
+ }
+ assert -k == 5*n;
+ assert false; // this just shows the effect of MyBogusId even more; there is no complaint about this assert
+}
+
+procedure Id10(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + MultipleArgs(19, 23);
+ }
+ assert 0 <= i; // error: no information is known about i
+}
+
+procedure Id11(n: int)
+{
+ var i, k: int;
+ i, k := 0, 0;
+ while (i < n)
+ {
+ i := i + 1;
+ k := k + BoolToInt(false); // this should not be treated as an identity function, since it goes from one type to another
+ }
+ assert 0 <= k; // error: no information is known about k
+}
+
+procedure Id12(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId0(false);
+ }
+ assert 0 <= i; // error: no information is known about i
+}
+
+procedure Id13(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId0(1);
+ }
+ assert 0 <= i;
+}
+
+procedure Id14(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId0(-1);
+ }
+ assert 0 <= i; // error: this does not hold
+}
+
+procedure Id15(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId1(1);
+ }
+ assert 0 <= i; // fine: SometimesId1 claims to be an identity and the use of it is int->int
+}
+
+procedure Id16(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId2(false);
+ }
+ assert 0 <= i; // error: no information is known about i
+}
+
+procedure Id17(n: int)
+{
+ var i: int;
+ i := 0;
+ while (i < n)
+ {
+ i := i + SometimesId2(1);
+ }
+ assert 0 <= i; // fine: SometimesId2 claims to be an identity and the use of it is int->int
+}
+
+// real numbers
+
+procedure W0(N: real)
+{
+ var i, bf0: real;
+ i := 0.0;
+ while (i < N) {
+ bf0 := N - i;
+ i := i + 1.0;
+ // check termination:
+ assert 0.0 <= bf0;
+ assert N - i <= bf0 - 1.0;
+ }
+}
+
+// mod
+
+procedure Mod0(n: int)
+ requires 10 < n;
+{
+ var i: int;
+
+ i := 0;
+ while (i < 10)
+ {
+ i := (i mod n) + 1;
+ }
+ assert i == 10;
+}
diff --git a/Test/aitest0/Intervals.bpl.expect b/Test/aitest0/Intervals.bpl.expect
index a0769ec5..980593a9 100644
--- a/Test/aitest0/Intervals.bpl.expect
+++ b/Test/aitest0/Intervals.bpl.expect
@@ -54,4 +54,4 @@ Execution trace:
Intervals.bpl(303,3): anon3_LoopHead
Intervals.bpl(303,3): anon3_LoopDone
-Boogie program verifier finished with 16 verified, 11 errors
+Boogie program verifier finished with 17 verified, 11 errors
diff --git a/Test/aitest0/Issue25.bpl b/Test/aitest0/Issue25.bpl
new file mode 100644
index 00000000..6ffcd113
--- /dev/null
+++ b/Test/aitest0/Issue25.bpl
@@ -0,0 +1,14 @@
+// RUN: %boogie -infer:j "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+const N: int;
+axiom 0 <= N;
+
+procedure vacuous_post()
+ensures (forall k, l: int :: 0 <= k && k <= l && l < N ==> N < N); // Used to verify at some point (see https://github.com/boogie-org/boogie/issues/25).
+{
+var x: int;
+x := -N;
+while (x != x) {
+}
+}
diff --git a/Test/aitest0/Issue25.bpl.expect b/Test/aitest0/Issue25.bpl.expect
new file mode 100644
index 00000000..f56502e2
--- /dev/null
+++ b/Test/aitest0/Issue25.bpl.expect
@@ -0,0 +1,8 @@
+Issue25.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
+Issue25.bpl(8,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ Issue25.bpl(11,3): anon0
+ Issue25.bpl(12,1): anon2_LoopHead
+ Issue25.bpl(12,1): anon2_LoopDone
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/aitest0/constants.bpl b/Test/aitest0/constants.bpl
index a3b82df7..d2075e26 100644
--- a/Test/aitest0/constants.bpl
+++ b/Test/aitest0/constants.bpl
@@ -1,71 +1,71 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Test the constant propagation AI
-
-var GlobalFlag : bool;
-
-const A, B, C:int; // Consts
-
-procedure Join (b : bool)
- modifies GlobalFlag;
-{
- var x, y, z:int;
-
- start:
- GlobalFlag := true;
- x := 3;
- y := 4;
- z := x + y;
- goto Then, Else; // if (b)
-
- Then:
- assume b == true;
- x := x + 1;
- goto join;
-
- Else:
- assume b == false;
- y := 4;
- goto join;
-
- join:
- assert y == 4;
- assert z == 7;
- assert GlobalFlag == true;
- return;
-}
-
-
-procedure Loop ()
-{
- var c, i: int;
-
- start:
- c := 0; i := 0;
- goto test;
-
- test:
- // if (i < 10);
- goto Then, Else;
-
- Then:
- assume (i < 10);
- i := i + 1;
- goto test;
-
- Else:
- return;
-}
-
-procedure Evaluate ()
-{
- var i : int;
-
- start:
- i := 5;
- i := 3 * i + 1;
- i := 3 * (i + 1);
- i := 1 + 3 * i;
- i := (i + 1) * 3;
- return;
-}
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Test the constant propagation AI
+
+var GlobalFlag : bool;
+
+const A, B, C:int; // Consts
+
+procedure Join (b : bool)
+ modifies GlobalFlag;
+{
+ var x, y, z:int;
+
+ start:
+ GlobalFlag := true;
+ x := 3;
+ y := 4;
+ z := x + y;
+ goto Then, Else; // if (b)
+
+ Then:
+ assume b == true;
+ x := x + 1;
+ goto join;
+
+ Else:
+ assume b == false;
+ y := 4;
+ goto join;
+
+ join:
+ assert y == 4;
+ assert z == 7;
+ assert GlobalFlag == true;
+ return;
+}
+
+
+procedure Loop ()
+{
+ var c, i: int;
+
+ start:
+ c := 0; i := 0;
+ goto test;
+
+ test:
+ // if (i < 10);
+ goto Then, Else;
+
+ Then:
+ assume (i < 10);
+ i := i + 1;
+ goto test;
+
+ Else:
+ return;
+}
+
+procedure Evaluate ()
+{
+ var i : int;
+
+ start:
+ i := 5;
+ i := 3 * i + 1;
+ i := 3 * (i + 1);
+ i := 1 + 3 * i;
+ i := (i + 1) * 3;
+ return;
+}