diff options
| author |  Rustan Leino <unknown> | 2014-02-24 22:54:32 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-24 22:54:32 -0800 |
| commit | 9a172309c91360449dd6211b39b96fdff0a7d2d0 (patch) | |
| tree | 54cc884e9f63c1e7dbe9167d50ab59b87ce8c4e7 /Source/VCExpr/Boogie2VCExpr.cs | |
| parent | d9dc7b51a3c1af9177f5b70cf7425b1990d25e77 (diff) | |
(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.
Diffstat (limited to 'Source/VCExpr/Boogie2VCExpr.cs')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 2 |
1 files changed, 1 insertions, 1 deletions
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]
|