(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/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)

         {