summaryrefslogtreecommitdiff
path: root/Test/aitest0
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-06-28 01:44:30 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-06-28 01:44:30 +0100
commit962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d (patch)
tree27d5f9b0d130c6c1a6758bc0b7456b0aa51e34e0 /Test/aitest0
parente11d65009d0b4ba1327f5f5dd6b26367330611f0 (diff)
Normalise line endings using a .gitattributes file. Unfortunately
this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
Diffstat (limited to 'Test/aitest0')
-rw-r--r--Test/aitest0/Intervals.bpl668
-rw-r--r--Test/aitest0/constants.bpl142
2 files changed, 405 insertions, 405 deletions
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index 565b6823..fddce05a 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -1,334 +1,334 @@
-// 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;
+ }
+}
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;
+}