From 9a172309c91360449dd6211b39b96fdff0a7d2d0 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 24 Feb 2014 22:54:32 -0800
Subject: (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.

---
 Source/AbsInt/IntervalDomain.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Source/AbsInt/IntervalDomain.cs')

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) {
-- 
cgit v1.2.3