diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2016-06-06 23:14:18 -0600 |
commit | d652155ae013f36a1ee17653a8e458baad2d9c2c (patch) | |
tree | 067d600fe3cd1723afc11682935f0123a1eab653 /Test/aitest0 | |
parent | d7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff) |
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Test/aitest0')
-rw-r--r-- | Test/aitest0/Intervals.bpl | 683 | ||||
-rw-r--r-- | Test/aitest0/Intervals.bpl.expect | 2 | ||||
-rw-r--r-- | Test/aitest0/Issue25.bpl | 14 | ||||
-rw-r--r-- | Test/aitest0/Issue25.bpl.expect | 8 | ||||
-rw-r--r-- | Test/aitest0/constants.bpl | 142 |
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; +} |