diff options
| author |  tabarbe <unknown> | 2010-08-13 00:44:20 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-13 00:44:20 +0000 |
| commit | e81605e480d055843132b41a58451e4ab2cf18b0 (patch) | |
| tree | 6e7cf68fb797da9f29c20f4a8fc853546a36db31 /Source/VCExpr/VCExprASTVisitors.cs | |
| parent | 85ffcd8f1392bf871e585fe8efb60e38bfdb2f72 (diff) | |
Boogie: Committing new source code for VCExpr
Diffstat (limited to 'Source/VCExpr/VCExprASTVisitors.cs')
| -rw-r--r-- | Source/VCExpr/VCExprASTVisitors.cs | 1546 |
1 files changed, 984 insertions, 562 deletions
diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index c9d56962..4a13cbb5 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -8,51 +8,223 @@ using System.Text; using System.IO;
using System.Collections;
using System.Collections.Generic;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
// Some visitor skeletons for the VCExpression AST
-namespace Microsoft.Boogie.VCExprAST
-{
+namespace Microsoft.Boogie.VCExprAST {
using Microsoft.Boogie;
- public interface IVCExprVisitor<Result, Arg> {
- Result Visit(VCExprLiteral! node, Arg arg);
- Result Visit(VCExprNAry! node, Arg arg);
- Result Visit(VCExprVar! node, Arg arg);
- Result Visit(VCExprQuantifier! node, Arg arg);
- Result Visit(VCExprLet! node, Arg arg);
+ [ContractClass(typeof(IVCExprVisitorContracts<,>))]
+ public interface IVCExprVisitor<Result,Arg> {
+ Result Visit(VCExprLiteral/*!*/ node, Arg arg);
+ Result Visit(VCExprNAry/*!*/ node, Arg arg);
+ Result Visit(VCExprVar/*!*/ node, Arg arg);
+ Result Visit(VCExprQuantifier/*!*/ node, Arg arg);
+ Result Visit(VCExprLet/*!*/ node, Arg arg);
}
+ [ContractClassFor(typeof(IVCExprVisitor<,>))]
+ public abstract class IVCExprVisitorContracts<Result,Arg> : IVCExprVisitor<Result,Arg> {
+ #region IVCExprVisitor Members
+ public Result Visit(VCExprLiteral node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result Visit(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result Visit(VCExprVar node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result Visit(VCExprQuantifier node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result Visit(VCExprLet node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ #endregion
+ }
+ [ContractClass(typeof(IVCExprOpVisitorContracts<,>))]
public interface IVCExprOpVisitor<Result, Arg> {
- Result VisitNotOp (VCExprNAry! node, Arg arg);
- Result VisitEqOp (VCExprNAry! node, Arg arg);
- Result VisitNeqOp (VCExprNAry! node, Arg arg);
- Result VisitAndOp (VCExprNAry! node, Arg arg);
- Result VisitOrOp (VCExprNAry! node, Arg arg);
- Result VisitImpliesOp (VCExprNAry! node, Arg arg);
- Result VisitDistinctOp (VCExprNAry! node, Arg arg);
- Result VisitLabelOp (VCExprNAry! node, Arg arg);
- Result VisitSelectOp (VCExprNAry! node, Arg arg);
- Result VisitStoreOp (VCExprNAry! node, Arg arg);
- Result VisitBvOp (VCExprNAry! node, Arg arg);
- Result VisitBvExtractOp(VCExprNAry! node, Arg arg);
- Result VisitBvConcatOp (VCExprNAry! node, Arg arg);
- Result VisitAddOp (VCExprNAry! node, Arg arg);
- Result VisitSubOp (VCExprNAry! node, Arg arg);
- Result VisitMulOp (VCExprNAry! node, Arg arg);
- Result VisitDivOp (VCExprNAry! node, Arg arg);
- Result VisitModOp (VCExprNAry! node, Arg arg);
- Result VisitLtOp (VCExprNAry! node, Arg arg);
- Result VisitLeOp (VCExprNAry! node, Arg arg);
- Result VisitGtOp (VCExprNAry! node, Arg arg);
- Result VisitGeOp (VCExprNAry! node, Arg arg);
- Result VisitSubtypeOp (VCExprNAry! node, Arg arg);
- Result VisitSubtype3Op (VCExprNAry! node, Arg arg);
- Result VisitBoogieFunctionOp (VCExprNAry! node, Arg arg);
- Result VisitIfThenElseOp (VCExprNAry! node, Arg arg);
- Result VisitCustomOp (VCExprNAry! node, Arg arg);
+ Result VisitNotOp(VCExprNAry node, Arg arg);
+ Result VisitEqOp(VCExprNAry node, Arg arg);
+ Result VisitNeqOp(VCExprNAry node, Arg arg);
+ Result VisitAndOp(VCExprNAry node, Arg arg);
+ Result VisitOrOp(VCExprNAry node, Arg arg);
+ Result VisitImpliesOp(VCExprNAry node, Arg arg);
+ Result VisitDistinctOp(VCExprNAry node, Arg arg);
+ Result VisitLabelOp(VCExprNAry node, Arg arg);
+ Result VisitSelectOp(VCExprNAry node, Arg arg);
+ Result VisitStoreOp(VCExprNAry node, Arg arg);
+ Result VisitBvOp(VCExprNAry node, Arg arg);
+ Result VisitBvExtractOp(VCExprNAry node, Arg arg);
+ Result VisitBvConcatOp(VCExprNAry node, Arg arg);
+ Result VisitAddOp(VCExprNAry node, Arg arg);
+ Result VisitSubOp(VCExprNAry node, Arg arg);
+ Result VisitMulOp(VCExprNAry node, Arg arg);
+ Result VisitDivOp(VCExprNAry node, Arg arg);
+ Result VisitModOp(VCExprNAry node, Arg arg);
+ Result VisitLtOp(VCExprNAry node, Arg arg);
+ Result VisitLeOp(VCExprNAry node, Arg arg);
+ Result VisitGtOp(VCExprNAry node, Arg arg);
+ Result VisitGeOp(VCExprNAry node, Arg arg);
+ Result VisitSubtypeOp(VCExprNAry node, Arg arg);
+ Result VisitSubtype3Op(VCExprNAry node, Arg arg);
+ Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg);
+ Result VisitIfThenElseOp(VCExprNAry node, Arg arg);
+ Result VisitCustomOp (VCExprNAry node, Arg arg);
+ }
+ [ContractClassFor(typeof(IVCExprOpVisitor<,>))]
+ public abstract class IVCExprOpVisitorContracts<Result, Arg>:IVCExprOpVisitor<Result,Arg> {
+ #region IVCExprOpVisitor<Result,Arg> Members
+
+ public Result VisitNotOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitEqOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitNeqOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitAndOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitOrOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitImpliesOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitDistinctOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitLabelOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitSelectOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitStoreOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitBvOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitBvExtractOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitBvConcatOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitAddOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitSubOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitMulOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitDivOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitModOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitLtOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitLeOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitGtOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitGeOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitSubtypeOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitSubtype3Op(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitIfThenElseOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitCustomOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ #endregion
}
//////////////////////////////////////////////////////////////////////////////
@@ -64,29 +236,35 @@ namespace Microsoft.Boogie.VCExprAST // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary
// to avoid stack overflows
+
+ [ContractClass(typeof(TraversingVCExprVisitorContracts<,>))]
public abstract class TraversingVCExprVisitor<Result, Arg>
: IVCExprVisitor<Result, Arg> {
- protected abstract Result StandardResult(VCExpr! node, Arg arg);
+ protected abstract Result StandardResult(VCExpr/*!*/ node, Arg arg);
- public Result Traverse(VCExpr! node, Arg arg) {
+ public Result Traverse(VCExpr node, Arg arg) {
+ Contract.Requires(node != null);
return node.Accept(this, arg);
}
- public virtual Result Visit(VCExprLiteral! node, Arg arg) {
+ public virtual Result Visit(VCExprLiteral node, Arg arg) {
+ Contract.Requires(node != null);
return StandardResult(node, arg);
}
- public virtual Result Visit(VCExprNAry! node, Arg arg) {
+ public virtual Result Visit(VCExprNAry node, Arg arg){
+Contract.Requires(node != null);
Result res = StandardResult(node, arg);
if (node.TypeParamArity == 0) {
- VCExprOp! op = node.Op;
+ Contract.Assert(node.Op != null);
+ VCExprOp op = node.Op;
IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
enumerator.MoveNext(); // skip the node itself
while (enumerator.MoveNext()) {
- VCExpr! expr = (VCExpr!)enumerator.Current;
+ VCExpr/*!*/ expr = cce.NonNull((VCExpr/*!*/)enumerator.Current);
VCExprNAry naryExpr = expr as VCExprNAry;
if (naryExpr == null || !naryExpr.Op.Equals(op)) {
expr.Accept(this, arg);
@@ -95,34 +273,45 @@ namespace Microsoft.Boogie.VCExprAST }
}
} else {
- foreach (VCExpr! e in node)
- e.Accept(this, arg);
+ foreach (VCExpr e in node){Contract.Assert(e != null);
+ e.Accept(this, arg);}
}
return res;
}
- public virtual Result Visit(VCExprVar! node, Arg arg) {
+ public virtual Result Visit(VCExprVar node, Arg arg) {
+ Contract.Requires(node != null);
return StandardResult(node, arg);
}
- public virtual Result Visit(VCExprQuantifier! node, Arg arg) {
+ public virtual Result Visit(VCExprQuantifier node, Arg arg){
+Contract.Requires(node != null);
Result res = StandardResult(node, arg);
- foreach (VCTrigger! trigger in node.Triggers)
- foreach (VCExpr! expr in trigger.Exprs)
- expr.Accept(this, arg);
+ foreach (VCTrigger/*!*/ trigger in node.Triggers){Contract.Assert(trigger != null);
+ foreach (VCExpr/*!*/ expr in trigger.Exprs) {
+ Contract.Assert(expr != null);
+ expr.Accept(this, arg);}}
node.Body.Accept(this, arg);
return res;
}
- public virtual Result Visit(VCExprLet! node, Arg arg) {
+ public virtual Result Visit(VCExprLet node, Arg arg){
+Contract.Requires(node != null);
Result res = StandardResult(node, arg);
// visit the bound expressions first
- foreach (VCExprLetBinding! binding in node)
- binding.E.Accept(this, arg);
+ foreach (VCExprLetBinding/*!*/ binding in node) {
+ Contract.Assert(binding != null);
+ binding.E.Accept(this, arg);}
node.Body.Accept(this, arg);
return res;
}
}
-
+ [ContractClassFor(typeof(TraversingVCExprVisitor<,>))]
+ public abstract class TraversingVCExprVisitorContracts<Result, Arg> : TraversingVCExprVisitor<Result, Arg> {
+ protected override Result StandardResult(VCExpr node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+ }
//////////////////////////////////////////////////////////////////////////////
// Class to iterate over the nodes of a tree of VCExprNAry. This is
// used to avoid handling such VCExpr recursively, which can easily
@@ -130,13 +319,19 @@ namespace Microsoft.Boogie.VCExprAST public class VCExprNAryEnumerator : IEnumerator {
- private readonly VCExprNAry! CompleteExpr;
+ private readonly VCExprNAry/*!*/ CompleteExpr;
private VCExpr CurrentExpr = null;
- private readonly Stack<VCExpr!>! ExprTodo = new Stack<VCExpr!> ();
-
- public VCExprNAryEnumerator(VCExprNAry! completeExpr) {
+ private readonly Stack<VCExpr/*!*/>/*!*/ ExprTodo = new Stack<VCExpr/*!*/>();
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(CompleteExpr != null);
+ Contract.Invariant(cce.NonNullElements(ExprTodo));
+ }
+
+ public VCExprNAryEnumerator(VCExprNAry completeExpr){
+Contract.Requires(completeExpr != null);
this.CompleteExpr = completeExpr;
- Stack<VCExpr!>! exprTodo = new Stack<VCExpr!> ();
+ Stack<VCExpr/*!*/>/*!*/ exprTodo = new Stack<VCExpr/*!*/>();
exprTodo.Push(completeExpr);
ExprTodo = exprTodo;
}
@@ -144,10 +339,11 @@ namespace Microsoft.Boogie.VCExprAST // Method using which a subclass can decide whether the
// subexpressions of an expression should be enumerated as well
// The default is to enumerate all nodes
- protected virtual bool Descend(VCExprNAry! expr) {
+ protected virtual bool Descend(VCExprNAry expr) {
+ Contract.Requires(expr != null);
return true;
}
-
+
////////////////////////////////////////////////////////////////////////////
public bool MoveNext() {
@@ -160,14 +356,15 @@ namespace Microsoft.Boogie.VCExprAST for (int i = currentNAry.Arity - 1; i >= 0; --i)
ExprTodo.Push(currentNAry[i]);
}
-
+
return true;
}
public object Current {
get {
- return (!)CurrentExpr;
- } }
+ return cce.NonNull(CurrentExpr);
+ }
+ }
public void Reset() {
ExprTodo.Clear();
@@ -176,19 +373,27 @@ namespace Microsoft.Boogie.VCExprAST }
}
-
+
//////////////////////////////////////////////////////////////////////////////
public class VCExprNAryUniformOpEnumerator : VCExprNAryEnumerator {
- private readonly VCExprOp! Op;
- public VCExprNAryUniformOpEnumerator(VCExprNAry! completeExpr) {
- base(completeExpr);
+ private readonly VCExprOp/*!*/ Op;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Op != null);
+ }
+
+ public VCExprNAryUniformOpEnumerator(VCExprNAry completeExpr)
+ : base(completeExpr) {
+ Contract.Requires(completeExpr != null);
+
this.Op = completeExpr.Op;
}
- protected override bool Descend(VCExprNAry! expr) {
+ protected override bool Descend(VCExprNAry expr) {
+ Contract.Requires(expr != null);
return expr.Op.Equals(Op) &&
- // we never skip nodes with type parameters
- // (those are too interesting ...)
+ // we never skip nodes with type parameters
+ // (those are too interesting ...)
expr.TypeParamArity == 0;
}
}
@@ -200,19 +405,33 @@ namespace Microsoft.Boogie.VCExprAST : TraversingVCExprVisitor<Result, Arg> {
// Maps with all variables bound above a certain location in the VCExpression.
// The value of the map tells how often a particular symbol was bound
- private readonly IDictionary<VCExprVar!, int>! BoundTermVarsDict =
- new Dictionary<VCExprVar!, int> ();
- private readonly IDictionary<TypeVariable!, int>! BoundTypeVarsDict =
- new Dictionary<TypeVariable!, int> ();
-
- protected ICollection<VCExprVar!>! BoundTermVars { get {
- return BoundTermVarsDict.Keys;
- } }
- protected ICollection<TypeVariable!>! BoundTypeVars { get {
- return BoundTypeVarsDict.Keys;
- } }
-
- private void AddBoundVar<T>(IDictionary<T!, int>! dict, T! sym) {
+ private readonly IDictionary<VCExprVar/*!*/, int>/*!*/ BoundTermVarsDict =
+ new Dictionary<VCExprVar/*!*/, int>();
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(BoundTermVarsDict));
+ Contract.Invariant(cce.NonNullElements(BoundTypeVarsDict));
+ }
+
+ private readonly IDictionary<TypeVariable/*!*/, int>/*!*/ BoundTypeVarsDict =
+ new Dictionary<TypeVariable/*!*/, int>();
+
+ protected ICollection<VCExprVar/*!*/>/*!*/ BoundTermVars {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<VCExprVar>>()));
+ return BoundTermVarsDict.Keys;
+ }
+ }
+ protected ICollection<TypeVariable/*!*/>/*!*/ BoundTypeVars {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<TypeVariable>>()));
+ return BoundTypeVarsDict.Keys;
+ }
+ }
+
+ private void AddBoundVar<T>(IDictionary<T, int> dict, T sym) {
+ Contract.Requires(sym != null);
+ Contract.Requires(cce.NonNullElements(dict));
int n;
if (dict.TryGetValue(sym, out n))
dict[sym] = n + 1;
@@ -220,47 +439,54 @@ namespace Microsoft.Boogie.VCExprAST dict[sym] = 1;
}
- private void RemoveBoundVar<T>(IDictionary<T!, int>! dict, T! sym) {
+ private void RemoveBoundVar<T>(IDictionary<T/*!*/, int/*!*/>/*!*/ dict, T sym) {
+ Contract.Requires(sym != null);
+ Contract.Requires(cce.NonNullElements(dict));
int n;
bool b = dict.TryGetValue(sym, out n);
- assert b && n > 0;
+ Contract.Assert(b && n > 0);
if (n == 1)
dict.Remove(sym);
else
dict[sym] = n - 1;
}
- public override Result Visit(VCExprQuantifier! node, Arg arg) {
+ public override Result Visit(VCExprQuantifier node, Arg arg){
+Contract.Requires(node != null);
// we temporarily add bound (term and type) variables to the
// corresponding lists
- foreach (VCExprVar! v in node.BoundVars)
- AddBoundVar<VCExprVar>(BoundTermVarsDict, v);
- foreach (TypeVariable! v in node.TypeParameters)
- AddBoundVar<TypeVariable>(BoundTypeVarsDict, v);
+ foreach (VCExprVar/*!*/ v in node.BoundVars){Contract.Assert(v != null);
+ AddBoundVar<VCExprVar>(BoundTermVarsDict, v);}
+ foreach (TypeVariable/*!*/ v in node.TypeParameters){Contract.Assert(v != null);
+ AddBoundVar<TypeVariable>(BoundTypeVarsDict, v);}
Result res;
try {
res = VisitAfterBinding(node, arg);
} finally {
- foreach (VCExprVar! v in node.BoundVars)
- RemoveBoundVar<VCExprVar>(BoundTermVarsDict, v);
- foreach (TypeVariable! v in node.TypeParameters)
- RemoveBoundVar<TypeVariable>(BoundTypeVarsDict, v);
+ foreach (VCExprVar/*!*/ v in node.BoundVars){Contract.Assert(v != null);
+ RemoveBoundVar<VCExprVar>(BoundTermVarsDict, v);}
+ foreach (TypeVariable/*!*/ v in node.TypeParameters) {
+ Contract.Assert(v != null);
+ RemoveBoundVar<TypeVariable>(BoundTypeVarsDict, v);}
}
return res;
}
- public override Result Visit(VCExprLet! node, Arg arg) {
+ public override Result Visit(VCExprLet node, Arg arg){
+Contract.Requires(node != null);
// we temporarily add bound term variables to the
// corresponding lists
- foreach (VCExprVar! v in node.BoundVars)
- AddBoundVar<VCExprVar>(BoundTermVarsDict, v);
+ foreach (VCExprVar/*!*/ v in node.BoundVars){Contract.Assert(v != null);
+ AddBoundVar<VCExprVar>(BoundTermVarsDict, v);}
Result res;
try {
res = VisitAfterBinding(node, arg);
} finally {
- foreach (VCExprVar! v in node.BoundVars)
+ foreach (VCExprVar/*!*/ v in node.BoundVars) {
+ Contract.Assert(v != null);
RemoveBoundVar<VCExprVar>(BoundTermVarsDict, v);
+ }
}
return res;
}
@@ -271,11 +497,13 @@ namespace Microsoft.Boogie.VCExprAST // (when overriding the normal visit-methods, the node will be visited
// before the binding happens)
- protected virtual Result VisitAfterBinding(VCExprQuantifier! node, Arg arg) {
+ protected virtual Result VisitAfterBinding(VCExprQuantifier node, Arg arg) {
+ Contract.Requires(node != null);
return base.Visit(node, arg);
}
- protected virtual Result VisitAfterBinding(VCExprLet! node, Arg arg) {
+ protected virtual Result VisitAfterBinding(VCExprLet node, Arg arg) {
+ Contract.Requires(node != null);
return base.Visit(node, arg);
}
}
@@ -285,174 +513,231 @@ namespace Microsoft.Boogie.VCExprAST // As the visitor is not used anywhere for the time being, it maybe should
// be removed
+ [ContractClass(typeof(CollectingVCExprVisitorContracts<,>))]
public abstract class CollectingVCExprVisitor<Result, Arg>
: IVCExprVisitor<Result, Arg> {
- protected abstract Result CombineResults(List<Result>! results, Arg arg);
+ protected abstract Result CombineResults(List<Result>/*!*/ results, Arg arg);
- public Result Collect(VCExpr! node, Arg arg) {
+ public Result Collect(VCExpr node, Arg arg) {
+ Contract.Requires(node != null);
return node.Accept(this, arg);
}
- public virtual Result Visit(VCExprLiteral! node, Arg arg) {
- return CombineResults(new List<Result> (), arg);
+ public virtual Result Visit(VCExprLiteral node, Arg arg) {
+ Contract.Requires(node != null);
+ return CombineResults(new List<Result>(), arg);
}
- public virtual Result Visit(VCExprNAry! node, Arg arg) {
- List<Result>! results = new List<Result> ();
- foreach (VCExpr! subnode in node)
- results.Add(subnode.Accept(this, arg));
+ public virtual Result Visit(VCExprNAry node, Arg arg){
+Contract.Requires(node != null);
+ List<Result>/*!*/ results = new List<Result> ();
+ foreach (VCExpr/*!*/ subnode in node) {
+ Contract.Assert(subnode != null);
+ results.Add(subnode.Accept(this, arg));}
return CombineResults(results, arg);
}
- public virtual Result Visit(VCExprVar! node, Arg arg) {
- return CombineResults(new List<Result> (), arg);
+ public virtual Result Visit(VCExprVar node, Arg arg) {
+ Contract.Requires(node != null);
+ return CombineResults(new List<Result>(), arg);
}
- public virtual Result Visit(VCExprQuantifier! node, Arg arg) {
- List<Result>! result = new List<Result> ();
+ public virtual Result Visit(VCExprQuantifier node, Arg arg){
+Contract.Requires(node != null);
+ List<Result>/*!*/ result = new List<Result> ();
result.Add(node.Body.Accept(this, arg));
- foreach (VCTrigger! trigger in node.Triggers)
- foreach (VCExpr! expr in trigger.Exprs)
- result.Add(expr.Accept(this, arg));
+ foreach (VCTrigger/*!*/ trigger in node.Triggers){Contract.Assert(trigger != null);
+ foreach (VCExpr/*!*/ expr in trigger.Exprs) {
+ Contract.Assert(expr != null);
+ result.Add(expr.Accept(this, arg));}}
return CombineResults(result, arg);
}
- public virtual Result Visit(VCExprLet! node, Arg arg) {
- List<Result>! results = new List<Result> ();
+ public virtual Result Visit(VCExprLet node, Arg arg){
+Contract.Requires(node != null);
+ List<Result>/*!*/ results = new List<Result> ();
// visit the bound expressions first
- foreach (VCExprLetBinding! binding in node)
+ foreach (VCExprLetBinding/*!*/ binding in node) {
+ Contract.Assert(binding != null);
results.Add(binding.E.Accept(this, arg));
+ }
results.Add(node.Body.Accept(this, arg));
return CombineResults(results, arg);
}
}
-
+ [ContractClassFor(typeof(CollectingVCExprVisitor<,>))]
+ public abstract class CollectingVCExprVisitorContracts<Result, Arg> : CollectingVCExprVisitor<Result, Arg> {
+ protected override Result CombineResults(List<Result> results, Arg arg) {
+ Contract.Requires(results != null);
+ throw new NotImplementedException();
+ }
+ }
////////////////////////////////////////////////////////////////////////////
- public class SizeComputingVisitor : TraversingVCExprVisitor<bool, bool> {
+ public class SizeComputingVisitor : TraversingVCExprVisitor<bool, bool> {
- private int Size = 0;
+ private int Size = 0;
- public static int ComputeSize(VCExpr! expr) {
- SizeComputingVisitor! visitor = new SizeComputingVisitor();
- visitor.Traverse(expr, true);
- return visitor.Size;
- }
-
- protected override bool StandardResult(VCExpr! node, bool arg) {
- Size = Size + 1;
- return true;
+ public static int ComputeSize(VCExpr expr) {
+ Contract.Requires(expr != null);
+ SizeComputingVisitor/*!*/ visitor = new SizeComputingVisitor();
+ visitor.Traverse(expr, true);
+ return visitor.Size;
+ }
+
+ protected override bool StandardResult(VCExpr node, bool arg) {
+ Contract.Requires(node != null);
+ Size = Size + 1;
+ return true;
+ }
}
- }
- ////////////////////////////////////////////////////////////////////////////
+ ////////////////////////////////////////////////////////////////////////////
- // Collect all free term and type variables in a VCExpr. Type variables
- // can occur free either in the types of bound variables, or in the type
- // parameters of VCExprNAry.
+ // Collect all free term and type variables in a VCExpr. Type variables
+ // can occur free either in the types of bound variables, or in the type
+ // parameters of VCExprNAry.
+
+ // the result and argument (of type bool) are not used currently
+ public class FreeVariableCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
+ public readonly Dictionary<VCExprVar/*!*/, object>/*!*/ FreeTermVars = new Dictionary<VCExprVar/*!*/, object>();
+ public readonly List<TypeVariable/*!*/>/*!*/ FreeTypeVars = new List<TypeVariable/*!*/>();
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(FreeTermVars));
+ Contract.Invariant(cce.NonNullElements(FreeTypeVars));
+ }
- // the result and argument (of type bool) are not used currently
- public class FreeVariableCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
- public readonly Dictionary<VCExprVar!,object>! FreeTermVars = new Dictionary<VCExprVar!,object> ();
- public readonly List<TypeVariable!>! FreeTypeVars = new List<TypeVariable!> ();
- // not used
- protected override bool StandardResult(VCExpr! node, bool arg) {
- return true;
- }
+ // not used
+ protected override bool StandardResult(VCExpr node, bool arg) {
+ Contract.Requires(node != null);
+ return true;
+ }
- public static Dictionary<VCExprVar!,object>! FreeTermVariables(VCExpr! node) {
- FreeVariableCollector collector = new FreeVariableCollector ();
- collector.Traverse(node, true);
- return collector.FreeTermVars;
- }
+ public static Dictionary<VCExprVar/*!*/, object/*!*/>/*!*/ FreeTermVariables(VCExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(cce.NonNullElements(Contract.Result<Dictionary<VCExprVar, object>>()));
+ FreeVariableCollector collector = new FreeVariableCollector();
+ collector.Traverse(node, true);
+ return collector.FreeTermVars;
+ }
- public static List<TypeVariable!>! FreeTypeVariables(VCExpr! node) {
- FreeVariableCollector collector = new FreeVariableCollector ();
- collector.Traverse(node, true);
- return collector.FreeTypeVars;
- }
+ public static List<TypeVariable/*!*/>/*!*/ FreeTypeVariables(VCExpr node) {
+ Contract.Requires(node != null);
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));
+ FreeVariableCollector collector = new FreeVariableCollector();
+ collector.Traverse(node, true);
+ return collector.FreeTypeVars;
+ }
- public void Reset() {
- FreeTermVars.Clear();
- FreeTypeVars.Clear();
- }
+ public void Reset() {
+ FreeTermVars.Clear();
+ FreeTypeVars.Clear();
+ }
- public void Collect(VCExpr! node) {
- Traverse(node, true);
- }
+ public void Collect(VCExpr node) {
+ Contract.Requires(node != null);
+ Traverse(node, true);
+ }
- public void Collect(Type! type) {
- AddTypeVariables(type.FreeVariables.ToList());
- }
+ public void Collect(Type type) {
+ Contract.Requires(type != null);
+ AddTypeVariables(type.FreeVariables.ToList());
+ }
- /////////////////////////////////////////////////////////////////////////
+ /////////////////////////////////////////////////////////////////////////
- private void CollectTypeVariables(IEnumerable<VCExprVar!>! boundVars) {
- foreach (VCExprVar! var in boundVars)
+ private void CollectTypeVariables(IEnumerable<VCExprVar/*!*/>/*!*/ boundVars){Contract.Requires(cce.NonNullElements(boundVars));
+ foreach (VCExprVar/*!*/ var in boundVars) {
+ Contract.Assert(var != null);
Collect(var.Type);
+ }
}
- private void AddTypeVariables(IEnumerable<TypeVariable!>! typeVars) {
- foreach (TypeVariable! tvar in typeVars)
- if (!BoundTypeVars.Contains(tvar) && !FreeTypeVars.Contains(tvar))
- FreeTypeVars.Add(tvar);
- }
+ private void AddTypeVariables(IEnumerable<TypeVariable/*!*/>/*!*/ typeVars) {
+ Contract.Requires(cce.NonNullElements(typeVars));
+ foreach (TypeVariable/*!*/ tvar in typeVars) {
+ Contract.Assert(tvar != null);
+ if (!BoundTypeVars.Contains(tvar) && !FreeTypeVars.Contains(tvar))
+ FreeTypeVars.Add(tvar);
+ }
+ }
- public override bool Visit(VCExprVar! node, bool arg) {
- if (!BoundTermVars.Contains(node) && !FreeTermVars.ContainsKey(node)) {
- FreeTermVars.Add(node, null);
- Collect(node.Type);
+ public override bool Visit(VCExprVar node, bool arg) {
+ Contract.Requires(node != null);
+ if (!BoundTermVars.Contains(node) && !FreeTermVars.ContainsKey(node)) {
+ FreeTermVars.Add(node, null);
+ Collect(node.Type);
+ }
+ return true;
}
- return true;
- }
- public override bool Visit(VCExprNAry! node, bool arg) {
- foreach (Type! t in node.TypeArguments)
- Collect(t);
- return base.Visit(node, arg);
- }
+ public override bool Visit(VCExprNAry node, bool arg) {
+ Contract.Requires(node != null);
+ foreach (Type/*!*/ t in node.TypeArguments) {
+ Contract.Assert(t != null);
+ Collect(t);
+ }
+ return base.Visit(node, arg);
+ }
- protected override bool VisitAfterBinding(VCExprQuantifier! node, bool arg) {
- CollectTypeVariables(node.BoundVars);
- return base.VisitAfterBinding(node, arg);
- }
+ protected override bool VisitAfterBinding(VCExprQuantifier node, bool arg) {
+ Contract.Requires(node != null);
+ CollectTypeVariables(node.BoundVars);
+ return base.VisitAfterBinding(node, arg);
+ }
- protected override bool VisitAfterBinding(VCExprLet! node, bool arg) {
- CollectTypeVariables(node.BoundVars);
- return base.VisitAfterBinding(node, arg);
+ protected override bool VisitAfterBinding(VCExprLet node, bool arg) {
+ Contract.Requires(node != null);
+ CollectTypeVariables(node.BoundVars);
+ return base.VisitAfterBinding(node, arg);
+ }
}
- }
-
- ////////////////////////////////////////////////////////////////////////////
- // Framework for mutating VCExprs
- // The Visit implementations in the following visitor work
- // recursively, apart from the implementation for VCExprNAry that
- // uses its own stack when applied to nested nodes with the same
- // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary
- // to avoid stack overflows (like in TraversingVCExprVisitor)
+ ////////////////////////////////////////////////////////////////////////////
+ // Framework for mutating VCExprs
+
+ // The Visit implementations in the following visitor work
+ // recursively, apart from the implementation for VCExprNAry that
+ // uses its own stack when applied to nested nodes with the same
+ // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary
+ // to avoid stack overflows (like in TraversingVCExprVisitor)
+
+ public abstract class MutatingVCExprVisitor<Arg>
+ : IVCExprVisitor<VCExpr/*!*/, Arg> {
+ protected readonly VCExpressionGenerator/*!*/ Gen;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Gen != null);
+ }
- public abstract class MutatingVCExprVisitor<Arg>
- : IVCExprVisitor<VCExpr!, Arg> {
- protected readonly VCExpressionGenerator! Gen;
- public MutatingVCExprVisitor(VCExpressionGenerator! gen) {
- this.Gen = gen;
- }
+ public MutatingVCExprVisitor(VCExpressionGenerator gen) {
+ Contract.Requires(gen != null);
+ this.Gen = gen;
+ }
- public VCExpr! Mutate(VCExpr! expr, Arg arg) {
- return expr.Accept(this, arg);
- }
+ public VCExpr Mutate(VCExpr expr, Arg arg) {
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return expr.Accept(this, arg);
+ }
- public List<VCExpr!>! MutateSeq(IEnumerable<VCExpr!>! exprs, Arg arg) {
- List<VCExpr!>! res = new List<VCExpr!> ();
- foreach (VCExpr! expr in exprs)
+ public List<VCExpr/*!*/>/*!*/ MutateSeq(IEnumerable<VCExpr/*!*/>/*!*/ exprs, Arg arg){
+Contract.Requires(cce.NonNullElements(exprs));
+Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
+ List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/> ();
+ foreach (VCExpr/*!*/ expr in exprs) {
+ Contract.Assert(expr != null);
res.Add(expr.Accept(this, arg));
+ }
return res;
}
- private List<VCExpr!>! MutateList(List<VCExpr!>! exprs, Arg arg) {
+ private List<VCExpr/*!*/>/*!*/ MutateList(List<VCExpr/*!*/>/*!*/ exprs, Arg arg){
+Contract.Requires(cce.NonNullElements(exprs));
+Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExpr>>()));
bool changed = false;
- List<VCExpr!>! res = new List<VCExpr!> ();
- foreach (VCExpr! expr in exprs) {
- VCExpr! newExpr = expr.Accept(this, arg);
+ List<VCExpr/*!*/>/*!*/ res = new List<VCExpr/*!*/> ();
+ foreach (VCExpr/*!*/ expr in exprs) {Contract.Assert(expr != null);
+ VCExpr/*!*/ newExpr = expr.Accept(this, arg);
if (!Object.ReferenceEquals(expr, newExpr))
changed = true;
res.Add(newExpr);
@@ -462,54 +747,69 @@ namespace Microsoft.Boogie.VCExprAST return res;
}
- public virtual VCExpr! Visit(VCExprLiteral! node, Arg arg) {
- return node;
- }
-
- ////////////////////////////////////////////////////////////////////////////
-
- // Special element used to mark the positions in the todo-stack where
- // results have to be popped from the result-stack.
- private static readonly VCExpr! CombineResultsMarker = new VCExprLiteral (Type.Bool);
+ public virtual VCExpr Visit(VCExprLiteral node, Arg arg) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return node;
+ }
- // The todo-stack contains records of the shape
- //
- // arg0
- // arg1
- // arg2
- // ...
- // CombineResultsMarker
- // f(arg0, arg1, arg2, ...) (the original expression)
+ ////////////////////////////////////////////////////////////////////////////
+
+ // Special element used to mark the positions in the todo-stack where
+ // results have to be popped from the result-stack.
+ private static readonly VCExpr/*!*/ CombineResultsMarker = new VCExprLiteral(Type.Bool);
+
+ // The todo-stack contains records of the shape
+ //
+ // arg0
+ // arg1
+ // arg2
+ // ...
+ // CombineResultsMarker
+ // f(arg0, arg1, arg2, ...) (the original expression)
+
+ private readonly Stack<VCExpr/*!*/>/*!*/ NAryExprTodoStack = new Stack<VCExpr/*!*/>();
+ private readonly Stack<VCExpr/*!*/>/*!*/ NAryExprResultStack = new Stack<VCExpr/*!*/>();
+ [ContractInvariantMethod]
+ void ObjectInvarianta() {
+ Contract.Invariant(cce.NonNullElements(NAryExprResultStack));
+ Contract.Invariant(cce.NonNullElements(NAryExprTodoStack));
+ }
- private readonly Stack<VCExpr!>! NAryExprTodoStack = new Stack<VCExpr!> ();
- private readonly Stack<VCExpr!>! NAryExprResultStack = new Stack<VCExpr!> ();
- private void PushTodo(VCExprNAry! exprTodo) {
- NAryExprTodoStack.Push(exprTodo);
- NAryExprTodoStack.Push(CombineResultsMarker);
- for (int i = exprTodo.Arity - 1; i >= 0; --i)
- NAryExprTodoStack.Push(exprTodo[i]);
- }
+ private void PushTodo(VCExprNAry exprTodo) {
+ Contract.Requires(exprTodo != null);
+ NAryExprTodoStack.Push(exprTodo);
+ NAryExprTodoStack.Push(CombineResultsMarker);
+ for (int i = exprTodo.Arity - 1; i >= 0; --i)
+ NAryExprTodoStack.Push(exprTodo[i]);
+ }
- public virtual VCExpr! Visit(VCExprNAry! node, Arg arg) {
- VCExprOp! op = node.Op;
+ public virtual VCExpr Visit(VCExprNAry node, Arg arg){
+Contract.Requires(node != null);
+Contract.Ensures(Contract.Result<VCExpr>() != null);
+ VCExprOp/*!*/ op = node.Op;
+ Contract.Assert(op != null);
int initialStackSize = NAryExprTodoStack.Count;
int initialResultStackSize = NAryExprResultStack.Count;
PushTodo(node);
while (NAryExprTodoStack.Count > initialStackSize) {
- VCExpr! subExpr = NAryExprTodoStack.Pop();
+ VCExpr/*!*/ subExpr = NAryExprTodoStack.Pop();
+ Contract.Assert(subExpr != null);
if (Object.ReferenceEquals(subExpr, CombineResultsMarker)) {
//
// assemble a result
- VCExprNAry! originalExpr = (VCExprNAry)NAryExprTodoStack.Pop();
+ VCExprNAry/*!*/ originalExpr = (VCExprNAry)NAryExprTodoStack.Pop();
+ Contract.Assert(originalExpr != null);
bool changed = false;
- List<VCExpr!>! newSubExprs = new List<VCExpr!> ();
+ List<VCExpr/*!*/>/*!*/ newSubExprs = new List<VCExpr/*!*/> ();
for (int i = op.Arity - 1; i >= 0; --i) {
- VCExpr! nextSubExpr = NAryExprResultStack.Pop();
+ VCExpr/*!*/ nextSubExpr = NAryExprResultStack.Pop();
+ Contract.Assert(nextSubExpr != null);
if (!Object.ReferenceEquals(nextSubExpr, originalExpr[i]))
changed = true;
newSubExprs.Insert(0, nextSubExpr);
@@ -532,35 +832,41 @@ namespace Microsoft.Boogie.VCExprAST }
}
- assert NAryExprTodoStack.Count == initialStackSize &&
- NAryExprResultStack.Count == initialResultStackSize + 1;
+ Contract.Assert(NAryExprTodoStack.Count == initialStackSize && NAryExprResultStack.Count == initialResultStackSize + 1);
return NAryExprResultStack.Pop();
}
- protected virtual VCExpr! UpdateModifiedNode(VCExprNAry! originalNode,
- List<VCExpr!>! newSubExprs,
- // has any of the subexpressions changed?
- bool changed,
- Arg arg) {
- if (changed)
- return Gen.Function(originalNode.Op,
- newSubExprs, originalNode.TypeArguments);
- else
- return originalNode;
- }
+ protected virtual VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, // has any of the subexpressions changed?
+ bool changed,
+ Arg arg) {
+ Contract.Requires(cce.NonNullElements(newSubExprs));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
- ////////////////////////////////////////////////////////////////////////////
+ if (changed)
+ return Gen.Function(originalNode.Op,
+ newSubExprs, originalNode.TypeArguments);
+ else
+ return originalNode;
+ }
- public virtual VCExpr! Visit(VCExprVar! node, Arg arg) {
- return node;
- }
+ ////////////////////////////////////////////////////////////////////////////
+
+ public virtual VCExpr Visit(VCExprVar node, Arg arg) {
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return node;
+ }
- protected List<VCTrigger!>! MutateTriggers(List<VCTrigger!>! triggers, Arg arg) {
- List<VCTrigger!>! newTriggers = new List<VCTrigger!> ();
+ protected List<VCTrigger/*!*/>/*!*/ MutateTriggers(List<VCTrigger/*!*/>/*!*/ triggers, Arg arg){
+Contract.Requires(cce.NonNullElements(triggers));
+Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCTrigger>>()));
+ List<VCTrigger/*!*/>/*!*/ newTriggers = new List<VCTrigger/*!*/> ();
bool changed = false;
- foreach (VCTrigger! trigger in triggers) {
- List<VCExpr!>! exprs = trigger.Exprs;
- List<VCExpr!>! newExprs = MutateList(exprs, arg);
+ foreach (VCTrigger/*!*/ trigger in triggers) {
+ Contract.Assert(trigger != null);
+ List<VCExpr/*!*/>/*!*/ exprs = trigger.Exprs;
+ List<VCExpr/*!*/>/*!*/ newExprs = MutateList(exprs, arg);
+
if (Object.ReferenceEquals(exprs, newExprs)) {
newTriggers.Add(trigger);
} else {
@@ -573,17 +879,23 @@ namespace Microsoft.Boogie.VCExprAST return newTriggers;
}
- public virtual VCExpr! Visit(VCExprQuantifier! node, Arg arg) {
+ public virtual VCExpr Visit(VCExprQuantifier node, Arg arg){
+Contract.Requires(node != null);
+Contract.Ensures(Contract.Result<VCExpr>() != null);
bool changed = false;
- VCExpr! body = node.Body;
- VCExpr! newbody = body.Accept(this, arg);
+ VCExpr/*!*/ body = node.Body;
+ Contract.Assert(body != null);
+ VCExpr/*!*/ newbody = body.Accept(this, arg);
+ Contract.Assert(newbody != null);
if (!Object.ReferenceEquals(body, newbody))
changed = true;
// visit the trigger expressions as well
- List<VCTrigger!>! triggers = node.Triggers;
- List<VCTrigger!>! newTriggers = MutateTriggers(triggers, arg);
+ List<VCTrigger/*!*/>/*!*/ triggers = node.Triggers;
+ Contract.Assert(cce.NonNullElements(triggers));
+ List<VCTrigger/*!*/>/*!*/ newTriggers = MutateTriggers(triggers, arg);
+ Contract.Assert(cce.NonNullElements(newTriggers));
if (!Object.ReferenceEquals(triggers, newTriggers))
changed = true;
@@ -593,19 +905,22 @@ namespace Microsoft.Boogie.VCExprAST newTriggers, node.Infos, newbody);
}
- public virtual VCExpr! Visit(VCExprLet! node, Arg arg) {
+ public virtual VCExpr Visit(VCExprLet node, Arg arg){
+Contract.Requires(node != null);
+Contract.Ensures(Contract.Result<VCExpr>() != null);
bool changed = false;
- VCExpr! body = node.Body;
- VCExpr! newbody = body.Accept(this, arg);
+ VCExpr/*!*/ body = node.Body;
+ VCExpr/*!*/ newbody = body.Accept(this, arg);
if (!Object.ReferenceEquals(body, newbody))
changed = true;
- List<VCExprLetBinding!>! newbindings = new List<VCExprLetBinding!> ();
+ List<VCExprLetBinding/*!*/>/*!*/ newbindings = new List<VCExprLetBinding/*!*/> ();
for (int i = 0; i < node.Length; ++i) {
- VCExprLetBinding! binding = node[i];
- VCExpr! e = binding.E;
- VCExpr! newE = e.Accept(this, arg);
+ VCExprLetBinding/*!*/ binding = node[i];
+ Contract.Assert(binding != null);
+ VCExpr/*!*/ e = binding.E;
+ VCExpr/*!*/ newE = e.Accept(this, arg);
if (Object.ReferenceEquals(e, newE)) {
newbindings.Add(binding);
} else {
@@ -618,174 +933,220 @@ namespace Microsoft.Boogie.VCExprAST return node;
return Gen.Let(newbindings, newbody);
}
- }
-
- ////////////////////////////////////////////////////////////////////////////
- // Substitutions and a visitor for applying substitutions. A substitution can
- // substitute both type variables and term variables
+ }
- public class VCExprSubstitution {
- private readonly List<IDictionary<VCExprVar!, VCExpr!>!>! TermSubsts;
- private readonly List<IDictionary<TypeVariable!, Type!>!>! TypeSubsts;
+ ////////////////////////////////////////////////////////////////////////////
+ // Substitutions and a visitor for applying substitutions. A substitution can
+ // substitute both type variables and term variables
+
+ public class VCExprSubstitution {
+ private readonly List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>/*!*/ TermSubsts;
+ [ContractInvariantMethod]
+ void TermSubstsInvariantMethod() {
+ Contract.Invariant(TermSubsts != null && Contract.ForAll(TermSubsts, i => cce.NonNullElements(i)));
+ }
+ private readonly List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>/*!*/ TypeSubsts;
+ [ContractInvariantMethod]
+ void TypeSubstsInvariantMethod() {
+ Contract.Invariant(TermSubsts != null && Contract.ForAll(TypeSubsts, i => cce.NonNullElements(i)));
+ }
- public VCExprSubstitution(IDictionary<VCExprVar!, VCExpr!>! termSubst,
- IDictionary<TypeVariable!, Type!>! typeSubst) {
- List<IDictionary<VCExprVar!, VCExpr!>!>! termSubsts =
- new List<IDictionary<VCExprVar!, VCExpr!>!> ();
+ public VCExprSubstitution(IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ termSubst, IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst) {
+ Contract.Requires(cce.NonNullElements(termSubst));
+ Contract.Requires(cce.NonNullElements(typeSubst));
+ List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/>/*!*/ termSubsts =
+ new List<IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/> ();
termSubsts.Add(termSubst);
- List<IDictionary<TypeVariable!, Type!>!>! typeSubsts =
- new List<IDictionary<TypeVariable!, Type!>!> ();
+ List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>/*!*/ typeSubsts =
+ new List<IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/>();
typeSubsts.Add(typeSubst);
this.TermSubsts = termSubsts;
this.TypeSubsts = typeSubsts;
}
- public VCExprSubstitution() {
- this(new Dictionary<VCExprVar!, VCExpr!> (), new Dictionary<TypeVariable!, Type!> ());
+ public VCExprSubstitution() :this(new Dictionary<VCExprVar/*!*/, VCExpr/*!*/>(), new Dictionary<TypeVariable/*!*/, Type/*!*/>()){
+
}
- public void PushScope() {
- TermSubsts.Add(new Dictionary<VCExprVar!, VCExpr!> ());
- TypeSubsts.Add(new Dictionary<TypeVariable!, Type!> ());
+ public void PushScope() {
+ TermSubsts.Add(new Dictionary<VCExprVar/*!*/, VCExpr/*!*/> ());
+ TypeSubsts.Add(new Dictionary<TypeVariable/*!*/, Type/*!*/>());
}
- public void PopScope() {
- TermSubsts.RemoveAt(TermSubsts.Count - 1);
- TypeSubsts.RemoveAt(TypeSubsts.Count - 1);
- }
+ public void PopScope() {
+ TermSubsts.RemoveAt(TermSubsts.Count - 1);
+ TypeSubsts.RemoveAt(TypeSubsts.Count - 1);
+ }
- public VCExpr this[VCExprVar! var] {
- get {
- VCExpr res;
- for (int i = TermSubsts.Count - 1; i >= 0; --i) {
- if (TermSubsts[i].TryGetValue(var, out res))
- return res;
+ public VCExpr this[VCExprVar/*!*/ var] {
+ get {
+ Contract.Requires(var != null);
+ VCExpr res;
+ for (int i = TermSubsts.Count - 1; i >= 0; --i) {
+ if (TermSubsts[i].TryGetValue(var, out res))
+ return res;
+ }
+ return null;
+ }
+ set {
+ TermSubsts[TermSubsts.Count - 1][var] = cce.NonNull(value);
}
- return null;
- }
- set {
- TermSubsts[TermSubsts.Count - 1][var] = (!)value;
}
- }
- public Type this[TypeVariable! var] {
- get {
- Type res;
- for (int i = TypeSubsts.Count - 1; i >= 0; --i) {
- if (TypeSubsts[i].TryGetValue(var, out res))
- return res;
+ public Type this[TypeVariable/*!*/ var] {
+ get {
+ Contract.Requires(var != null);
+ Type res;
+ for (int i = TypeSubsts.Count - 1; i >= 0; --i) {
+ if (TypeSubsts[i].TryGetValue(var, out res))
+ return res;
+ }
+ return null;
+ }
+ set {
+ TypeSubsts[TypeSubsts.Count - 1][var] = cce.NonNull(value);
}
- return null;
- }
- set {
- TypeSubsts[TypeSubsts.Count - 1][var] = (!)value;
}
- }
- public bool ContainsKey(VCExprVar! var) {
- return this[var] != null;
- }
+ public bool ContainsKey(VCExprVar var) {
+ Contract.Requires(var != null);
+ return this[var] != null;
+ }
- public bool ContainsKey(TypeVariable! var) {
- return this[var] != null;
- }
+ public bool ContainsKey(TypeVariable var) {
+ Contract.Requires(var != null);
+ return this[var] != null;
+ }
- public bool TermSubstIsEmpty { get {
- return forall{IDictionary<VCExprVar!, VCExpr!>! dict in TermSubsts;
- dict.Count == 0};
- } }
+ public bool TermSubstIsEmpty {
+ get {
+ return Contract.ForAll(TermSubsts, dict => dict.Count == 0);
+ }
+ }
- public bool TypeSubstIsEmpty { get {
- return forall{IDictionary<TypeVariable!, Type!>! dict in TypeSubsts;
- dict.Count == 0};
- } }
+ public bool TypeSubstIsEmpty {
+ get {
+ return Contract.ForAll(TypeSubsts, dict => dict.Count == 0);
+ }
+ }
- public IDictionary<TypeVariable!, Type!>! ToTypeSubst { get {
- IDictionary<TypeVariable!, Type!>! res = new Dictionary<TypeVariable!, Type!> ();
- foreach (IDictionary<TypeVariable!, Type!>! dict in TypeSubsts)
- foreach (KeyValuePair<TypeVariable!, Type!> pair in dict)
- // later ones overwrite earlier ones
- res[pair.Key] = pair.Value;
- return res;
- } }
+ public IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ ToTypeSubst {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result < IDictionary<TypeVariable, Type>>()));
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ res = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
+ foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {
+ foreach (KeyValuePair<TypeVariable/*!*/, Type/*!*/> pair in dict) {
+ Contract.Assert(cce.NonNullElements(pair));
+ // later ones overwrite earlier ones
+ res[pair.Key] = pair.Value;
+ }
+ }
+ return res;
+ }
+ }
- // the variables that are not mapped to themselves
- public IEnumerable<VCExprVar!>! TermDomain { get {
- Dictionary<VCExprVar!, bool>! domain = new Dictionary<VCExprVar!, bool> ();
- foreach (IDictionary<VCExprVar!, VCExpr!>! dict in TermSubsts)
- foreach (VCExprVar! var in dict.Keys)
+ // the variables that are not mapped to themselves
+ public IEnumerable<VCExprVar/*!*/>/*!*/ TermDomain {
+ get {Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<VCExprVar>>()));
+ Dictionary<VCExprVar/*!*/, bool>/*!*/ domain = new Dictionary<VCExprVar/*!*/, bool> ();
+ foreach (IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ dict in TermSubsts) {
+ Contract.Assert(dict != null);
+ foreach (VCExprVar/*!*/ var in dict.Keys) {
+ Contract.Assert(var != null);
if (!var.Equals(this[var]))
domain.Add(var, true);
+ }
+ }
return domain.Keys;
- } }
+ }
+ }
- // the variables that are not mapped to themselves
- public IEnumerable<TypeVariable!>! TypeDomain { get {
- Dictionary<TypeVariable!, bool>! domain = new Dictionary<TypeVariable!, bool> ();
- foreach (IDictionary<TypeVariable!, Type!>! dict in TypeSubsts)
- foreach (TypeVariable! var in dict.Keys)
+ // the variables that are not mapped to themselves
+ public IEnumerable<TypeVariable/*!*/>/*!*/ TypeDomain {
+ get {Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<TypeVariable>>()));
+ Dictionary<TypeVariable/*!*/, bool>/*!*/ domain = new Dictionary<TypeVariable/*!*/, bool> ();
+ foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts) {
+ Contract.Assert(dict != null);
+ foreach (TypeVariable/*!*/ var in dict.Keys) {
+ Contract.Assert(var != null);
if (!var.Equals(this[var]))
domain.Add(var, true);
+ }
+ }
return domain.Keys;
- } }
-
- public FreeVariableCollector! Codomains { get {
- FreeVariableCollector! coll = new FreeVariableCollector ();
- foreach (VCExprVar! var in TermDomain)
- coll.Collect((!)this[var]);
- foreach (TypeVariable! var in TypeDomain)
- coll.Collect((!)this[var]);
+ }
+ }
+
+ public FreeVariableCollector/*!*/ Codomains {
+ get {Contract.Ensures(Contract.Result<FreeVariableCollector>() != null);
+
+ FreeVariableCollector/*!*/ coll = new FreeVariableCollector ();
+ foreach (VCExprVar/*!*/ var in TermDomain)
+ coll.Collect(cce.NonNull(this)[var]);
+ foreach (TypeVariable/*!*/ var in TypeDomain)
+ coll.Collect(cce.NonNull(this)[var]);
return coll;
- } }
+ }
+ }
- public VCExprSubstitution! Clone() {
- VCExprSubstitution! res = new VCExprSubstitution ();
- foreach (IDictionary<VCExprVar!, VCExpr!>! dict in TermSubsts)
+ public VCExprSubstitution Clone() {
+Contract.Ensures(Contract.Result<VCExprSubstitution>() != null);
+ VCExprSubstitution/*!*/ res = new VCExprSubstitution ();
+ foreach (IDictionary<VCExprVar/*!*/, VCExpr/*!*/>/*!*/ dict in TermSubsts)
res.TermSubsts.Add(HelperFuns.Clone(dict));
- foreach (IDictionary<TypeVariable!, Type!>! dict in TypeSubsts)
+ foreach (IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ dict in TypeSubsts)
res.TypeSubsts.Add(HelperFuns.Clone(dict));
return res;
}
- }
+ }
- /////////////////////////////////////////////////////////////////////////////////
+ /////////////////////////////////////////////////////////////////////////////////
- public class SubstitutingVCExprVisitor
- : MutatingVCExprVisitor<VCExprSubstitution!> {
- public SubstitutingVCExprVisitor(VCExpressionGenerator! gen) {
- base(gen);
- }
+ public class SubstitutingVCExprVisitor
+ : MutatingVCExprVisitor<VCExprSubstitution/*!*/> {
+ public SubstitutingVCExprVisitor(VCExpressionGenerator gen) :base(gen){
+ Contract.Requires(gen != null);
+
+ }
- // when descending across a binder, we have to check that no collisions
- // or variable capture can occur. if this might happen, we replace the
- // term and type variables bound by the binder with fresh variables
- private bool CollisionPossible(IEnumerable<TypeVariable!>! typeParams,
- IEnumerable<VCExprVar!>! boundVars,
- VCExprSubstitution! substitution) {
+ // when descending across a binder, we have to check that no collisions
+ // or variable capture can occur. if this might happen, we replace the
+ // term and type variables bound by the binder with fresh variables
+ private bool CollisionPossible(IEnumerable<TypeVariable/*!*/>/*!*/ typeParams, IEnumerable<VCExprVar/*!*/>/*!*/ boundVars, VCExprSubstitution/*!*/ substitution) {
+ Contract.Requires(cce.NonNullElements(typeParams));
+ Contract.Requires(cce.NonNullElements(boundVars));
+ Contract.Requires(substitution != null);
// variables can be shadowed by a binder
- if (exists{TypeVariable! var in typeParams; substitution.ContainsKey(var)} ||
- exists{VCExprVar! var in boundVars; substitution.ContainsKey(var)})
+ if (Contract.Exists(typeParams, var=> substitution.ContainsKey(var)) ||
+ Contract.Exists(boundVars, var=> substitution.ContainsKey(var)))
return true;
// compute the codomain of the substitution
- FreeVariableCollector! coll = substitution.Codomains;
+ FreeVariableCollector coll = substitution.Codomains;
+ Contract.Assert(coll != null);
// variables could be captured when applying the substitution
- return exists{TypeVariable! var in typeParams; coll.FreeTypeVars.Contains(var)} ||
- exists{VCExprVar! var in boundVars; coll.FreeTermVars.ContainsKey(var)};
+ return Contract.Exists(typeParams, var=> coll.FreeTypeVars.Contains(var)) ||
+ Contract.Exists(boundVars, var=> coll.FreeTermVars.ContainsKey(var));
}
- // can be overwritten if names of bound variables are to be changed
- protected virtual string! ChooseNewVariableName(string! oldName) {
- return oldName;
- }
+ // can be overwritten if names of bound variables are to be changed
+ protected virtual string ChooseNewVariableName(string oldName) {
+ Contract.Requires(oldName != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+ return oldName;
+ }
- // handle type parameters in VCExprNAry
- protected override VCExpr! UpdateModifiedNode(VCExprNAry! originalNode,
- List<VCExpr!>! newSubExprs,
- bool changed,
- VCExprSubstitution! substitution) {
- List<Type!>! typeParams = new List<Type!> ();
- foreach (Type! t in originalNode.TypeArguments) {
- Type! newType = t.Substitute(substitution.ToTypeSubst);
+ // handle type parameters in VCExprNAry
+ protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List<VCExpr/*!*/>/*!*/ newSubExprs, bool changed, VCExprSubstitution/*!*/ substitution) {
+ Contract.Requires(originalNode != null);
+ Contract.Requires(cce.NonNullElements(newSubExprs));
+ Contract.Requires(substitution != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ List<Type/*!*/>/*!*/ typeParams = new List<Type/*!*/> ();
+ foreach (Type/*!*/ t in originalNode.TypeArguments) {
+ Contract.Assert(t != null);
+ Type/*!*/ newType = t.Substitute(substitution.ToTypeSubst);
+ Contract.Assert(newType != null);
if (!ReferenceEquals(t, newType))
changed = true;
typeParams.Add(newType);
@@ -796,211 +1157,272 @@ namespace Microsoft.Boogie.VCExprAST return originalNode;
}
- public override VCExpr! Visit(VCExprQuantifier! node,
- VCExprSubstitution! substitution) {
- // the default is to refresh bound variables only if necessary
- // because of collisions
- return Visit(node, substitution, false);
- }
-
- public VCExpr! Visit(VCExprQuantifier! node,
- VCExprSubstitution! substitution,
- bool refreshBoundVariables) {
- substitution.PushScope(); try {
+ public override VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution) {
+ Contract.Requires(node != null);
+ Contract.Requires(substitution != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
- List<TypeVariable!>! typeParams = node.TypeParameters;
- bool refreshAllVariables = refreshBoundVariables ||
- CollisionPossible(node.TypeParameters, node.BoundVars, substitution);
- if (refreshAllVariables) {
- // we introduce fresh type variables to ensure that none gets captured
- typeParams = new List<TypeVariable!> ();
- foreach (TypeVariable! var in node.TypeParameters) {
- TypeVariable! freshVar =
- new TypeVariable (Token.NoToken, ChooseNewVariableName(var.Name));
- typeParams.Add(freshVar);
- substitution[var] = freshVar;
- // this might overwrite other elements of the substitution, deliberately
- }
+ // the default is to refresh bound variables only if necessary
+ // because of collisions
+ return Visit(node, substitution, false);
}
- List<VCExprVar!>! boundVars = node.BoundVars;
- if (refreshAllVariables || !substitution.TypeSubstIsEmpty) {
- // collisions are possible, or we also substitute type variables. in this case
- // the bound term variables have to be replaced with fresh variables with the
- // right types
- boundVars = new List<VCExprVar!> ();
- IDictionary<TypeVariable!, Type!>! typeSubst = substitution.ToTypeSubst;
- foreach (VCExprVar! var in node.BoundVars) {
- VCExprVar! freshVar =
- Gen.Variable(ChooseNewVariableName(var.Name),
- var.Type.Substitute(typeSubst));
- boundVars.Add(freshVar);
- substitution[var] = freshVar;
- // this might overwrite other elements of the substitution, deliberately
- }
- }
+ public VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution, bool refreshBoundVariables) {
+ Contract.Requires(node != null);
+ Contract.Requires(substitution != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ substitution.PushScope();
+ try {
+
+ List<TypeVariable/*!*/>/*!*/ typeParams = node.TypeParameters;
+ Contract.Assert(cce.NonNullElements(typeParams));
+ bool refreshAllVariables = refreshBoundVariables ||
+ CollisionPossible(node.TypeParameters, node.BoundVars, substitution);
+ if (refreshAllVariables) {
+ // we introduce fresh type variables to ensure that none gets captured
+ typeParams = new List<TypeVariable/*!*/>();
+ foreach (TypeVariable/*!*/ var in node.TypeParameters) {
+ Contract.Assert(var != null);
+ TypeVariable/*!*/ freshVar =
+ new TypeVariable(Token.NoToken, ChooseNewVariableName(var.Name));
+ Contract.Assert(freshVar != null);
+ typeParams.Add(freshVar);
+ substitution[var] = freshVar;
+ // this might overwrite other elements of the substitution, deliberately
+ }
+ }
- List<VCTrigger!>! newTriggers = new List<VCTrigger!> ();
- foreach (VCTrigger! trigger in node.Triggers)
- newTriggers.Add(Gen.Trigger(trigger.Pos, MutateSeq(trigger.Exprs, substitution)));
+ List<VCExprVar/*!*/>/*!*/ boundVars = node.BoundVars;
+ Contract.Assert(cce.NonNullElements(boundVars));
+ if (refreshAllVariables || !substitution.TypeSubstIsEmpty) {
+ // collisions are possible, or we also substitute type variables. in this case
+ // the bound term variables have to be replaced with fresh variables with the
+ // right types
+ boundVars = new List<VCExprVar/*!*/>();
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;
+ Contract.Assert(cce.NonNullElements(typeSubst));
+ foreach (VCExprVar/*!*/ var in node.BoundVars) {
+ Contract.Assert(var != null);
+ VCExprVar/*!*/ freshVar =
+ Gen.Variable(ChooseNewVariableName(var.Name),
+ var.Type.Substitute(typeSubst));
+ Contract.Assert(freshVar != null);
+ boundVars.Add(freshVar);
+ substitution[var] = freshVar;
+ // this might overwrite other elements of the substitution, deliberately
+ }
+ }
- VCExpr! newBody = Mutate(node.Body, substitution);
+ List<VCTrigger/*!*/>/*!*/ newTriggers = new List<VCTrigger/*!*/>();
+ foreach (VCTrigger/*!*/ trigger in node.Triggers) {
+ Contract.Assert(trigger != null);
+ newTriggers.Add(Gen.Trigger(trigger.Pos, MutateSeq(trigger.Exprs, substitution)));
+ }
- return Gen.Quantify(node.Quan, typeParams, boundVars,
- newTriggers, node.Infos, newBody);
+ VCExpr/*!*/ newBody = Mutate(node.Body, substitution);
+ Contract.Assert(newBody != null);
- } finally {
- substitution.PopScope();
+ return Gen.Quantify(node.Quan, typeParams, boundVars,
+ newTriggers, node.Infos, newBody);
+
+ } finally {
+ substitution.PopScope();
+ }
}
- }
- public override VCExpr! Visit(VCExprVar! node,
- VCExprSubstitution! substitution) {
- VCExpr res = substitution[node];
- if (res != null)
- return res;
- return node;
- }
+ public override VCExpr Visit(VCExprVar node, VCExprSubstitution substitution) {
+ Contract.Requires(substitution != null);
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ VCExpr res = substitution[node];
+ if (res != null)
+ return res;
+ return node;
+ }
- public override VCExpr! Visit(VCExprLet! node,
- VCExprSubstitution! substitution) {
- // the default is to refresh bound variables only if necessary
- // because of collisions
- return Visit(node, substitution, false);
- }
+ public override VCExpr Visit(VCExprLet node, VCExprSubstitution substitution) {
+ Contract.Requires(substitution != null);
+ Contract.Requires(node != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ // the default is to refresh bound variables only if necessary
+ // because of collisions
+ return Visit(node, substitution, false);
+ }
- public VCExpr! Visit(VCExprLet! node,
- VCExprSubstitution! substitution,
- bool refreshBoundVariables) {
+ public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refreshBoundVariables){
+Contract.Requires(substitution != null);
+Contract.Requires(node != null);
+Contract.Ensures(Contract.Result<VCExpr>() != null);
// let-expressions do not have type parameters (fortunately ...)
substitution.PushScope (); try {
bool refreshAllVariables =
refreshBoundVariables ||
!substitution.TypeSubstIsEmpty ||
- CollisionPossible(new List<TypeVariable!> (), node.BoundVars, substitution);
+ CollisionPossible(new List<TypeVariable/*!*/> (), node.BoundVars, substitution);
- List<VCExprVar!>! newBoundVars = node.BoundVars;
+ List<VCExprVar/*!*/>/*!*/ newBoundVars = node.BoundVars;
+ Contract.Assert(cce.NonNullElements(newBoundVars));
if (refreshAllVariables) {
// collisions are possible, or we also substitute type variables. in this case
// the bound term variables have to be replaced with fresh variables with the
// right types
- newBoundVars = new List<VCExprVar!> ();
- IDictionary<TypeVariable!, Type!>! typeSubst = substitution.ToTypeSubst;
- foreach (VCExprVar! var in node.BoundVars) {
- VCExprVar! freshVar =
+ newBoundVars = new List<VCExprVar/*!*/> ();
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ typeSubst = substitution.ToTypeSubst;
+ Contract.Assert(cce.NonNullElements(typeSubst));
+ foreach (VCExprVar/*!*/ var in node.BoundVars) {
+ Contract.Assert(var != null);
+ VCExprVar/*!*/ freshVar =
Gen.Variable(ChooseNewVariableName(var.Name),
var.Type.Substitute(typeSubst));
+ Contract.Assert(freshVar != null);
newBoundVars.Add(freshVar);
substitution[var] = freshVar;
// this might overwrite other elements of the substitution, deliberately
}
}
- List<VCExprLetBinding!>! newbindings = new List<VCExprLetBinding!> ();
+ List<VCExprLetBinding/*!*/>/*!*/ newbindings = new List<VCExprLetBinding/*!*/> ();
for (int i = 0; i < node.Length; ++i) {
- VCExprLetBinding! binding = node[i];
+ VCExprLetBinding/*!*/ binding = node[i];
+ Contract.Assert(binding != null);
newbindings.Add(Gen.LetBinding(newBoundVars[i], Mutate(binding.E, substitution)));
}
-
- VCExpr! newBody = Mutate(node.Body, substitution);
+
+ VCExpr/*!*/ newBody = Mutate(node.Body, substitution);
+ Contract.Assert(newBody != null);
return Gen.Let(newbindings, newBody);
} finally {
substitution.PopScope();
}
}
- }
+ }
- ////////////////////////////////////////////////////////////////////////////
+ ////////////////////////////////////////////////////////////////////////////
+ [ContractClassFor(typeof(StandardVCExprOpVisitor<,>))]
+ public abstract class StandardVCExprOpVisitorContracts<Result, Arg> : StandardVCExprOpVisitor<Result, Arg> {
+ protected override Result StandardResult(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+ }
- public abstract class StandardVCExprOpVisitor<Result, Arg>
- : IVCExprOpVisitor<Result, Arg> {
- protected abstract Result StandardResult(VCExprNAry! node, Arg arg);
- public virtual Result VisitNotOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitEqOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitNeqOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitAndOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitOrOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitImpliesOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitDistinctOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitLabelOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitSelectOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitStoreOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitBvOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitBvExtractOp(VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitBvConcatOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitIfThenElseOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitCustomOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitAddOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitSubOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitMulOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitDivOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitModOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitLtOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitLeOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitGtOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitGeOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitSubtypeOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
- }
- public virtual Result VisitSubtype3Op (VCExprNAry! node, Arg arg) {
+ [ContractClass(typeof(StandardVCExprOpVisitorContracts<,>))]
+ public abstract class StandardVCExprOpVisitor<Result, Arg>
+ : IVCExprOpVisitor<Result, Arg> {
+ protected abstract Result StandardResult(VCExprNAry/*!*/ node, Arg arg);
+
+ public virtual Result VisitNotOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitEqOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitNeqOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitAndOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitOrOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitImpliesOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitDistinctOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitLabelOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitSelectOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitStoreOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitBvOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitBvExtractOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitBvConcatOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitIfThenElseOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitCustomOp (VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
return StandardResult(node, arg);
}
- public virtual Result VisitBoogieFunctionOp (VCExprNAry! node, Arg arg) {
- return StandardResult(node, arg);
+ public virtual Result VisitAddOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitSubOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitMulOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitDivOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitModOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitLtOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitLeOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitGtOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitGeOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitSubtypeOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitSubtype3Op(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
}
- }
-
-}
-
+ }
\ No newline at end of file |