diff options
| author |  tabarbe <unknown> | 2010-08-20 22:32:24 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-20 22:32:24 +0000 |
| commit | 72b39a6962d7f6c7ca1aab9919791238c7baba3f (patch) | |
| tree | 75bb9c1b956d1b368f4cf2983a20a913211dd350 /Source/Core/StandardVisitor.cs | |
| parent | 96d9624e9e22dbe9090e0bd7d538cafbf0a16463 (diff) | |
Boogie: Committing changed source files
Diffstat (limited to 'Source/Core/StandardVisitor.cs')
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 500 |
1 files changed, 291 insertions, 209 deletions
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 10984ff3..528e442f 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -8,150 +8,174 @@ //---------------------------------------------------------------------------------------------
using System.Collections.Generic;
+using System.Diagnostics.Contracts;
-namespace Microsoft.Boogie
-{
+namespace Microsoft.Boogie {
+ [ContractClass(typeof(VisitorContracts))]
/// <summary>
/// Base for all classes that process the Absy using the visitor pattern.
/// </summary>
- public abstract class Visitor
- {
+ public abstract class Visitor {
/// <summary>
/// Switches on node.NodeType to call a visitor method that has been specialized for node.
/// </summary>
/// <param name="a">The Absy node to be visited.</param>
/// <returns> Returns null if node is null. Otherwise returns an updated node (possibly a different object).</returns>
- public abstract Absy! Visit (Absy! node);
-
+ public abstract Absy/*!*/ Visit(Absy/*!*/ node);
+
/// <summary>
/// Transfers the state from one visitor to another. This enables separate visitor instances to cooperative process a single IR.
/// </summary>
- public virtual void TransferStateTo(Visitor targetVisitor)
- {
+ public virtual void TransferStateTo(Visitor targetVisitor) {
}
- public virtual ExprSeq! VisitExprSeq(ExprSeq! list)
- {
- for( int i = 0, n = list.Length; i < n; i++)
- list[i] = (Expr)this.Visit( (!) list[i]);
+ public virtual ExprSeq VisitExprSeq(ExprSeq list) {
+ Contract.Requires(list != null);
+ Contract.Ensures(Contract.Result<ExprSeq>() != null);
+ for (int i = 0, n = list.Length; i < n; i++)
+ list[i] = (Expr)this.Visit(cce.NonNull(list[i]));
return list;
}
}
+ [ContractClassFor(typeof(Visitor))]
+ abstract class VisitorContracts : Visitor {
+ public override Absy Visit(Absy node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
+
+ throw new System.NotImplementedException();
+ }
+ }
/// <summary>
/// Walks an IR, mutuating it into a new form
/// </summary>
- public abstract class StandardVisitor: Visitor
- {
+ public abstract class StandardVisitor : Visitor {
public Visitor callingVisitor;
-
- public StandardVisitor()
- {
+
+ public StandardVisitor() {
}
- public StandardVisitor(Visitor callingVisitor)
- {
+ public StandardVisitor(Visitor callingVisitor) {
this.callingVisitor = callingVisitor;
}
- public override Absy! Visit (Absy! node)
- {
+ public override Absy Visit(Absy node) {
+ //Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return node.StdDispatch(this);
}
- public virtual AIVariableExpr! VisitAIVariableExpr(AIVariableExpr! node)
- {
+ public virtual AIVariableExpr VisitAIVariableExpr(AIVariableExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<AIVariableExpr>() != null);
return node;
}
- public virtual Cmd! VisitAssertCmd(AssertCmd! node)
- {
+ public virtual Cmd VisitAssertCmd(AssertCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
node.Expr = this.VisitExpr(node.Expr);
return node;
}
- public virtual Cmd! VisitAssignCmd(AssignCmd! node)
- {
+ public virtual Cmd VisitAssignCmd(AssignCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
for (int i = 0; i < node.Lhss.Count; ++i) {
- node.Lhss[i] = (AssignLhs!)this.Visit(node.Lhss[i]);
- node.Rhss[i] = (Expr!)this.Visit(node.Rhss[i]);
+ node.Lhss[i] = cce.NonNull((AssignLhs)this.Visit(node.Lhss[i]));
+ node.Rhss[i] = cce.NonNull((Expr/*!*/)this.Visit(node.Rhss[i]));
}
return node;
}
- public virtual Cmd! VisitAssumeCmd(AssumeCmd! node)
- {
+ public virtual Cmd VisitAssumeCmd(AssumeCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
node.Expr = this.VisitExpr(node.Expr);
return node;
}
- public virtual AtomicRE! VisitAtomicRE(AtomicRE! node)
- {
+ public virtual AtomicRE VisitAtomicRE(AtomicRE node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<AtomicRE>() != null);
node.b = this.VisitBlock(node.b);
return node;
}
- public virtual Axiom! VisitAxiom(Axiom! node)
- {
+ public virtual Axiom VisitAxiom(Axiom node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Axiom>() != null);
node.Expr = this.VisitExpr(node.Expr);
return node;
}
- public virtual Type! VisitBasicType(BasicType! node)
- {
+ public virtual Type VisitBasicType(BasicType node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
return this.VisitType(node);
}
- public virtual BvConcatExpr! VisitBvConcatExpr(BvConcatExpr! node)
- {
+ public virtual BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<BvConcatExpr>() != null);
node.E0 = this.VisitExpr(node.E0);
node.E1 = this.VisitExpr(node.E1);
return node;
}
- public virtual Type! VisitBvType(BvType! node)
- {
+ public virtual Type VisitBvType(BvType node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
return this.VisitType(node);
}
- public virtual Type! VisitBvTypeProxy(BvTypeProxy! node)
- {
+ public virtual Type VisitBvTypeProxy(BvTypeProxy node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
// 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);
return this.VisitType(node);
}
- public virtual Block! VisitBlock(Block! node)
- {
+ public virtual Block VisitBlock(Block node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Block>() != null);
node.Cmds = this.VisitCmdSeq(node.Cmds);
- node.TransferCmd = (TransferCmd)this.Visit((!)node.TransferCmd);
+ node.TransferCmd = (TransferCmd)this.Visit(cce.NonNull(node.TransferCmd));
return node;
}
- public virtual Expr! VisitCodeExpr(CodeExpr! node)
- {
+ public virtual Expr VisitCodeExpr(CodeExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
node.LocVars = this.VisitVariableSeq(node.LocVars);
node.Blocks = this.VisitBlockList(node.Blocks);
return node;
}
- public virtual BlockSeq! VisitBlockSeq(BlockSeq! blockSeq)
- {
+ public virtual BlockSeq VisitBlockSeq(BlockSeq blockSeq) {
+ Contract.Requires(blockSeq != null);
+ Contract.Ensures(Contract.Result<BlockSeq>() != null);
for (int i = 0, n = blockSeq.Length; i < n; i++)
- blockSeq[i] = this.VisitBlock( (!)blockSeq[i]);
+ blockSeq[i] = this.VisitBlock(cce.NonNull(blockSeq[i]));
return blockSeq;
}
- public virtual List<Block!>! VisitBlockList(List<Block!>! blocks)
- {
+ public virtual List<Block/*!*/>/*!*/ VisitBlockList(List<Block/*!*/>/*!*/ blocks) {
+ Contract.Requires(cce.NonNullElements(blocks));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
for (int i = 0, n = blocks.Count; i < n; i++) {
blocks[i] = this.VisitBlock(blocks[i]);
}
return blocks;
}
- public virtual BoundVariable! VisitBoundVariable(BoundVariable! node)
- {
- node = (BoundVariable) this.VisitVariable(node);
+ public virtual BoundVariable VisitBoundVariable(BoundVariable node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<BoundVariable>() != null);
+ node = (BoundVariable)this.VisitVariable(node);
return node;
}
- public virtual Cmd! VisitCallCmd(CallCmd! node)
- {
+ public virtual Cmd VisitCallCmd(CallCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
for (int i = 0; i < node.Ins.Count; ++i)
if (node.Ins[i] != null)
- node.Ins[i] = this.VisitExpr((!)node.Ins[i]);
+ node.Ins[i] = this.VisitExpr(cce.NonNull(node.Ins[i]));
for (int i = 0; i < node.Outs.Count; ++i)
if (node.Outs[i] != null)
- node.Outs[i] = (IdentifierExpr)this.VisitIdentifierExpr((!)node.Outs[i]);
+ node.Outs[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(node.Outs[i]));
return node;
}
- public virtual Cmd! VisitCallForallCmd(CallForallCmd! node)
- {
+ public virtual Cmd VisitCallForallCmd(CallForallCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
List<Expr> elist = new List<Expr>(node.Ins.Count);
foreach (Expr arg in node.Ins) {
if (arg == null) {
@@ -161,180 +185,211 @@ namespace Microsoft.Boogie }
}
node.Ins = elist;
- node.Proc = this.VisitProcedure((!)node.Proc);
+ node.Proc = this.VisitProcedure(cce.NonNull(node.Proc));
return node;
}
- public virtual CmdSeq! VisitCmdSeq(CmdSeq! cmdSeq)
- {
+ public virtual CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
+ Contract.Requires(cmdSeq != null);
+ Contract.Ensures(Contract.Result<CmdSeq>() != null);
for (int i = 0, n = cmdSeq.Length; i < n; i++)
- cmdSeq[i] = (Cmd) this.Visit( (!)cmdSeq[i]); // call general Visit so subtypes of Cmd get visited by their particular visitor
+ cmdSeq[i] = (Cmd)this.Visit(cce.NonNull(cmdSeq[i])); // call general Visit so subtypes of Cmd get visited by their particular visitor
return cmdSeq;
}
- public virtual Choice! VisitChoice(Choice! node)
- {
+ public virtual Choice VisitChoice(Choice node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Choice>() != null);
node.rs = this.VisitRESeq(node.rs);
return node;
}
- public virtual Cmd! VisitCommentCmd(CommentCmd! node)
- {
+ public virtual Cmd VisitCommentCmd(CommentCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
return node;
}
- public virtual Constant! VisitConstant(Constant! node)
- {
+ public virtual Constant VisitConstant(Constant node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Constant>() != null);
return node;
}
- public virtual CtorType! VisitCtorType(CtorType! node)
- {
+ public virtual CtorType VisitCtorType(CtorType node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<CtorType>() != null);
for (int i = 0; i < node.Arguments.Length; ++i)
- node.Arguments[i] = (Type!)this.Visit(node.Arguments[i]);
+ node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));
return node;
}
- public virtual Declaration! VisitDeclaration(Declaration! node)
- {
+ public virtual Declaration VisitDeclaration(Declaration node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Declaration>() != null);
return node;
}
- public virtual List<Declaration!>! VisitDeclarationList(List<Declaration!>! declarationList)
- {
+ public virtual List<Declaration/*!*/>/*!*/ VisitDeclarationList(List<Declaration/*!*/>/*!*/ declarationList) {
+ Contract.Requires(cce.NonNullElements(declarationList));
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Declaration>>()));
for (int i = 0, n = declarationList.Count; i < n; i++)
- declarationList[i] = (Declaration!) this.Visit(declarationList[i]);
+ declarationList[i] = cce.NonNull((Declaration/*!*/)this.Visit(declarationList[i]));
return declarationList;
}
- public virtual DeclWithFormals! VisitDeclWithFormals(DeclWithFormals! node)
- {
+ public virtual DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<DeclWithFormals>() != null);
node.InParams = this.VisitVariableSeq(node.InParams);
node.OutParams = this.VisitVariableSeq(node.OutParams);
return node;
}
- public virtual ExistsExpr! VisitExistsExpr(ExistsExpr! node)
- {
- node = (ExistsExpr) this.VisitQuantifierExpr(node);
+ public virtual ExistsExpr VisitExistsExpr(ExistsExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<ExistsExpr>() != null);
+ node = (ExistsExpr)this.VisitQuantifierExpr(node);
return node;
}
- public virtual BvExtractExpr! VisitBvExtractExpr(BvExtractExpr! node)
- {
+ public virtual BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<BvExtractExpr>() != null);
node.Bitvector = this.VisitExpr(node.Bitvector);
return node;
}
- public virtual Expr! VisitExpr(Expr! node)
- {
- Expr e = (Expr) this.Visit(node);
+ public virtual Expr VisitExpr(Expr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ Expr e = (Expr)this.Visit(node);
return e;
}
- public override ExprSeq! VisitExprSeq(ExprSeq! exprSeq)
- {
+ public override ExprSeq VisitExprSeq(ExprSeq exprSeq) {
+ //Contract.Requires(exprSeq != null);
+ Contract.Ensures(Contract.Result<ExprSeq>() != null);
for (int i = 0, n = exprSeq.Length; i < n; i++)
- exprSeq[i] = this.VisitExpr( (!)exprSeq[i]);
+ exprSeq[i] = this.VisitExpr(cce.NonNull(exprSeq[i]));
return exprSeq;
}
- public virtual Requires! VisitRequires(Requires! @requires)
- {
+ public virtual Requires VisitRequires(Requires @requires) {
+ Contract.Requires(@requires != null);
+ Contract.Ensures(Contract.Result<Requires>() != null);
@requires.Condition = this.VisitExpr(@requires.Condition);
return @requires;
}
- public virtual RequiresSeq! VisitRequiresSeq(RequiresSeq! requiresSeq)
- {
+ public virtual RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) {
+ Contract.Requires(requiresSeq != null);
+ Contract.Ensures(Contract.Result<RequiresSeq>() != null);
for (int i = 0, n = requiresSeq.Length; i < n; i++)
requiresSeq[i] = this.VisitRequires(requiresSeq[i]);
return requiresSeq;
}
- public virtual Ensures! VisitEnsures(Ensures! @ensures)
- {
+ public virtual Ensures VisitEnsures(Ensures @ensures) {
+ Contract.Requires(@ensures != null);
+ Contract.Ensures(Contract.Result<Ensures>() != null);
@ensures.Condition = this.VisitExpr(@ensures.Condition);
return @ensures;
}
- public virtual EnsuresSeq! VisitEnsuresSeq(EnsuresSeq! ensuresSeq)
- {
+ public virtual EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) {
+ Contract.Requires(ensuresSeq != null);
+ Contract.Ensures(Contract.Result<EnsuresSeq>() != null);
for (int i = 0, n = ensuresSeq.Length; i < n; i++)
ensuresSeq[i] = this.VisitEnsures(ensuresSeq[i]);
return ensuresSeq;
}
- public virtual ForallExpr! VisitForallExpr(ForallExpr! node)
- {
- node = (ForallExpr) this.VisitQuantifierExpr(node);
+ public virtual ForallExpr VisitForallExpr(ForallExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<ForallExpr>() != null);
+ node = (ForallExpr)this.VisitQuantifierExpr(node);
return node;
}
- public virtual LambdaExpr! VisitLambdaExpr(LambdaExpr! node)
- {
- node = (LambdaExpr) this.VisitBinderExpr(node);
+ public virtual LambdaExpr VisitLambdaExpr(LambdaExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<LambdaExpr>() != null);
+ node = (LambdaExpr)this.VisitBinderExpr(node);
return node;
}
- public virtual Formal! VisitFormal(Formal! node)
- {
+ public virtual Formal VisitFormal(Formal node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Formal>() != null);
return node;
}
- public virtual Function! VisitFunction(Function! node)
- {
- node = (Function) this.VisitDeclWithFormals(node);
+ public virtual Function VisitFunction(Function node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Function>() != null);
+ node = (Function)this.VisitDeclWithFormals(node);
if (node.Body != null)
node.Body = this.VisitExpr(node.Body);
return node;
}
- public virtual GlobalVariable! VisitGlobalVariable(GlobalVariable! node)
- {
- node = (GlobalVariable) this.VisitVariable(node);
+ public virtual GlobalVariable VisitGlobalVariable(GlobalVariable node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<GlobalVariable>() != null);
+ node = (GlobalVariable)this.VisitVariable(node);
return node;
}
- public virtual GotoCmd! VisitGotoCmd(GotoCmd! node)
- {
+ public virtual GotoCmd VisitGotoCmd(GotoCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<GotoCmd>() != null);
// do not visit the labelTargets, or control-flow loops will lead to a looping visitor
return node;
}
- public virtual Cmd! VisitHavocCmd(HavocCmd! node)
- {
+ public virtual Cmd VisitHavocCmd(HavocCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
node.Vars = this.VisitIdentifierExprSeq(node.Vars);
return node;
}
- public virtual Expr! VisitIdentifierExpr(IdentifierExpr! node)
- {
+ public virtual Expr VisitIdentifierExpr(IdentifierExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
if (node.Decl != null)
node.Decl = this.VisitVariable(node.Decl);
return node;
}
- public virtual IdentifierExprSeq! VisitIdentifierExprSeq(IdentifierExprSeq! identifierExprSeq)
- {
+ public virtual IdentifierExprSeq VisitIdentifierExprSeq(IdentifierExprSeq identifierExprSeq) {
+ Contract.Requires(identifierExprSeq != null);
+ Contract.Ensures(Contract.Result<IdentifierExprSeq>() != null);
for (int i = 0, n = identifierExprSeq.Length; i < n; i++)
- identifierExprSeq[i] = (IdentifierExpr) this.VisitIdentifierExpr( (!)identifierExprSeq[i]);
+ identifierExprSeq[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(identifierExprSeq[i]));
return identifierExprSeq;
}
- public virtual Implementation! VisitImplementation(Implementation! node)
- {
+ public virtual Implementation VisitImplementation(Implementation node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Implementation>() != null);
node.LocVars = this.VisitVariableSeq(node.LocVars);
node.Blocks = this.VisitBlockList(node.Blocks);
- node.Proc = this.VisitProcedure((!)node.Proc);
- node = (Implementation) this.VisitDeclWithFormals(node); // do this first or last?
+ node.Proc = this.VisitProcedure(cce.NonNull(node.Proc));
+ node = (Implementation)this.VisitDeclWithFormals(node); // do this first or last?
return node;
}
- public virtual LiteralExpr! VisitLiteralExpr(LiteralExpr! node)
- {
+ public virtual LiteralExpr VisitLiteralExpr(LiteralExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return node;
}
- public virtual LocalVariable! VisitLocalVariable(LocalVariable! node)
- {
+ public virtual LocalVariable VisitLocalVariable(LocalVariable node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<LocalVariable>() != null);
return node;
}
- public virtual AssignLhs! VisitMapAssignLhs(MapAssignLhs! node)
- {
- node.Map = (AssignLhs!)this.Visit(node.Map);
+ public virtual AssignLhs VisitMapAssignLhs(MapAssignLhs node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<AssignLhs>() != null);
+ node.Map = cce.NonNull((AssignLhs)this.Visit(node.Map));
for (int i = 0; i < node.Indexes.Count; ++i)
- node.Indexes[i] = (Expr!)this.Visit(node.Indexes[i]);
+ node.Indexes[i] = cce.NonNull((Expr)this.Visit(node.Indexes[i]));
return node;
}
- public virtual MapType! VisitMapType(MapType! node)
- {
+ public virtual MapType VisitMapType(MapType node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<MapType>() != null);
// 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.Length; ++i)
- node.Arguments[i] = (Type!)this.Visit(node.Arguments[i]);
- node.Result = (Type!)this.Visit(node.Result);
+ node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));
+ node.Result = cce.NonNull((Type/*!*/)this.Visit(node.Result));
return node;
}
- public virtual Type! VisitMapTypeProxy(MapTypeProxy! node)
- {
+ public virtual Type VisitMapTypeProxy(MapTypeProxy node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
// if the type proxy is instantiated with some more
// specific type, we visit the instantiation
if (node.ProxyFor != null)
@@ -342,18 +397,21 @@ namespace Microsoft.Boogie return this.VisitType(node);
}
- public virtual Expr! VisitNAryExpr(NAryExpr! node)
- {
+ public virtual Expr VisitNAryExpr(NAryExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
node.Args = this.VisitExprSeq(node.Args);
return node;
}
- public virtual Expr! VisitOldExpr(OldExpr! node)
- {
+ public virtual Expr VisitOldExpr(OldExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
node.Expr = this.VisitExpr(node.Expr);
return node;
}
- public virtual Procedure! VisitProcedure(Procedure! node)
- {
+ public virtual Procedure VisitProcedure(Procedure node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Procedure>() != null);
node.Ensures = this.VisitEnsuresSeq(node.Ensures);
node.InParams = this.VisitVariableSeq(node.InParams);
node.Modifies = this.VisitIdentifierExprSeq(node.Modifies);
@@ -361,69 +419,81 @@ namespace Microsoft.Boogie node.Requires = this.VisitRequiresSeq(node.Requires);
return node;
}
- public virtual Program! VisitProgram(Program! node)
- {
+ public virtual Program VisitProgram(Program node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Program>() != null);
node.TopLevelDeclarations = this.VisitDeclarationList(node.TopLevelDeclarations);
return node;
}
- public virtual BinderExpr! VisitBinderExpr(BinderExpr! node)
- {
+ public virtual BinderExpr VisitBinderExpr(BinderExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<BinderExpr>() != null);
node.Body = this.VisitExpr(node.Body);
node.Dummies = this.VisitVariableSeq(node.Dummies);
//node.Type = this.VisitType(node.Type);
return node;
}
- public virtual QuantifierExpr! VisitQuantifierExpr(QuantifierExpr! node)
- {
- node = (QuantifierExpr!) this.VisitBinderExpr(node);
+ public virtual QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<QuantifierExpr>() != null);
+ node = cce.NonNull((QuantifierExpr)this.VisitBinderExpr(node));
if (node.Triggers != null) {
node.Triggers = this.VisitTrigger(node.Triggers);
}
return node;
}
- public virtual Cmd! VisitRE(RE! node)
- {
- return (Cmd) this.Visit(node); // Call general visit so subtypes get visited by their particular visitor
+ public virtual Cmd VisitRE(RE node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
+ return (Cmd)this.Visit(node); // Call general visit so subtypes get visited by their particular visitor
}
- public virtual RESeq! VisitRESeq(RESeq! reSeq)
- {
+ public virtual RESeq VisitRESeq(RESeq reSeq) {
+ Contract.Requires(reSeq != null);
+ Contract.Ensures(Contract.Result<RESeq>() != null);
for (int i = 0, n = reSeq.Length; i < n; i++)
- reSeq[i] = (RE) this.VisitRE( (!)reSeq[i]);
+ reSeq[i] = (RE)this.VisitRE(cce.NonNull(reSeq[i]));
return reSeq;
}
- public virtual ReturnCmd! VisitReturnCmd(ReturnCmd! node)
- {
- return (ReturnCmd) this.VisitTransferCmd(node);
+ public virtual ReturnCmd VisitReturnCmd(ReturnCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<ReturnCmd>() != null);
+ return (ReturnCmd)this.VisitTransferCmd(node);
}
- public virtual ReturnExprCmd! VisitReturnExprCmd(ReturnExprCmd! node)
- {
+ public virtual ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<ReturnExprCmd>() != null);
node.Expr = this.VisitExpr(node.Expr);
return node;
}
- public virtual Sequential! VisitSequential(Sequential! node)
- {
- node.first = (RE) this.VisitRE(node.first);
- node.second = (RE) this.VisitRE(node.second);
+ public virtual Sequential VisitSequential(Sequential node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Sequential>() != null);
+ node.first = (RE)this.VisitRE(node.first);
+ node.second = (RE)this.VisitRE(node.second);
return node;
}
- public virtual AssignLhs! VisitSimpleAssignLhs(SimpleAssignLhs! node)
- {
+ public virtual AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<AssignLhs>() != null);
node.AssignedVariable =
- (IdentifierExpr) this.VisitIdentifierExpr(node.AssignedVariable);
+ (IdentifierExpr)this.VisitIdentifierExpr(node.AssignedVariable);
return node;
}
- public virtual Cmd! VisitStateCmd(StateCmd! node)
- {
+ public virtual Cmd VisitStateCmd(StateCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
node.Locals = this.VisitVariableSeq(node.Locals);
node.Cmds = this.VisitCmdSeq(node.Cmds);
return node;
}
- public virtual TransferCmd! VisitTransferCmd(TransferCmd! node)
- {
+ public virtual TransferCmd VisitTransferCmd(TransferCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<TransferCmd>() != null);
return node;
}
- public virtual Trigger! VisitTrigger(Trigger! node)
- {
+ public virtual Trigger VisitTrigger(Trigger node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Trigger>() != null);
Trigger origNext = node.Next;
if (origNext != null) {
Trigger newNext = this.VisitTrigger(origNext);
@@ -436,65 +506,77 @@ namespace Microsoft.Boogie return node;
}
// called by default for all nullary type constructors and type variables
- public virtual Type! VisitType(Type! node)
- {
+ public virtual Type VisitType(Type node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
return node;
}
- public virtual TypedIdent! VisitTypedIdent(TypedIdent! node)
- {
+ public virtual TypedIdent VisitTypedIdent(TypedIdent node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<TypedIdent>() != null);
node.Type = (Type)this.Visit(node.Type);
return node;
}
- public virtual Declaration! VisitTypeCtorDecl(TypeCtorDecl! node)
- {
+ public virtual Declaration VisitTypeCtorDecl(TypeCtorDecl node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Declaration>() != null);
return this.VisitDeclaration(node);
}
- public virtual Type! VisitTypeSynonymAnnotation(TypeSynonymAnnotation! node)
- {
- node.ExpandedType = (Type!)this.Visit(node.ExpandedType);
+ public virtual Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ node.ExpandedType = cce.NonNull((Type/*!*/)this.Visit(node.ExpandedType));
for (int i = 0; i < node.Arguments.Length; ++i)
- node.Arguments[i] = (Type!)this.Visit(node.Arguments[i]);
+ node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i]));
return node;
}
- public virtual Declaration! VisitTypeSynonymDecl(TypeSynonymDecl! node)
- {
+ public virtual Declaration VisitTypeSynonymDecl(TypeSynonymDecl node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Declaration>() != null);
return this.VisitDeclaration(node);
}
- public virtual Type! VisitTypeVariable(TypeVariable! node)
- {
+ public virtual Type VisitTypeVariable(TypeVariable node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
return this.VisitType(node);
}
- public virtual Type! VisitTypeProxy(TypeProxy! node)
- {
+ public virtual Type VisitTypeProxy(TypeProxy node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
// 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);
+ return cce.NonNull((Type/*!*/)this.Visit(node.ProxyFor));
return this.VisitType(node);
}
- public virtual Type! VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier! node)
- {
+ public virtual Type VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
return this.VisitType(node);
}
- public virtual Variable! VisitVariable(Variable! node)
- {
+ public virtual Variable VisitVariable(Variable node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Variable>() != null);
node.TypedIdent = this.VisitTypedIdent(node.TypedIdent);
return node;
}
- public virtual VariableSeq! VisitVariableSeq(VariableSeq! variableSeq)
- {
+ public virtual VariableSeq VisitVariableSeq(VariableSeq variableSeq) {
+ Contract.Requires(variableSeq != null);
+ Contract.Ensures(Contract.Result<VariableSeq>() != null);
for (int i = 0, n = variableSeq.Length; i < n; i++)
- variableSeq[i] = this.VisitVariable( (!)variableSeq[i]);
+ variableSeq[i] = this.VisitVariable(cce.NonNull(variableSeq[i]));
return variableSeq;
- }
- public virtual Cmd! VisitAssertEnsuresCmd(AssertEnsuresCmd! node)
- {
+ }
+ public virtual Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
node.Ensures = this.VisitEnsures(node.Ensures);
node.Expr = this.VisitExpr(node.Expr);
return node;
- }
- public virtual Cmd! VisitAssertRequiresCmd(AssertRequiresCmd! node)
- {
+ }
+ public virtual Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<Cmd>() != null);
node.Requires = this.VisitRequires(node.Requires);
node.Expr = this.VisitExpr(node.Expr);
return node;
|