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

3 files changed, 6 insertions, 6 deletions

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 95c29157..9f73e4a1 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -463,7 +463,7 @@ namespace Microsoft.Boogie.Houdini {
         }

 

         // Remove functions AbsHoudiniConstant from the expressions and substitute them with "true"

-        class ExistentialExprModelMassage : StandardVisitor

+        class ExistentialExprModelMassage : ReadOnlyVisitor

         {

             List<Function> ahFuncs;

 

@@ -491,7 +491,7 @@ namespace Microsoft.Boogie.Houdini {
             }

         }

 

-        class FunctionCollector : StandardVisitor

+        class FunctionCollector : ReadOnlyVisitor

         {

             public List<Tuple<Function, ExistsExpr>> functionsUsed;

             ExistsExpr existentialExpr;

@@ -3683,7 +3683,7 @@ namespace Microsoft.Boogie.Houdini {
         }

 

 

-        class GatherLiterals : StandardVisitor

+        class GatherLiterals : ReadOnlyVisitor

         {

             public List<Tuple<Variable, Expr>> literals;

             bool inOld;

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 252321b6..6ffaef22 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -16,7 +16,7 @@ using VC;
 using System.Linq;

 

 namespace Microsoft.Boogie.Houdini {

-  public class ExistentialConstantCollector : StandardVisitor {

+  public class ExistentialConstantCollector : ReadOnlyVisitor {

       public static void CollectHoudiniConstants(Houdini houdini, Implementation impl, out ExistentialConstantCollector collector)

       {

           collector = new ExistentialConstantCollector(houdini);

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index b05a2e5f..393c71eb 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -293,7 +293,7 @@ namespace Microsoft.Boogie.Houdini {
     }

   }

 

-  public class InlineEnsuresVisitor : StandardVisitor {

+  public class InlineEnsuresVisitor : ReadOnlyVisitor {

     public override Ensures VisitEnsures(Ensures ensures) {

       ensures.Attributes = new QKeyValue(Token.NoToken, "assume", new List<object>(), ensures.Attributes);

       return base.VisitEnsures(ensures);

@@ -448,7 +448,7 @@ namespace Microsoft.Boogie.Houdini {
     }

 

       // Compute dependencies between candidates

-    public class CrossDependencies : StandardVisitor

+    public class CrossDependencies : ReadOnlyVisitor

     {

         public CrossDependencies(HashSet<Variable> constants)

         {