diff options
Diffstat (limited to 'Source/Core/StandardVisitor.cs')
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 569 |
1 files changed, 560 insertions, 9 deletions
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 4605019f..d4be8ed4 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;
@@ -297,9 +295,9 @@ namespace Microsoft.Boogie { node = (ForallExpr)this.VisitQuantifierExpr(node);
return node;
}
- public virtual LambdaExpr VisitLambdaExpr(LambdaExpr node) {
+ public virtual Expr VisitLambdaExpr(LambdaExpr node) {
Contract.Requires(node != null);
- Contract.Ensures(Contract.Result<LambdaExpr>() != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
node = (LambdaExpr)this.VisitBinderExpr(node);
return node;
}
@@ -434,6 +432,20 @@ namespace Microsoft.Boogie { node.TopLevelDeclarations = this.VisitDeclarationList(node.TopLevelDeclarations);
return node;
}
+ public virtual QKeyValue VisitQKeyValue(QKeyValue node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<QKeyValue>() != null);
+ for (int i = 0, n = node.Params.Count; i < n; i++) {
+ var e = node.Params[i] as Expr;
+ if (e != null) {
+ node.Params[i] = (Expr)this.Visit(e);
+ }
+ }
+ if (node.Next != null) {
+ node.Next = (QKeyValue)this.Visit(node.Next);
+ }
+ return node;
+ }
public virtual BinderExpr VisitBinderExpr(BinderExpr node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<BinderExpr>() != null);
@@ -603,4 +615,543 @@ namespace Microsoft.Boogie { return node;
}
}
+
+ /// <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()
+ {
+ }
+ public ReadOnlyVisitor(Visitor callingVisitor)
+ {
+ this.callingVisitor = callingVisitor;
+ }
+ public override Absy Visit(Absy node)
+ {
+ Contract.Ensures(Contract.Result<Absy>() == node);
+ return node.StdDispatch(this);
+ }
+ public override Cmd VisitAssertCmd(AssertCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ public override Cmd VisitAssignCmd(AssignCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ for (int i = 0; i < node.Lhss.Count; ++i)
+ {
+ this.Visit(node.Lhss[i]);
+ this.Visit(node.Rhss[i]);
+ }
+ return node;
+ }
+ public override Cmd VisitAssumeCmd(AssumeCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ public override AtomicRE VisitAtomicRE(AtomicRE node)
+ {
+ Contract.Ensures(Contract.Result<AtomicRE>() == node);
+ this.VisitBlock(node.b);
+ return node;
+ }
+ public override Axiom VisitAxiom(Axiom node)
+ {
+ Contract.Ensures(Contract.Result<Axiom>() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ public override Type VisitBasicType(BasicType node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ return this.VisitType(node);
+ }
+ public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node)
+ {
+ Contract.Ensures(Contract.Result<BvConcatExpr>() == node);
+ this.VisitExpr(node.E0);
+ this.VisitExpr(node.E1);
+ return node;
+ }
+ public override Type VisitBvType(BvType node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ return this.VisitType(node);
+ }
+ public override Type VisitBvTypeProxy(BvTypeProxy node)
+ {
+ 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)
+ this.Visit(node.ProxyFor);
+ return this.VisitType(node);
+ }
+ public override Block VisitBlock(Block node)
+ {
+ 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.Ensures(Contract.Result<Expr>() == node);
+ this.VisitVariableSeq(node.LocVars);
+ this.VisitBlockList(node.Blocks);
+ return node;
+ }
+ public override List<Block> VisitBlockSeq(List<Block> blockSeq)
+ {
+ 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.Ensures(Contract.Result<List<Block>>() == blocks);
+ for (int i = 0, n = blocks.Count; i < n; i++)
+ {
+ this.VisitBlock(blocks[i]);
+ }
+ return blocks;
+ }
+ public override BoundVariable VisitBoundVariable(BoundVariable node)
+ {
+ Contract.Ensures(Contract.Result<BoundVariable>() == node);
+ return (BoundVariable)this.VisitVariable(node);
+ }
+ public override Cmd VisitCallCmd(CallCmd node)
+ {
+ 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]);
+ for (int i = 0; i < node.Outs.Count; ++i)
+ if (node.Outs[i] != null)
+ this.VisitIdentifierExpr(node.Outs[i]);
+ return node;
+ }
+ public override Cmd VisitParCallCmd(ParCallCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ for (int i = 0; i < node.CallCmds.Count; i++)
+ {
+ if (node.CallCmds[i] != null)
+ this.VisitCallCmd(node.CallCmds[i]);
+ }
+ return node;
+ }
+ public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq)
+ {
+ 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.Ensures(Contract.Result<Choice>() == node);
+ this.VisitRESeq(node.rs);
+ return node;
+ }
+ public override Cmd VisitCommentCmd(CommentCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ return node;
+ }
+ public override Constant VisitConstant(Constant node)
+ {
+ Contract.Ensures(Contract.Result<Constant>() == node);
+ return node;
+ }
+ public override CtorType VisitCtorType(CtorType node)
+ {
+ 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.Ensures(Contract.Result<Declaration>() == node);
+ return node;
+ }
+ public override List<Declaration/*!*/>/*!*/ VisitDeclarationList(List<Declaration/*!*/>/*!*/ declarationList)
+ {
+ 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.Ensures(Contract.Result<DeclWithFormals>() == node);
+ this.VisitVariableSeq(node.InParams);
+ this.VisitVariableSeq(node.OutParams);
+ return node;
+ }
+ public override ExistsExpr VisitExistsExpr(ExistsExpr node)
+ {
+ Contract.Ensures(Contract.Result<ExistsExpr>() == node);
+ return (ExistsExpr)this.VisitQuantifierExpr(node);
+ }
+ public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node)
+ {
+ Contract.Ensures(Contract.Result<BvExtractExpr>() == node);
+ this.VisitExpr(node.Bitvector);
+ return node;
+ }
+ public override Expr VisitExpr(Expr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() == node);
+ return (Expr)this.Visit(node);
+ }
+ public override List<Expr> VisitExprSeq(List<Expr> exprSeq)
+ {
+ 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)
+ {
+ Contract.Ensures(Contract.Result<Requires>() == requires);
+ this.VisitExpr(requires.Condition);
+ return requires;
+ }
+ public override List<Requires> VisitRequiresSeq(List<Requires> requiresSeq)
+ {
+ 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)
+ {
+ Contract.Ensures(Contract.Result<Ensures>() == ensures);
+ this.VisitExpr(ensures.Condition);
+ return ensures;
+ }
+ public override List<Ensures> VisitEnsuresSeq(List<Ensures> ensuresSeq)
+ {
+ 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.Ensures(Contract.Result<ForallExpr>() == node);
+ return (ForallExpr)this.VisitQuantifierExpr(node);
+ }
+ public override Expr VisitLambdaExpr(LambdaExpr node) {
+ Contract.Ensures(Contract.Result<Expr>() == node);
+ return this.VisitBinderExpr(node);
+ }
+ public override Formal VisitFormal(Formal node)
+ {
+ Contract.Ensures(Contract.Result<Formal>() == node);
+ return node;
+ }
+ public override Function VisitFunction(Function node)
+ {
+ Contract.Ensures(Contract.Result<Function>() == node);
+ node = (Function)this.VisitDeclWithFormals(node);
+ if (node.Body != null)
+ this.VisitExpr(node.Body);
+ return node;
+ }
+ public override GlobalVariable VisitGlobalVariable(GlobalVariable node)
+ {
+ Contract.Ensures(Contract.Result<GlobalVariable>() == node);
+ return (GlobalVariable)this.VisitVariable(node);
+ }
+ public override GotoCmd VisitGotoCmd(GotoCmd node)
+ {
+ 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.Ensures(Contract.Result<Cmd>() == node);
+ this.VisitIdentifierExprSeq(node.Vars);
+ return node;
+ }
+ public override Expr VisitIdentifierExpr(IdentifierExpr node)
+ {
+ 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.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.Ensures(Contract.Result<Implementation>() == node);
+ this.VisitVariableSeq(node.LocVars);
+ this.VisitBlockList(node.Blocks);
+ this.VisitProcedure(cce.NonNull(node.Proc));
+ return (Implementation)this.VisitDeclWithFormals(node); // do this first or last?
+ }
+ public override LiteralExpr VisitLiteralExpr(LiteralExpr node)
+ {
+ Contract.Ensures(Contract.Result<LiteralExpr>() == node);
+ return node;
+ }
+
+ public override LocalVariable VisitLocalVariable(LocalVariable node)
+ {
+ Contract.Ensures(Contract.Result<LocalVariable>() == node);
+ return node;
+ }
+
+ public override AssignLhs VisitMapAssignLhs(MapAssignLhs node)
+ {
+ Contract.Ensures(Contract.Result<AssignLhs>() == node);
+ this.Visit(node.Map);
+ for (int i = 0; i < node.Indexes.Count; ++i)
+ this.Visit(node.Indexes[i]);
+ return node;
+ }
+ public override MapType VisitMapType(MapType node)
+ {
+ Contract.Ensures(Contract.Result<MapType>() == node);
+ // not doing anything about the bound variables ... maybe
+ // these should be visited as well ...
+ //
+ // NOTE: when overriding this method, you have to make sure that
+ // the bound variables of the map type are updated correctly
+ for (int i = 0; i < node.Arguments.Count; ++i)
+ this.Visit(node.Arguments[i]);
+ this.Visit(node.Result);
+ return node;
+ }
+ public override Type VisitMapTypeProxy(MapTypeProxy node)
+ {
+ 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)
+ this.Visit(node.ProxyFor);
+ return this.VisitType(node);
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() == node);
+ this.VisitExprSeq(node.Args);
+ return node;
+ }
+ public override Expr VisitOldExpr(OldExpr node)
+ {
+ Contract.Ensures(Contract.Result<Expr>() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ public override Procedure VisitProcedure(Procedure node)
+ {
+ Contract.Ensures(Contract.Result<Procedure>() == node);
+ this.VisitEnsuresSeq(node.Ensures);
+ this.VisitVariableSeq(node.InParams);
+ this.VisitIdentifierExprSeq(node.Modifies);
+ this.VisitVariableSeq(node.OutParams);
+ this.VisitRequiresSeq(node.Requires);
+ return node;
+ }
+ public override Program VisitProgram(Program node)
+ {
+ Contract.Ensures(Contract.Result<Program>() == node);
+ this.VisitDeclarationList(node.TopLevelDeclarations);
+ return node;
+ }
+ public override QKeyValue VisitQKeyValue(QKeyValue node) {
+ Contract.Ensures(Contract.Result<QKeyValue>() == node);
+ for (int i = 0, n = node.Params.Count; i < n; i++) {
+ var e = node.Params[i] as Expr;
+ if (e != null) {
+ this.Visit(e);
+ }
+ }
+ if (node.Next != null) {
+ this.Visit(node.Next);
+ }
+ return node;
+ }
+ public override BinderExpr VisitBinderExpr(BinderExpr node)
+ {
+ Contract.Ensures(Contract.Result<BinderExpr>() == node);
+ this.VisitExpr(node.Body);
+ this.VisitVariableSeq(node.Dummies);
+ // this.VisitType(node.Type);
+ return node;
+ }
+ public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node)
+ {
+ Contract.Ensures(Contract.Result<QuantifierExpr>() == node);
+ this.VisitBinderExpr(node);
+ if (node.Triggers != null)
+ {
+ this.VisitTrigger(node.Triggers);
+ }
+ return node;
+ }
+ public override Cmd VisitRE(RE node)
+ {
+ 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.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.Ensures(Contract.Result<ReturnCmd>() == node);
+ return (ReturnCmd)this.VisitTransferCmd(node);
+ }
+ public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node)
+ {
+ Contract.Ensures(Contract.Result<ReturnExprCmd>() == node);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ public override Sequential VisitSequential(Sequential node)
+ {
+ Contract.Ensures(Contract.Result<Sequential>() == node);
+ this.VisitRE(node.first);
+ this.VisitRE(node.second);
+ return node;
+ }
+ public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node)
+ {
+ Contract.Ensures(Contract.Result<AssignLhs>() == node);
+ this.VisitIdentifierExpr(node.AssignedVariable);
+ return node;
+ }
+ public override Cmd VisitStateCmd(StateCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ this.VisitVariableSeq(node.Locals);
+ this.VisitCmdSeq(node.Cmds);
+ return node;
+ }
+ public override TransferCmd VisitTransferCmd(TransferCmd node)
+ {
+ Contract.Ensures(Contract.Result<TransferCmd>() == node);
+ return node;
+ }
+ public override Trigger VisitTrigger(Trigger node)
+ {
+ Contract.Ensures(Contract.Result<Trigger>() == node);
+ Trigger origNext = node.Next;
+ if (origNext != null)
+ {
+ this.VisitTrigger(origNext);
+ }
+ this.VisitExprSeq(node.Tr);
+ return node;
+ }
+ // called by default for all nullary type constructors and type variables
+ public override Type VisitType(Type node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ return node;
+ }
+ public override TypedIdent VisitTypedIdent(TypedIdent node)
+ {
+ Contract.Ensures(Contract.Result<TypedIdent>() == node);
+ this.Visit(node.Type);
+ return node;
+ }
+ public override Declaration VisitTypeCtorDecl(TypeCtorDecl node)
+ {
+ Contract.Ensures(Contract.Result<Declaration>() == node);
+ return this.VisitDeclaration(node);
+ }
+ public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node)
+ {
+ 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]);
+ return node;
+ }
+ public override Declaration VisitTypeSynonymDecl(TypeSynonymDecl node)
+ {
+ Contract.Ensures(Contract.Result<Declaration>() == node);
+ return this.VisitDeclaration(node);
+ }
+ public override Type VisitTypeVariable(TypeVariable node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ return this.VisitType(node);
+ }
+ public override Type VisitTypeProxy(TypeProxy node)
+ {
+ 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)
+ this.Visit(node.ProxyFor);
+ return this.VisitType(node);
+ }
+ public override Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node)
+ {
+ Contract.Ensures(Contract.Result<Type>() == node);
+ return this.VisitType(node);
+ }
+ public override Variable VisitVariable(Variable node)
+ {
+ Contract.Ensures(Contract.Result<Variable>() == node);
+ this.VisitTypedIdent(node.TypedIdent);
+ return node;
+ }
+ public override List<Variable> VisitVariableSeq(List<Variable> variableSeq)
+ {
+ 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.Ensures(Contract.Result<YieldCmd>() == node);
+ return node;
+ }
+ public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ this.VisitEnsures(node.Ensures);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node)
+ {
+ Contract.Ensures(Contract.Result<Cmd>() == node);
+ this.VisitRequires(node.Requires);
+ this.VisitExpr(node.Expr);
+ return node;
+ }
+ }
}
|