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/Houdini/AbstractHoudini.cs | 6 +++---
 Source/Houdini/Checker.cs         | 2 +-
 Source/Houdini/Houdini.cs         | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'Source/Houdini')

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