diff options
| author |  Rustan Leino <unknown> | 2013-07-05 14:37:11 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-07-05 14:37:11 -0700 |
| commit | 7fbe519af9271420e5b513021dd1f846a4337e7e (patch) | |
| tree | e5f6f182941bef103b49a461518a30ab343b43d4 /Test/aitest0/Intervals.bpl | |
| parent | fc33b0b2938ad4e81e34c87f054c2880bb56cd17 (diff) | |
Added support in the abstract interpreter for an attribute {:identity}, which says that a function is an identity function.
Diffstat (limited to 'Test/aitest0/Intervals.bpl')
| -rw-r--r-- | Test/aitest0/Intervals.bpl | 225 |
1 files changed, 225 insertions, 0 deletions
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl index 4520a032..6a588bbe 100644 --- a/Test/aitest0/Intervals.bpl +++ b/Test/aitest0/Intervals.bpl @@ -91,3 +91,228 @@ procedure UnaryNegation1() returns (x: int) // this was once buggy 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
+}
+
|