summaryrefslogtreecommitdiff
path: root/Source/AbsInt
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2014-02-24 22:54:32 -0800
committerGravatar Rustan Leino <unknown>2014-02-24 22:54:32 -0800
commit9a172309c91360449dd6211b39b96fdff0a7d2d0 (patch)
tree54cc884e9f63c1e7dbe9167d50ab59b87ce8c4e7 /Source/AbsInt
parentd9dc7b51a3c1af9177f5b70cf7425b1990d25e77 (diff)
(Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions of its methods now demand the return value to equal the given node.
Changed read-only visitors to extend from ReadOnlyVisitor instead of just StandardVisitor.
Diffstat (limited to 'Source/AbsInt')
-rw-r--r--Source/AbsInt/IntervalDomain.cs4
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 0dbcaaba..4b5ae903 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -610,7 +610,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
return lo != null || hi != null;
}
- class PEVisitor : StandardVisitor
+ class PEVisitor : ReadOnlyVisitor
{
public BigInteger? Lo;
public BigInteger? Hi;
@@ -990,7 +990,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
}
}
- public class ThresholdFinder : StandardVisitor
+ public class ThresholdFinder : ReadOnlyVisitor
{
readonly Implementation Impl;
public ThresholdFinder(Implementation impl) {