diff options
| author |  Rustan Leino <unknown> | 2014-04-13 11:28:18 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-13 11:28:18 -0700 |
| commit | 0121d5231da0ac092b5295ed265684fa7c1f53f4 (patch) | |
| tree | 4b5fa390e7e04d57afeab9b2d4f143c26e890c6e /Test/aitest9 | |
| parent | 812961fd5f0cb1ca17737bebd9d09a318d38ccb6 (diff) | |
Fixed abstract interpretation for reals
Diffstat (limited to 'Test/aitest9')
| -rw-r--r-- | Test/aitest9/TestIntervals.bpl | 30 | ||||
| -rw-r--r-- | Test/aitest9/answer | 12 |
2 files changed, 41 insertions, 1 deletions
diff --git a/Test/aitest9/TestIntervals.bpl b/Test/aitest9/TestIntervals.bpl index bee73a57..622a0b36 100644 --- a/Test/aitest9/TestIntervals.bpl +++ b/Test/aitest9/TestIntervals.bpl @@ -38,3 +38,33 @@ procedure Q(myField: Field [ref][teflon]bool, r: ref, t: teflon) {
Heap[myField][r][t] := true;
}
+
+// -----
+
+procedure Neq()
+{
+ var n: int;
+ assume 2 <= n && n <= 10;
+ assume 2 != n;
+ assume n != 10;
+ while (*) {
+ n := n;
+ }
+ assert 3 <= n;
+ assert n < 10;
+}
+
+procedure NeqX()
+{
+ var n: real;
+ assume 2.0 <= n && n <= 10.0;
+ assume 2.0 != n;
+ assume n != 10.0;
+ // The following statement will cause Boogie to know about n only
+ // what the abstract interpreter has inferred so far.
+ while (*) { n := n; }
+
+ assert 2.0 <= n && n <= 10.0; // yes
+ assert 2.0 < n; // error, the abstract domain is not precise enough to figure this out
+ assert n < 10.0; // error, ditto
+}
diff --git a/Test/aitest9/answer b/Test/aitest9/answer index d68508af..88af771c 100644 --- a/Test/aitest9/answer +++ b/Test/aitest9/answer @@ -17,5 +17,15 @@ Execution trace: TestIntervals.bpl(13,14): anon11_Then
TestIntervals.bpl(14,14): anon12_Then
TestIntervals.bpl(17,5): anon8
+TestIntervals.bpl(68,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ TestIntervals.bpl(60,3): anon0
+ TestIntervals.bpl(65,3): anon3_LoopHead
+ TestIntervals.bpl(65,3): anon3_LoopDone
+TestIntervals.bpl(69,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ TestIntervals.bpl(60,3): anon0
+ TestIntervals.bpl(65,3): anon3_LoopHead
+ TestIntervals.bpl(65,3): anon3_LoopDone
-Boogie program verifier finished with 1 verified, 1 error
+Boogie program verifier finished with 2 verified, 3 errors
|