(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, 3 insertions, 3 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;