(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.

12 files changed, 117 insertions, 189 deletions

diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs
index 0dbcaaba..4b5ae903 100644
--- a/Source/AbsInt/IntervalDomain.cs
+++ b/Source/AbsInt/IntervalDomain.cs
@@ -610,7 +610,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
       return lo != null || hi != null;

     }

 

-    class PEVisitor : StandardVisitor

+    class PEVisitor : ReadOnlyVisitor

     {

       public BigInteger? Lo;

       public BigInteger? Hi;

@@ -990,7 +990,7 @@ namespace Microsoft.Boogie.AbstractInterpretation
     }

   }

 

-  public class ThresholdFinder : StandardVisitor

+  public class ThresholdFinder : ReadOnlyVisitor

   {

     readonly Implementation Impl;

     public ThresholdFinder(Implementation impl) {

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;

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)

         {

diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs
index e2bbcdf5..45e69eed 100644
--- a/Source/Core/AbsyQuant.cs
+++ b/Source/Core/AbsyQuant.cs
@@ -599,7 +599,7 @@ namespace Microsoft.Boogie {
     }

 

     #region never triggers

-    private class NeverTriggerCollector : StandardVisitor {

+    private class NeverTriggerCollector : ReadOnlyVisitor {

       QuantifierExpr/*!*/ parent;

       [ContractInvariantMethod]

       void ObjectInvariant() {

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index bdfefb04..e14d4fd3 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -38,7 +38,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public class ModSetCollector : StandardVisitor {

+  public class ModSetCollector : ReadOnlyVisitor {

     static Procedure enclosingProc;

     static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;

     static HashSet<Procedure> yieldingProcs;

@@ -264,7 +264,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public class VariableCollector : StandardVisitor {

+  public class VariableCollector : ReadOnlyVisitor {

     public HashSet<Variable/*!*/>/*!*/ usedVars;

     public HashSet<Variable/*!*/>/*!*/ oldVarsUsed;

     [ContractInvariantMethod]

@@ -303,7 +303,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public class BlockCoalescer : StandardVisitor {

+  public class BlockCoalescer : ReadOnlyVisitor {

     public static void CoalesceBlocks(Program program) {

       Contract.Requires(program != null);

       BlockCoalescer blockCoalescer = new BlockCoalescer();

@@ -1642,7 +1642,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
     }

   }

 

-  public class TokenEliminator : StandardVisitor

+  public class TokenEliminator : ReadOnlyVisitor

   {

       public int TokenCount = 0;

       public override Expr VisitExpr(Expr node)

diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index cf0918f2..742c39f6 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -51,7 +51,7 @@ namespace Microsoft.Boogie {
   }

 

   /// <summary>

-  /// Walks an IR, mutating it into a new form

+  /// Walks an IR, mutating it into a new form. (For a subclass that does not mutate the IR, see ReadOnlyVisitor.)

   /// </summary>   

   public abstract class StandardVisitor : Visitor {

     public Visitor callingVisitor;

@@ -62,8 +62,6 @@ namespace Microsoft.Boogie {
       this.callingVisitor = callingVisitor;

     }

     public override Absy Visit(Absy node) {

-      //Contract.Requires(node != null);

-      Contract.Ensures(Contract.Result<Absy>() != null);

       return node.StdDispatch(this);

     }

     public virtual Cmd VisitAssertCmd(AssertCmd node) {

@@ -150,8 +148,8 @@ namespace Microsoft.Boogie {
       return blockSeq;

     }

     public virtual List<Block/*!*/>/*!*/ VisitBlockList(List<Block/*!*/>/*!*/ blocks) {

-      Contract.Requires(cce.NonNullElements(blocks));

-      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

+      Contract.Requires(blocks != null);

+      Contract.Ensures(Contract.Result<List<Block>>() != null);

       for (int i = 0, n = blocks.Count; i < n; i++) {

         blocks[i] = this.VisitBlock(blocks[i]);

       }

@@ -227,8 +225,8 @@ namespace Microsoft.Boogie {
       return node;

     }

     public virtual List<Declaration/*!*/>/*!*/ VisitDeclarationList(List<Declaration/*!*/>/*!*/ declarationList) {

-      Contract.Requires(cce.NonNullElements(declarationList));

-      Contract.Ensures(cce.NonNullElements(Contract.Result<List<Declaration>>()));

+      Contract.Requires(declarationList != null);

+      Contract.Ensures(Contract.Result<List<Declaration>>() != null);

       for (int i = 0, n = declarationList.Count; i < n; i++)

         declarationList[i] = cce.NonNull((Declaration/*!*/)this.Visit(declarationList[i]));

       return declarationList;

@@ -604,6 +602,12 @@ namespace Microsoft.Boogie {
     }

   }

 

+  /// <summary>

+  /// A ReadOnlyVisitor visits all the nodes of a given Absy.  The visitor may collect information from

+  /// the nodes, may change fields contained in the data structure, but may not replace any nodes in the

+  /// data structure.  To enforce this, all Visit...(node) methods have a postcondition that says that

+  /// the return value is equal to the given "node".

+  /// </summary>

   public abstract class ReadOnlyVisitor : StandardVisitor

   {

       public ReadOnlyVisitor()

@@ -615,21 +619,18 @@ namespace Microsoft.Boogie {
       }

       public override Absy Visit(Absy node)

       {

-          //Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Absy>() != null);

+          Contract.Ensures(Contract.Result<Absy>() == node);

           return node.StdDispatch(this);

       }

       public override Cmd VisitAssertCmd(AssertCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Cmd>() != null);

+          Contract.Ensures(Contract.Result<Cmd>() == node);

           this.VisitExpr(node.Expr);

           return node;

       }

       public override Cmd VisitAssignCmd(AssignCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Cmd>() != null);

+          Contract.Ensures(Contract.Result<Cmd>() == node);

           for (int i = 0; i < node.Lhss.Count; ++i)

           {

               this.Visit(node.Lhss[i]);

@@ -639,83 +640,72 @@ namespace Microsoft.Boogie {
       }

       public override Cmd VisitAssumeCmd(AssumeCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Cmd>() != null);

+          Contract.Ensures(Contract.Result<Cmd>() == node);

           this.VisitExpr(node.Expr);

           return node;

       }

       public override AtomicRE VisitAtomicRE(AtomicRE node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<AtomicRE>() != null);

+          Contract.Ensures(Contract.Result<AtomicRE>() == node);

           this.VisitBlock(node.b);

           return node;

       }

       public override Axiom VisitAxiom(Axiom node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Axiom>() != null);

+          Contract.Ensures(Contract.Result<Axiom>() == node);

           this.VisitExpr(node.Expr);

           return node;

       }

       public override Type VisitBasicType(BasicType node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Type>() != null);

+          Contract.Ensures(Contract.Result<Type>() == node);

           return this.VisitType(node);

       }

       public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<BvConcatExpr>() != null);

+          Contract.Ensures(Contract.Result<BvConcatExpr>() == node);

           this.VisitExpr(node.E0);

           this.VisitExpr(node.E1);

           return node;

       }

       public override Type VisitBvType(BvType node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Type>() != null);

+          Contract.Ensures(Contract.Result<Type>() == node);

           return this.VisitType(node);

       }

       public override Type VisitBvTypeProxy(BvTypeProxy node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Type>() != null);

+          Contract.Ensures(Contract.Result<Type>() == node);

           // if the type proxy is instantiated with some more

           // specific type, we visit the instantiation

           if (node.ProxyFor != null)

-              return (Type)this.Visit(node.ProxyFor);

+              this.Visit(node.ProxyFor);

           return this.VisitType(node);

       }

       public override Block VisitBlock(Block node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Block>() != null);

+          Contract.Ensures(Contract.Result<Block>() == node);

           this.VisitCmdSeq(node.Cmds);

           this.Visit(cce.NonNull(node.TransferCmd));

           return node;

       }

       public override Expr VisitCodeExpr(CodeExpr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Expr>() != null);

+          Contract.Ensures(Contract.Result<Expr>() == node);

           this.VisitVariableSeq(node.LocVars);

           this.VisitBlockList(node.Blocks);

           return node;

       }

       public override List<Block> VisitBlockSeq(List<Block> blockSeq)

       {

-          Contract.Requires(blockSeq != null);

-          Contract.Ensures(Contract.Result<List<Block>>() != null);

+          Contract.Ensures(Contract.Result<List<Block>>() == blockSeq);

           for (int i = 0, n = blockSeq.Count; i < n; i++)

               this.VisitBlock(cce.NonNull(blockSeq[i]));

           return blockSeq;

       }

       public override List<Block/*!*/>/*!*/ VisitBlockList(List<Block/*!*/>/*!*/ blocks)

       {

-          Contract.Requires(cce.NonNullElements(blocks));

-          Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

+          Contract.Ensures(Contract.Result<List<Block>>() == blocks);

           for (int i = 0, n = blocks.Count; i < n; i++)

           {

               this.VisitBlock(blocks[i]);

@@ -724,14 +714,12 @@ namespace Microsoft.Boogie {
       }

       public override BoundVariable VisitBoundVariable(BoundVariable node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<BoundVariable>() != null);

+          Contract.Ensures(Contract.Result<BoundVariable>() == node);

           return (BoundVariable)this.VisitVariable(node);

       }

       public override Cmd VisitCallCmd(CallCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Cmd>() != null);

+          Contract.Ensures(Contract.Result<Cmd>() == node);

           for (int i = 0; i < node.Ins.Count; ++i)

               if (node.Ins[i] != null)

                   this.VisitExpr(node.Ins[i]);

@@ -742,8 +730,7 @@ namespace Microsoft.Boogie {
       }

       public override Cmd VisitParCallCmd(ParCallCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Cmd>() != null);

+          Contract.Ensures(Contract.Result<Cmd>() == node);

           for (int i = 0; i < node.CallCmds.Count; i++)

           {

               if (node.CallCmds[i] != null)

@@ -753,140 +740,120 @@ namespace Microsoft.Boogie {
       }

       public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)

       {

-          Contract.Requires(cmdSeq != null);

-          Contract.Ensures(Contract.Result<List<Cmd>>() != null);

+          Contract.Ensures(Contract.Result<List<Cmd>>() == cmdSeq);

           for (int i = 0, n = cmdSeq.Count; i < n; i++)

               this.Visit(cce.NonNull(cmdSeq[i])); // call general Visit so subtypes of Cmd get visited by their particular visitor

           return cmdSeq;

       }

       public override Choice VisitChoice(Choice node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Choice>() != null);

+          Contract.Ensures(Contract.Result<Choice>() == node);

           this.VisitRESeq(node.rs);

           return node;

       }

       public override Cmd VisitCommentCmd(CommentCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Cmd>() != null);

+          Contract.Ensures(Contract.Result<Cmd>() == node);

           return node;

       }

       public override Constant VisitConstant(Constant node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Constant>() != null);

+          Contract.Ensures(Contract.Result<Constant>() == node);

           return node;

       }

       public override CtorType VisitCtorType(CtorType node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<CtorType>() != null);

+          Contract.Ensures(Contract.Result<CtorType>() == node);

           for (int i = 0; i < node.Arguments.Count; ++i)

               this.Visit(node.Arguments[i]);

           return node;

       }

       public override Declaration VisitDeclaration(Declaration node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Declaration>() != null);

+          Contract.Ensures(Contract.Result<Declaration>() == node);

           return node;

       }

       public override List<Declaration/*!*/>/*!*/ VisitDeclarationList(List<Declaration/*!*/>/*!*/ declarationList)

       {

-          Contract.Requires(cce.NonNullElements(declarationList));

-          Contract.Ensures(cce.NonNullElements(Contract.Result<List<Declaration>>()));

+          Contract.Ensures(Contract.Result<List<Declaration>>() == declarationList);

           for (int i = 0, n = declarationList.Count; i < n; i++)

               this.Visit(declarationList[i]);

           return declarationList;

       }

       public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<DeclWithFormals>() != null);

+          Contract.Ensures(Contract.Result<DeclWithFormals>() == node);

           this.VisitVariableSeq(node.InParams);

           this.VisitVariableSeq(node.OutParams);

           return node;

       }

       public override ExistsExpr VisitExistsExpr(ExistsExpr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<ExistsExpr>() != null);

+          Contract.Ensures(Contract.Result<ExistsExpr>() == node);

           return (ExistsExpr)this.VisitQuantifierExpr(node);

       }

       public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<BvExtractExpr>() != null);

+          Contract.Ensures(Contract.Result<BvExtractExpr>() == node);

           this.VisitExpr(node.Bitvector);

           return node;

       }

       public override Expr VisitExpr(Expr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Expr>() != null);

+          Contract.Ensures(Contract.Result<Expr>() == node);

           return (Expr)this.Visit(node);

       }

       public override List<Expr> VisitExprSeq(List<Expr> exprSeq)

       {

-          //Contract.Requires(exprSeq != null);

-          Contract.Ensures(Contract.Result<List<Expr>>() != null);

+          Contract.Ensures(Contract.Result<List<Expr>>() == exprSeq);

           for (int i = 0, n = exprSeq.Count; i < n; i++)

               this.VisitExpr(cce.NonNull(exprSeq[i]));

           return exprSeq;

       }

-      public override Requires VisitRequires(Requires @requires)

+      public override Requires VisitRequires(Requires requires)

       {

-          Contract.Requires(@requires != null);

-          Contract.Ensures(Contract.Result<Requires>() != null);

-          this.VisitExpr(@requires.Condition);

-          return @requires;

+          Contract.Ensures(Contract.Result<Requires>() == requires);

+          this.VisitExpr(requires.Condition);

+          return requires;

       }

       public override List<Requires> VisitRequiresSeq(List<Requires> requiresSeq)

       {

-          Contract.Requires(requiresSeq != null);

-          Contract.Ensures(Contract.Result<List<Requires>>() != null);

+          Contract.Ensures(Contract.Result<List<Requires>>() == requiresSeq);

           for (int i = 0, n = requiresSeq.Count; i < n; i++)

               this.VisitRequires(requiresSeq[i]);

           return requiresSeq;

       }

-      public override Ensures VisitEnsures(Ensures @ensures)

+      public override Ensures VisitEnsures(Ensures ensures)

       {

-          Contract.Requires(@ensures != null);

-          Contract.Ensures(Contract.Result<Ensures>() != null);

-          this.VisitExpr(@ensures.Condition);

-          return @ensures;

+          Contract.Ensures(Contract.Result<Ensures>() == ensures);

+          this.VisitExpr(ensures.Condition);

+          return ensures;

       }

       public override List<Ensures> VisitEnsuresSeq(List<Ensures> ensuresSeq)

       {

-          Contract.Requires(ensuresSeq != null);

-          Contract.Ensures(Contract.Result<List<Ensures>>() != null);

+          Contract.Ensures(Contract.Result<List<Ensures>>() == ensuresSeq);

           for (int i = 0, n = ensuresSeq.Count; i < n; i++)

               this.VisitEnsures(ensuresSeq[i]);

           return ensuresSeq;

       }

       public override ForallExpr VisitForallExpr(ForallExpr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<ForallExpr>() != null);

+          Contract.Ensures(Contract.Result<ForallExpr>() == node);

           return (ForallExpr)this.VisitQuantifierExpr(node);

       }

       public override LambdaExpr VisitLambdaExpr(LambdaExpr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<LambdaExpr>() != null);

+          Contract.Ensures(Contract.Result<LambdaExpr>() == node);

           return (LambdaExpr)this.VisitBinderExpr(node);

       }

       public override Formal VisitFormal(Formal node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Formal>() != null);

+          Contract.Ensures(Contract.Result<Formal>() == node);

           return node;

       }

       public override Function VisitFunction(Function node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Function>() != null);

+          Contract.Ensures(Contract.Result<Function>() == node);

           node = (Function)this.VisitDeclWithFormals(node);

           if (node.Body != null)

               this.VisitExpr(node.Body);

@@ -894,44 +861,38 @@ namespace Microsoft.Boogie {
       }

       public override GlobalVariable VisitGlobalVariable(GlobalVariable node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<GlobalVariable>() != null);

+          Contract.Ensures(Contract.Result<GlobalVariable>() == node);

           return (GlobalVariable)this.VisitVariable(node);

       }

       public override GotoCmd VisitGotoCmd(GotoCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<GotoCmd>() != null);

+          Contract.Ensures(Contract.Result<GotoCmd>() == node);

           // do not visit the labelTargets, or control-flow loops will lead to a looping visitor

           return node;

       }

       public override Cmd VisitHavocCmd(HavocCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Cmd>() != null);

+          Contract.Ensures(Contract.Result<Cmd>() == node);

           this.VisitIdentifierExprSeq(node.Vars);

           return node;

       }

       public override Expr VisitIdentifierExpr(IdentifierExpr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Expr>() != null);

+          Contract.Ensures(Contract.Result<Expr>() == node);

           if (node.Decl != null)

               this.VisitVariable(node.Decl);

           return node;

       }

       public override List<IdentifierExpr> VisitIdentifierExprSeq(List<IdentifierExpr> identifierExprSeq)

       {

-          Contract.Requires(identifierExprSeq != null);

-          Contract.Ensures(Contract.Result<List<IdentifierExpr>>() != null);

+          Contract.Ensures(Contract.Result<List<IdentifierExpr>>() == identifierExprSeq);

           for (int i = 0, n = identifierExprSeq.Count; i < n; i++)

               this.VisitIdentifierExpr(cce.NonNull(identifierExprSeq[i]));

           return identifierExprSeq;

       }

       public override Implementation VisitImplementation(Implementation node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Implementation>() != null);

+          Contract.Ensures(Contract.Result<Implementation>() == node);

           this.VisitVariableSeq(node.LocVars);

           this.VisitBlockList(node.Blocks);

           this.VisitProcedure(cce.NonNull(node.Proc));

@@ -939,22 +900,19 @@ namespace Microsoft.Boogie {
       }

       public override LiteralExpr VisitLiteralExpr(LiteralExpr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<LiteralExpr>() != null);

+          Contract.Ensures(Contract.Result<LiteralExpr>() == node);

           return node;

       }

 

       public override LocalVariable VisitLocalVariable(LocalVariable node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<LocalVariable>() != null);

+          Contract.Ensures(Contract.Result<LocalVariable>() == node);

           return node;

       }

 

       public override AssignLhs VisitMapAssignLhs(MapAssignLhs node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<AssignLhs>() != null);

+          Contract.Ensures(Contract.Result<AssignLhs>() == node);

           this.Visit(node.Map);

           for (int i = 0; i < node.Indexes.Count; ++i)

               this.Visit(node.Indexes[i]);

@@ -962,8 +920,7 @@ namespace Microsoft.Boogie {
       }

       public override MapType VisitMapType(MapType node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<MapType>() != null);

+          Contract.Ensures(Contract.Result<MapType>() == node);

           // not doing anything about the bound variables ... maybe

           // these should be visited as well ...

           //

@@ -976,33 +933,29 @@ namespace Microsoft.Boogie {
       }

       public override Type VisitMapTypeProxy(MapTypeProxy node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Type>() != null);

+          Contract.Ensures(Contract.Result<Type>() == node);

           // if the type proxy is instantiated with some more

           // specific type, we visit the instantiation

           if (node.ProxyFor != null)

-              return (Type)this.Visit(node.ProxyFor);

+              this.Visit(node.ProxyFor);

           return this.VisitType(node);

       }

 

       public override Expr VisitNAryExpr(NAryExpr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Expr>() != null);

+          Contract.Ensures(Contract.Result<Expr>() == node);

           this.VisitExprSeq(node.Args);

           return node;

       }

       public override Expr VisitOldExpr(OldExpr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Expr>() != null);

+          Contract.Ensures(Contract.Result<Expr>() == node);

           this.VisitExpr(node.Expr);

           return node;

       }

       public override Procedure VisitProcedure(Procedure node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Procedure>() != null);

+          Contract.Ensures(Contract.Result<Procedure>() == node);

           this.VisitEnsuresSeq(node.Ensures);

           this.VisitVariableSeq(node.InParams);

           this.VisitIdentifierExprSeq(node.Modifies);

@@ -1012,15 +965,13 @@ namespace Microsoft.Boogie {
       }

       public override Program VisitProgram(Program node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Program>() != null);

+          Contract.Ensures(Contract.Result<Program>() == node);

           this.VisitDeclarationList(node.TopLevelDeclarations);

           return node;

       }

       public override BinderExpr VisitBinderExpr(BinderExpr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<BinderExpr>() != null);

+          Contract.Ensures(Contract.Result<BinderExpr>() == node);

           this.VisitExpr(node.Body);

           this.VisitVariableSeq(node.Dummies);

           // this.VisitType(node.Type);

@@ -1028,8 +979,7 @@ namespace Microsoft.Boogie {
       }

       public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<QuantifierExpr>() != null);

+          Contract.Ensures(Contract.Result<QuantifierExpr>() == node);

           this.VisitBinderExpr(node);

           if (node.Triggers != null)

           {

@@ -1039,64 +989,55 @@ namespace Microsoft.Boogie {
       }

       public override Cmd VisitRE(RE node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Cmd>() != null);

+          Contract.Ensures(Contract.Result<Cmd>() == node);

           return (Cmd)this.Visit(node); // Call general visit so subtypes get visited by their particular visitor

       }

       public override List<RE> VisitRESeq(List<RE> reSeq)

       {

-          Contract.Requires(reSeq != null);

-          Contract.Ensures(Contract.Result<List<RE>>() != null);

+          Contract.Ensures(Contract.Result<List<RE>>() == reSeq);

           for (int i = 0, n = reSeq.Count; i < n; i++)

               this.VisitRE(cce.NonNull(reSeq[i]));

           return reSeq;

       }

       public override ReturnCmd VisitReturnCmd(ReturnCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<ReturnCmd>() != null);

+          Contract.Ensures(Contract.Result<ReturnCmd>() == node);

           return (ReturnCmd)this.VisitTransferCmd(node);

       }

       public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<ReturnExprCmd>() != null);

+          Contract.Ensures(Contract.Result<ReturnExprCmd>() == node);

           this.VisitExpr(node.Expr);

           return node;

       }

       public override Sequential VisitSequential(Sequential node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Sequential>() != null);

+          Contract.Ensures(Contract.Result<Sequential>() == node);

           this.VisitRE(node.first);

           this.VisitRE(node.second);

           return node;

       }

       public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<AssignLhs>() != null);

+          Contract.Ensures(Contract.Result<AssignLhs>() == node);

           this.VisitIdentifierExpr(node.AssignedVariable);

           return node;

       }

       public override Cmd VisitStateCmd(StateCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Cmd>() != null);

+          Contract.Ensures(Contract.Result<Cmd>() == node);

           this.VisitVariableSeq(node.Locals);

           this.VisitCmdSeq(node.Cmds);

           return node;

       }

       public override TransferCmd VisitTransferCmd(TransferCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<TransferCmd>() != null);

+          Contract.Ensures(Contract.Result<TransferCmd>() == node);

           return node;

       }

       public override Trigger VisitTrigger(Trigger node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Trigger>() != null);

+          Contract.Ensures(Contract.Result<Trigger>() == node);

           Trigger origNext = node.Next;

           if (origNext != null)

           {

@@ -1108,27 +1049,23 @@ namespace Microsoft.Boogie {
       // called by default for all nullary type constructors and type variables

       public override Type VisitType(Type node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Type>() != null);

+          Contract.Ensures(Contract.Result<Type>() == node);

           return node;

       }

       public override TypedIdent VisitTypedIdent(TypedIdent node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<TypedIdent>() != null);

+          Contract.Ensures(Contract.Result<TypedIdent>() == node);

           this.Visit(node.Type);

           return node;

       }

       public override Declaration VisitTypeCtorDecl(TypeCtorDecl node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Declaration>() != null);

+          Contract.Ensures(Contract.Result<Declaration>() == node);

           return this.VisitDeclaration(node);

       }

       public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Type>() != null);

+          Contract.Ensures(Contract.Result<Type>() == node);

           node.ExpandedType = cce.NonNull((Type/*!*/)this.Visit(node.ExpandedType));

           for (int i = 0; i < node.Arguments.Count; ++i)

               this.Visit(node.Arguments[i]);

@@ -1136,65 +1073,56 @@ namespace Microsoft.Boogie {
       }

       public override Declaration VisitTypeSynonymDecl(TypeSynonymDecl node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Declaration>() != null);

+          Contract.Ensures(Contract.Result<Declaration>() == node);

           return this.VisitDeclaration(node);

       }

       public override Type VisitTypeVariable(TypeVariable node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Type>() != null);

+          Contract.Ensures(Contract.Result<Type>() == node);

           return this.VisitType(node);

       }

       public override Type VisitTypeProxy(TypeProxy node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Type>() != null);

+          Contract.Ensures(Contract.Result<Type>() == node);

           // if the type proxy is instantiated with some more

           // specific type, we visit the instantiation

           if (node.ProxyFor != null)

-              return cce.NonNull((Type/*!*/)this.Visit(node.ProxyFor));

+              this.Visit(node.ProxyFor);

           return this.VisitType(node);

       }

       public override Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Type>() != null);

+          Contract.Ensures(Contract.Result<Type>() == node);

           return this.VisitType(node);

       }

       public override Variable VisitVariable(Variable node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Variable>() != null);

+          Contract.Ensures(Contract.Result<Variable>() == node);

           this.VisitTypedIdent(node.TypedIdent);

           return node;

       }

       public override List<Variable> VisitVariableSeq(List<Variable> variableSeq)

       {

-          Contract.Requires(variableSeq != null);

-          Contract.Ensures(Contract.Result<List<Variable>>() != null);

+          Contract.Ensures(Contract.Result<List<Variable>>() == variableSeq);

           for (int i = 0, n = variableSeq.Count; i < n; i++)

               this.VisitVariable(cce.NonNull(variableSeq[i]));

           return variableSeq;

       }

       public override YieldCmd VisitYieldCmd(YieldCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<YieldCmd>() != null);

+          Contract.Ensures(Contract.Result<YieldCmd>() == node);

           return node;

       }

       public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Cmd>() != null);

+          Contract.Ensures(Contract.Result<Cmd>() == node);

           this.VisitEnsures(node.Ensures);

           this.VisitExpr(node.Expr);

           return node;

       }

       public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node)

       {

-          Contract.Requires(node != null);

-          Contract.Ensures(Contract.Result<Cmd>() != null);

+          Contract.Ensures(Contract.Result<Cmd>() == node);

           this.VisitRequires(node.Requires);

           this.VisitExpr(node.Expr);

           return node;

diff --git a/Source/Core/TypeAmbiguitySeeker.cs b/Source/Core/TypeAmbiguitySeeker.cs
index dac8ceb2..753385a1 100644
--- a/Source/Core/TypeAmbiguitySeeker.cs
+++ b/Source/Core/TypeAmbiguitySeeker.cs
@@ -14,7 +14,7 @@ using System.Collections.Generic;
 

 namespace Microsoft.Boogie {

 

-  public class TypeAmbiguitySeeker : StandardVisitor {

+  public class TypeAmbiguitySeeker : ReadOnlyVisitor {

 

     private readonly InTypeSeeker/*!*/ inTypeSeeker = new InTypeSeeker();

     private readonly TypecheckingContext/*!*/ TC;

@@ -62,7 +62,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  internal class InTypeSeeker : StandardVisitor {

+  internal class InTypeSeeker : ReadOnlyVisitor {

 

     internal bool FoundAmbiguity = false;

 

@@ -70,7 +70,7 @@ namespace Microsoft.Boogie {
     private Type Instantiate(Type node, Type inst) {

       Contract.Requires(inst != null);

       Contract.Requires(node != null);

-      Contract.Ensures(Contract.Result<Type>() != null);

+      Contract.Ensures(Contract.Result<Type>() == node);

       FoundAmbiguity = true;

       bool success = node.Unify(inst);

       Contract.Assert(success);

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)

         {

diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs
index 6119d522..a76566e4 100644
--- a/Source/Predication/UniformityAnalyser.cs
+++ b/Source/Predication/UniformityAnalyser.cs
@@ -396,7 +396,7 @@ namespace Microsoft.Boogie
             return !nonUniformBlocks[procedureName].Contains(b);

         }

 

-        class UniformExpressionAnalysisVisitor : StandardVisitor {

+        class UniformExpressionAnalysisVisitor : ReadOnlyVisitor {

 

           private bool isUniform = true;

           private Dictionary<string, bool> uniformityInfo;

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index bd8e7c79..a9963b72 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -49,7 +49,7 @@ namespace Microsoft.Boogie.VCExprAST {
 

   public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings, bool isPositiveContext);

 

-  public class Boogie2VCExprTranslator : StandardVisitor, ICloneable {

+  public class Boogie2VCExprTranslator : ReadOnlyVisitor, ICloneable {

     // Stack on which the various Visit-methods put the result of the translation

     private readonly Stack<VCExpr/*!*/>/*!*/ SubExpressions = new Stack<VCExpr>();

     [ContractInvariantMethod]