(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.

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) {