(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, 1 insertions, 1 deletions

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index ce29a700..27a4e6a5 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -177,7 +177,7 @@ namespace Microsoft.Boogie
         }

     }

 

-    public class MoverTypeChecker : StandardVisitor

+    public class MoverTypeChecker : ReadOnlyVisitor

     {

         public int FindPhaseNumber(Procedure proc)

         {