(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/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index 8408bf83..11e10e93 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -8,7 +8,7 @@ using System.Diagnostics;
 

 namespace Microsoft.Boogie

 {

-    public class LinearEraser : StandardVisitor

+    public class LinearEraser : ReadOnlyVisitor

     {

         private QKeyValue RemoveLinearAttribute(QKeyValue iter)

         {

@@ -31,7 +31,7 @@ namespace Microsoft.Boogie
         CONST

     }

 

-    public class LinearTypeChecker : StandardVisitor

+    public class LinearTypeChecker : ReadOnlyVisitor

     {

         public Program program;

         public int errorCount;