diff options
| author |  Rustan Leino <unknown> | 2014-04-08 08:31:05 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-04-08 08:31:05 -0700 |
| commit | 812961fd5f0cb1ca17737bebd9d09a318d38ccb6 (patch) | |
| tree | 84d98104bd72072cecae8b030c36320ac3ac7e5e /Test/aitest0 | |
| parent | 55bdb8b4ba8c49654fae37d74b34cbc4597c08fb (diff) | |
Fixed bug in abstract interpretation over reals
Diffstat (limited to 'Test/aitest0')
| -rw-r--r-- | Test/aitest0/Answer | 2 | ||||
| -rw-r--r-- | Test/aitest0/Intervals.bpl | 14 |
2 files changed, 15 insertions, 1 deletions
diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer index 961b3c33..cc518d1b 100644 --- a/Test/aitest0/Answer +++ b/Test/aitest0/Answer @@ -165,4 +165,4 @@ Execution trace: Intervals.bpl(301,3): anon3_LoopHead
Intervals.bpl(301,3): anon3_LoopDone
-Boogie program verifier finished with 15 verified, 11 errors
+Boogie program verifier finished with 16 verified, 11 errors
diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl index 6a588bbe..c769645f 100644 --- a/Test/aitest0/Intervals.bpl +++ b/Test/aitest0/Intervals.bpl @@ -316,3 +316,17 @@ procedure Id17(n: int) 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;
+ }
+}
|