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 /Source/Basetypes | |
| parent | 812961fd5f0cb1ca17737bebd9d09a318d38ccb6 (diff) | |
Fixed abstract interpretation for reals
Diffstat (limited to 'Source/Basetypes')
| -rw-r--r-- | Source/Basetypes/BigDec.cs | 34 |
1 files changed, 14 insertions, 20 deletions
diff --git a/Source/Basetypes/BigDec.cs b/Source/Basetypes/BigDec.cs index beb9ec54..feabb425 100644 --- a/Source/Basetypes/BigDec.cs +++ b/Source/Basetypes/BigDec.cs @@ -136,31 +136,25 @@ namespace Microsoft.Basetypes { ////////////////////////////////////////////////////////////////////////////
// Conversion operations
- [Pure]
- public BIM Floor(BIM? minimum, BIM? maximum) {
+ public void FloorCeiling(out BIM floor, out BIM ceiling) {
BIM n = this.mantissa;
-
- if (this.exponent >= 0) {
- int e = this.exponent;
- while (e > 0 && (minimum == null || minimum <= n) && (maximum == null || n <= maximum)) {
+ int e = this.exponent;
+ if (n.IsZero) {
+ floor = ceiling = n;
+ } else if (0 <= e) {
+ // it's an integer
+ for (; 0 < e; e--) {
n = n * ten;
- e = e - 1;
}
- }
- else {
- int e = -this.exponent;
- while (e > 0 && !n.IsZero) {
- n = n / ten;
- e = e - 1;
+ floor = ceiling = n;
+ } else {
+ // it's a non-zero integer, so the ceiling is one more than the fllor
+ for (; e < 0 && !n.IsZero; e++) {
+ n = n / ten; // since we're dividing by a positive number, this will round down
}
+ floor = n;
+ ceiling = n + 1;
}
-
- if (minimum != null && n < minimum)
- return (BIM)minimum;
- else if (maximum != null && maximum < n)
- return (BIM)maximum;
- else
- return n;
}
[Pure]
|