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/VCExpr/Boogie2VCExpr.cs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Source/VCExpr/Boogie2VCExpr.cs')

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