diff options
| author |  Valentin Wüstholz <wuestholz@gmail.com> | 2015-12-28 20:22:03 -0600 |
|---|---|---|
| committer | Valentin Wüstholz <wuestholz@gmail.com> | 2015-12-28 20:22:03 -0600 |
| commit | dd8e69b7b71a9375b7206a70633deae234175ef8 (patch) | |
| tree | 3ec3a9796afb6ce8c808a407c672237ce94f4b78 /Source | |
| parent | 1c16dc829c81426e17427c0d103ed831a48f1f81 (diff) | |
Improve precision of abstract interpreter for modulo operations.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index ee9d632b..2fd37463 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -884,6 +884,10 @@ namespace Microsoft.Boogie.AbstractInterpretation if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) { Lo = BigInteger.Zero; Hi = hi1; + if (lo0 < lo1 && hi0 != null && hi0 < lo1) { + Lo = lo0; + Hi = hi0; + } } break; case BinaryOperator.Opcode.RealDiv: |