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/VCExprAST.cs | |
| parent | 85ffcd8f1392bf871e585fe8efb60e38bfdb2f72 (diff) | |
Boogie: Committing new source code for VCExpr
Diffstat (limited to 'Source/VCExpr/VCExprAST.cs')
| -rw-r--r-- | Source/VCExpr/VCExprAST.cs | 1542 |
1 files changed, 1062 insertions, 480 deletions
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 7e5b31f1..40fadfac 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -8,145 +8,199 @@ using System.Text; using System.IO;
using System.Collections;
using System.Collections.Generic;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
// Prover-independent syntax trees for representing verification conditions
// The language can be seen as a simple polymorphically typed first-order logic,
// very similar to the expression language of Boogie
-namespace Microsoft.Boogie
-{
+namespace Microsoft.Boogie {
using Microsoft.Boogie.VCExprAST;
- public class VCExpressionGenerator
- {
- public static readonly VCExpr! False = new VCExprLiteral (Type.Bool);
- public static readonly VCExpr! True = new VCExprLiteral (Type.Bool);
+ public class VCExpressionGenerator {
+ public static readonly VCExpr False = new VCExprLiteral(Type.Bool);
+ public static readonly VCExpr True = new VCExprLiteral(Type.Bool);
private Function ControlFlowFunction = null;
- public VCExpr! ControlFlowFunctionApplication(VCExpr! e1, VCExpr! e2)
- {
+ public VCExpr ControlFlowFunctionApplication(VCExpr e1, VCExpr e2) {
+ Contract.Requires(e1 != null);
+ Contract.Requires(e2 != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
if (ControlFlowFunction == null) {
- Formal! first = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);
- Formal! second = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);
- VariableSeq! inputs = new VariableSeq();
+ Formal/*!*/ first = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);
+ Formal/*!*/ second = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), true);
+ VariableSeq inputs = new VariableSeq();
inputs.Add(first);
inputs.Add(second);
- Formal! returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), false);
+ Formal/*!*/ returnVar = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Int), false);
ControlFlowFunction = new Function(Token.NoToken, "ControlFlow", inputs, returnVar);
}
- List<VCExpr!> args = new List<VCExpr!>();
+ List<VCExpr/*!*/> args = new List<VCExpr/*!*/>();
args.Add(e1);
args.Add(e2);
return Function(BoogieFunctionOp(ControlFlowFunction), args);
}
-
- public VCExpr! Integer(BigNum x) {
+
+ public VCExpr/*!*/ Integer(BigNum x) {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
return new VCExprIntLit(x);
}
- public VCExpr! Function(VCExprOp! op,
- List<VCExpr!>! arguments,
- List<Type!>! typeArguments) {
+ public VCExpr/*!*/ Function(VCExprOp/*!*/ op,
+ List<VCExpr/*!*/>/*!*/ arguments,
+ List<Type/*!*/>/*!*/ typeArguments) {
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(arguments));
+ Contract.Requires(cce.NonNullElements(typeArguments));
if (typeArguments.Count > 0)
return new VCExprMultiAry(op, arguments, typeArguments);
switch (arguments.Count) {
- case 0: return new VCExprNullary(op);
- case 1: return new VCExprUnary(op, arguments);
- case 2: return new VCExprBinary(op, arguments);
- default: return new VCExprMultiAry(op, arguments);
+ case 0:
+ return new VCExprNullary(op);
+ case 1:
+ return new VCExprUnary(op, arguments);
+ case 2:
+ return new VCExprBinary(op, arguments);
+ default:
+ return new VCExprMultiAry(op, arguments);
}
}
- public VCExpr! Function(VCExprOp! op, List<VCExpr!>! arguments) {
+ public VCExpr/*!*/ Function(VCExprOp/*!*/ op, List<VCExpr/*!*/>/*!*/ arguments) {
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(arguments));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
return Function(op, arguments, VCExprNAry.EMPTY_TYPE_LIST);
}
- public VCExpr! Function(VCExprOp! op, params VCExpr[]! arguments)
- requires forall{int i in (0:arguments.Length); arguments[i] != null};
- {
+ public VCExpr/*!*/ Function(VCExprOp/*!*/ op, params VCExpr[]/*!*/ arguments) {
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(arguments));
+
return Function(op,
HelperFuns.ToNonNullList(arguments),
VCExprNAry.EMPTY_TYPE_LIST);
}
- public VCExpr! Function(VCExprOp! op, VCExpr[]! arguments, Type[]! typeArguments)
- requires forall{int i in (0:arguments.Length); arguments[i] != null};
- requires forall{int i in (0:typeArguments.Length); typeArguments[i] != null};
- {
+ public VCExpr/*!*/ Function(VCExprOp/*!*/ op, VCExpr[]/*!*/ arguments, Type[]/*!*/ typeArguments) {
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(arguments));
+ Contract.Requires(cce.NonNullElements(typeArguments));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+
return Function(op,
HelperFuns.ToNonNullList(arguments),
HelperFuns.ToNonNullList(typeArguments));
}
- public VCExpr! Function(Function! op, List<VCExpr!>! arguments) {
+ public VCExpr/*!*/ Function(Function/*!*/ op, List<VCExpr/*!*/>/*!*/ arguments) {
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(arguments));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
return Function(BoogieFunctionOp(op), arguments, VCExprNAry.EMPTY_TYPE_LIST);
}
- public VCExpr! Function(Function! op, params VCExpr[]! arguments)
- requires forall{int i in (0:arguments.Length); arguments[i] != null};
- {
+ public VCExpr/*!*/ Function(Function/*!*/ op, params VCExpr[]/*!*/ arguments) {
+ Contract.Requires(cce.NonNullElements(arguments));
+ Contract.Requires(op != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
return Function(BoogieFunctionOp(op), arguments);
}
// The following method should really be called "ReduceLeft". It must
// only be used for the binary operators "and" and "or"
- public VCExpr! NAry(VCExprOp! op, List<VCExpr!>! args) {
+ public VCExpr/*!*/ NAry(VCExprOp/*!*/ op, List<VCExpr/*!*/>/*!*/ args) {
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
return NAry(op, args.ToArray());
}
- public VCExpr! NAry(VCExprOp! op, params VCExpr[]! args)
- requires forall{int i in (0:args.Length); args[i] != null};
- requires op == AndOp || op == OrOp; {
+ public VCExpr/*!*/ NAry(VCExprOp/*!*/ op, params VCExpr[]/*!*/ args) {
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Requires(op == AndOp || op == OrOp);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
bool and = (op == AndOp);
- VCExpr! e = and ? True : False;
+ VCExpr/*!*/ e = and ? True : False;
foreach (VCExpr a in args) {
- e = and ? AndSimp(e, (!)a) : OrSimp(e, (!)a);
+ e = and ? AndSimp(e, cce.NonNull(a)) : OrSimp(e, cce.NonNull(a));
}
return e;
- }
+ }
////////////////////////////////////////////////////////////////////////////////
- public static readonly VCExprOp! NotOp = new VCExprNAryOp (1, Type.Bool);
- public static readonly VCExprOp! EqOp = new VCExprNAryOp (2, Type.Bool);
- public static readonly VCExprOp! NeqOp = new VCExprNAryOp (2, Type.Bool);
- public static readonly VCExprOp! AndOp = new VCExprNAryOp (2, Type.Bool);
- public static readonly VCExprOp! OrOp = new VCExprNAryOp (2, Type.Bool);
- public static readonly VCExprOp! ImpliesOp = new VCExprNAryOp (2, Type.Bool);
+ public static readonly VCExprOp NotOp = new VCExprNAryOp(1, Type.Bool);
+ public static readonly VCExprOp EqOp = new VCExprNAryOp(2, Type.Bool);
+ public static readonly VCExprOp NeqOp = new VCExprNAryOp(2, Type.Bool);
+ public static readonly VCExprOp AndOp = new VCExprNAryOp(2, Type.Bool);
+ public static readonly VCExprOp OrOp = new VCExprNAryOp(2, Type.Bool);
+ public static readonly VCExprOp ImpliesOp = new VCExprNAryOp(2, Type.Bool);
- public VCExprDistinctOp! DistinctOp(int arity) {
- return new VCExprDistinctOp (arity);
+ public VCExprDistinctOp DistinctOp(int arity) {
+ Contract.Ensures(Contract.Result<VCExprDistinctOp>() != null);
+
+ return new VCExprDistinctOp(arity);
}
- public VCExpr! Not(List<VCExpr!>! args)
- requires args.Count == 1; {
+ public VCExpr/*!*/ Not(List<VCExpr/*!*/>/*!*/ args) {
+ Contract.Requires(args != null);
+ Contract.Requires(args.Count == 1);
+ Contract.Requires(args[0] != null);
return Function(NotOp, args);
}
- public VCExpr! Not(VCExpr! e0) {
+ public VCExpr/*!*/ Not(VCExpr/*!*/ e0) {
+ Contract.Requires(e0 != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
return Function(NotOp, e0);
}
- public VCExpr! Eq(VCExpr! e0, VCExpr! e1) {
+ public VCExpr/*!*/ Eq(VCExpr/*!*/ e0, VCExpr/*!*/ e1) {
return Function(EqOp, e0, e1);
}
- public VCExpr! Neq(VCExpr! e0, VCExpr! e1) {
+ public VCExpr/*!*/ Neq(VCExpr/*!*/ e0, VCExpr/*!*/ e1) {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
return Function(NeqOp, e0, e1);
}
- public VCExpr! And(VCExpr! e0, VCExpr! e1) {
+ public VCExpr/*!*/ And(VCExpr/*!*/ e0, VCExpr/*!*/ e1) {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(AndOp, e0, e1);
}
- public VCExpr! Or(VCExpr! e0, VCExpr! e1) {
+ public VCExpr/*!*/ Or(VCExpr/*!*/ e0, VCExpr/*!*/ e1) {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(OrOp, e0, e1);
}
- public VCExpr! Implies(VCExpr! e0, VCExpr! e1) {
+ public VCExpr/*!*/ Implies(VCExpr/*!*/ e0, VCExpr/*!*/ e1) {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(ImpliesOp, e0, e1);
}
- public VCExpr! Distinct(List<VCExpr!>! args) {
+ public VCExpr/*!*/ Distinct(List<VCExpr/*!*/>/*!*/ args) {
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
if (args.Count <= 1)
// trivial case
return True;
@@ -157,14 +211,19 @@ namespace Microsoft.Boogie // Versions of the propositional operators that automatically simplify in
// certain cases (for example, if one of the operators is True or False)
- public VCExpr! NotSimp(VCExpr! e0) {
+ public VCExpr NotSimp(VCExpr e0) {
+ Contract.Requires(e0 != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
if (e0.Equals(True))
return False;
if (e0.Equals(False))
return True;
return Not(e0);
}
- public VCExpr! AndSimp(VCExpr! e0, VCExpr! e1) {
+ public VCExpr AndSimp(VCExpr e0, VCExpr e1) {
+ Contract.Requires(e1 != null);
+ Contract.Requires(e0 != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
if (e0.Equals(True))
return e1;
if (e1.Equals(True))
@@ -173,7 +232,10 @@ namespace Microsoft.Boogie return False;
return And(e0, e1);
}
- public VCExpr! OrSimp(VCExpr! e0, VCExpr! e1) {
+ public VCExpr OrSimp(VCExpr e0, VCExpr e1) {
+ Contract.Requires(e1 != null);
+ Contract.Requires(e0 != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
if (e0.Equals(False))
return e1;
if (e1.Equals(False))
@@ -182,7 +244,10 @@ namespace Microsoft.Boogie return True;
return Or(e0, e1);
}
- public VCExpr! ImpliesSimp(VCExpr! e0, VCExpr! e1) {
+ public VCExpr ImpliesSimp(VCExpr e0, VCExpr e1) {
+ Contract.Requires(e1 != null);
+ Contract.Requires(e0 != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
if (e0.Equals(True))
return e1;
if (e1.Equals(False))
@@ -204,13 +269,14 @@ namespace Microsoft.Boogie }
return Implies(e0, e1);
}
-
+
///<summary>
/// Returns some measure of the number of conjuncts in e. This could be the total number of conjuncts in all
/// top-most layers of the expression, or it can simply be the length of the left-prong of this and-tree. The
/// important thing is that: AndSize(e0) >= AndSize(31) ==> AndSize(And(e0,e1)) > AndSize(e0).
///</summary>
- int AndSize(VCExpr! e) {
+ int AndSize(VCExpr e) {
+ Contract.Requires(e != null);
int n = 1;
while (true) {
VCExprNAry nary = e as VCExprNAry;
@@ -226,42 +292,54 @@ namespace Microsoft.Boogie ////////////////////////////////////////////////////////////////////////////////
// Further operators
- public static readonly VCExprOp! AddOp = new VCExprNAryOp (2, Type.Int);
- public static readonly VCExprOp! SubOp = new VCExprNAryOp (2, Type.Int);
- public static readonly VCExprOp! MulOp = new VCExprNAryOp (2, Type.Int);
- public static readonly VCExprOp! DivOp = new VCExprNAryOp (2, Type.Int);
- public static readonly VCExprOp! ModOp = new VCExprNAryOp (2, Type.Int);
- public static readonly VCExprOp! LtOp = new VCExprNAryOp (2, Type.Bool);
- public static readonly VCExprOp! LeOp = new VCExprNAryOp (2, Type.Bool);
- public static readonly VCExprOp! GtOp = new VCExprNAryOp (2, Type.Bool);
- public static readonly VCExprOp! GeOp = new VCExprNAryOp (2, Type.Bool);
- public static readonly VCExprOp! SubtypeOp = new VCExprNAryOp (2, Type.Bool);
+ public static readonly VCExprOp AddOp = new VCExprNAryOp(2, Type.Int);
+ public static readonly VCExprOp SubOp = new VCExprNAryOp(2, Type.Int);
+ public static readonly VCExprOp MulOp = new VCExprNAryOp(2, Type.Int);
+ public static readonly VCExprOp DivOp = new VCExprNAryOp(2, Type.Int);
+ public static readonly VCExprOp ModOp = new VCExprNAryOp(2, Type.Int);
+ public static readonly VCExprOp LtOp = new VCExprNAryOp(2, Type.Bool);
+ public static readonly VCExprOp LeOp = new VCExprNAryOp(2, Type.Bool);
+ public static readonly VCExprOp GtOp = new VCExprNAryOp(2, Type.Bool);
+ public static readonly VCExprOp GeOp = new VCExprNAryOp(2, Type.Bool);
+ public static readonly VCExprOp SubtypeOp = new VCExprNAryOp(2, Type.Bool);
// ternary version of the subtype operator, the first argument of which gives
// the type of the compared terms
- public static readonly VCExprOp! Subtype3Op = new VCExprNAryOp (3, Type.Bool);
- public static readonly VCExprOp! IfThenElseOp = new VCExprIfThenElseOp();
-
- public static readonly VCExprOp! TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool);
+ public static readonly VCExprOp Subtype3Op = new VCExprNAryOp(3, Type.Bool);
+ public static readonly VCExprOp IfThenElseOp = new VCExprIfThenElseOp();
+
+ public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool);
- public VCExprOp! BoogieFunctionOp(Function! func) {
+ public VCExprOp BoogieFunctionOp(Function func) {
+ Contract.Requires(func != null);
+ Contract.Ensures(Contract.Result<VCExprOp>() != null);
return new VCExprBoogieFunctionOp(func);
}
// Bitvector nodes
- public VCExpr! Bitvector(BvConst! bv) {
+ public VCExpr Bitvector(BvConst bv) {
+ Contract.Requires(bv != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(new VCExprBvOp(bv.Bits), Integer(bv.Value));
}
- public VCExpr! BvExtract(VCExpr! bv, int bits, int start, int end) {
+ public VCExpr BvExtract(VCExpr bv, int bits, int start, int end) {
+ Contract.Requires(bv != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(new VCExprBvExtractOp(start, end, bits), bv);
}
- public VCExpr! BvConcat(VCExpr! bv1, VCExpr! bv2) {
+ public VCExpr BvConcat(VCExpr bv1, VCExpr bv2) {
+ Contract.Requires(bv2 != null);
+ Contract.Requires(bv1 != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(new VCExprBvConcatOp(bv1.Type.BvBits, bv2.Type.BvBits), bv1, bv2);
}
- public VCExpr! AtMost(VCExpr! smaller, VCExpr! greater) {
+ public VCExpr AtMost(VCExpr smaller, VCExpr greater) {
+ Contract.Requires(greater != null);
+ Contract.Requires(smaller != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(SubtypeOp, smaller, greater);
}
@@ -270,31 +348,52 @@ namespace Microsoft.Boogie // Dispatcher for the visitor
// the declared singleton operators
- internal enum SingletonOp { NotOp, EqOp, NeqOp, AndOp, OrOp, ImpliesOp,
- AddOp, SubOp, MulOp,
- DivOp, ModOp, LtOp, LeOp, GtOp, GeOp, SubtypeOp,
- Subtype3Op, BvConcatOp };
- internal static Dictionary<VCExprOp!, SingletonOp>! SingletonOpDict;
+ internal enum SingletonOp {
+ NotOp,
+ EqOp,
+ NeqOp,
+ AndOp,
+ OrOp,
+ ImpliesOp,
+ AddOp,
+ SubOp,
+ MulOp,
+ DivOp,
+ ModOp,
+ LtOp,
+ LeOp,
+ GtOp,
+ GeOp,
+ SubtypeOp,
+ Subtype3Op,
+ BvConcatOp
+ };
+ internal static Dictionary<VCExprOp/*!*/, SingletonOp>/*!*/ SingletonOpDict;
+ [ContractInvariantMethod]
+ void MiscInvariant() {
+ Contract.Invariant(cce.NonNullElements(SingletonOpDict));
+ }
+
static VCExpressionGenerator() {
- SingletonOpDict = new Dictionary<VCExprOp!, SingletonOp> ();
- SingletonOpDict.Add(NotOp, SingletonOp.NotOp);
- SingletonOpDict.Add(EqOp, SingletonOp.EqOp);
- SingletonOpDict.Add(NeqOp, SingletonOp.NeqOp);
- SingletonOpDict.Add(AndOp, SingletonOp.AndOp);
- SingletonOpDict.Add(OrOp, SingletonOp.OrOp);
+ SingletonOpDict = new Dictionary<VCExprOp/*!*/, SingletonOp>();
+ SingletonOpDict.Add(NotOp, SingletonOp.NotOp);
+ SingletonOpDict.Add(EqOp, SingletonOp.EqOp);
+ SingletonOpDict.Add(NeqOp, SingletonOp.NeqOp);
+ SingletonOpDict.Add(AndOp, SingletonOp.AndOp);
+ SingletonOpDict.Add(OrOp, SingletonOp.OrOp);
SingletonOpDict.Add(ImpliesOp, SingletonOp.ImpliesOp);
- SingletonOpDict.Add(AddOp, SingletonOp.AddOp);
- SingletonOpDict.Add(SubOp, SingletonOp.SubOp);
- SingletonOpDict.Add(MulOp, SingletonOp.MulOp);
- SingletonOpDict.Add(DivOp, SingletonOp.DivOp);
- SingletonOpDict.Add(ModOp, SingletonOp.ModOp);
- SingletonOpDict.Add(LtOp, SingletonOp.LtOp);
- SingletonOpDict.Add(LeOp, SingletonOp.LeOp);
- SingletonOpDict.Add(GtOp, SingletonOp.GtOp);
- SingletonOpDict.Add(GeOp, SingletonOp.GeOp);
+ SingletonOpDict.Add(AddOp, SingletonOp.AddOp);
+ SingletonOpDict.Add(SubOp, SingletonOp.SubOp);
+ SingletonOpDict.Add(MulOp, SingletonOp.MulOp);
+ SingletonOpDict.Add(DivOp, SingletonOp.DivOp);
+ SingletonOpDict.Add(ModOp, SingletonOp.ModOp);
+ SingletonOpDict.Add(LtOp, SingletonOp.LtOp);
+ SingletonOpDict.Add(LeOp, SingletonOp.LeOp);
+ SingletonOpDict.Add(GtOp, SingletonOp.GtOp);
+ SingletonOpDict.Add(GeOp, SingletonOp.GeOp);
SingletonOpDict.Add(SubtypeOp, SingletonOp.SubtypeOp);
- SingletonOpDict.Add(Subtype3Op,SingletonOp.Subtype3Op);
+ SingletonOpDict.Add(Subtype3Op, SingletonOp.Subtype3Op);
}
////////////////////////////////////////////////////////////////////////////////
@@ -302,25 +401,32 @@ namespace Microsoft.Boogie // Let-bindings
- public VCExprLetBinding! LetBinding(VCExprVar! v, VCExpr! e) {
+ public VCExprLetBinding LetBinding(VCExprVar v, VCExpr e) {
+ Contract.Requires(e != null);
+ Contract.Requires(v != null);
+ Contract.Ensures(Contract.Result<VCExprLetBinding>() != null);
return new VCExprLetBinding(v, e);
}
-
+
// A "real" let expression. All let-bindings happen simultaneously, i.e.,
// at this level the order of the bindings does not matter. It is possible to
// create expressions like "let x = y, y = 5 in ...". All bound variables are
// bound in all bound terms/formulas and can occur there, but the dependencies
// have to be acyclic
- public VCExpr! Let(List<VCExprLetBinding!>! bindings, VCExpr! body) {
+ public VCExpr Let(List<VCExprLetBinding> bindings, VCExpr body) {
+ Contract.Requires(body != null);
+ Contract.Requires(cce.NonNullElements(bindings));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
if (bindings.Count == 0)
// no empty let-bindings
return body;
return new VCExprLet(bindings, body);
}
- public VCExpr! Let(VCExpr! body, params VCExprLetBinding[]! bindings)
- requires forall{int i in (0:bindings.Length); bindings[i] != null};
- {
+ public VCExpr Let(VCExpr body, params VCExprLetBinding[] bindings) {
+ Contract.Requires(body != null);
+ Contract.Requires((cce.NonNullElements(bindings)));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Let(HelperFuns.ToNonNullList(bindings), body);
}
@@ -338,8 +444,10 @@ namespace Microsoft.Boogie // Turn let-bindings let v = E in ... into implications E ==> v
- public VCExpr! AsImplications(List<VCExprLetBinding!>! bindings) {
- VCExpr! antecedents = True;
+ public VCExpr AsImplications(List<VCExprLetBinding> bindings) {
+ Contract.Requires(cce.NonNullElements(bindings));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ VCExpr/*!*/ antecedents = True;
foreach (VCExprLetBinding b in bindings)
// turn "LET_binding v = E" into "v <== E"
antecedents = AndSimp(antecedents, Implies(b.E, b.V));
@@ -347,8 +455,10 @@ namespace Microsoft.Boogie }
// Turn let-bindings let v = E in ... into equations v == E
- public VCExpr! AsEquations(List<VCExprLetBinding!>! bindings) {
- VCExpr! antecedents = True;
+ public VCExpr AsEquations(List<VCExprLetBinding> bindings) {
+ Contract.Requires(cce.NonNullElements(bindings));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ VCExpr/*!*/ antecedents = True;
foreach (VCExprLetBinding b in bindings)
// turn "LET_binding v = E" into "v <== E"
antecedents = AndSimp(antecedents, Eq(b.E, b.V));
@@ -359,50 +469,58 @@ namespace Microsoft.Boogie // Maps
- public VCExpr! Select(params VCExpr[]! allArgs)
- requires forall{int i in (0:allArgs.Length); allArgs[i] != null};
- {
+ public VCExpr Select(params VCExpr[] allArgs) {
+ Contract.Requires(allArgs != null);
+ Contract.Requires((cce.NonNullElements(allArgs)));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(new VCExprSelectOp(allArgs.Length - 1, 0),
HelperFuns.ToNonNullList(allArgs),
VCExprNAry.EMPTY_TYPE_LIST);
}
- public VCExpr! Select(VCExpr[]! allArgs, Type[]! typeArgs)
- requires 1 <= allArgs.Length;
- requires forall{int i in (0:allArgs.Length); allArgs[i] != null};
- requires forall{int i in (0:typeArgs.Length); typeArgs[i] != null};
- {
+ public VCExpr Select(VCExpr[] allArgs, Type[] typeArgs) {
+ Contract.Requires(1 <= allArgs.Length);
+ Contract.Requires(cce.NonNullElements(allArgs));
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(new VCExprSelectOp(allArgs.Length - 1, typeArgs.Length),
allArgs, typeArgs);
}
- public VCExpr! Select(List<VCExpr!>! allArgs, List<Type!>! typeArgs)
- requires 1 <= allArgs.Count;
- {
+ public VCExpr Select(List<VCExpr> allArgs, List<Type> typeArgs) {
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(cce.NonNullElements(allArgs));
+ Contract.Requires((1 <= allArgs.Count));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(new VCExprSelectOp(allArgs.Count - 1, typeArgs.Count),
allArgs, typeArgs);
}
- public VCExpr! Store(params VCExpr[]! allArgs)
- requires forall{int i in (0:allArgs.Length); allArgs[i] != null};
- {
+ public VCExpr Store(params VCExpr[] allArgs) {
+ Contract.Requires(allArgs != null);
+ Contract.Requires(cce.NonNullElements(allArgs));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(new VCExprStoreOp(allArgs.Length - 2, 0),
HelperFuns.ToNonNullList(allArgs),
VCExprNAry.EMPTY_TYPE_LIST);
}
- public VCExpr! Store(VCExpr[]! allArgs, Type[]! typeArgs)
- requires 2 <= allArgs.Length;
- requires forall{int i in (0:allArgs.Length); allArgs[i] != null};
- requires forall{int i in (0:typeArgs.Length); typeArgs[i] != null};
- {
+ public VCExpr Store(VCExpr[] allArgs, Type[] typeArgs) {
+ Contract.Requires(typeArgs != null);
+ Contract.Requires(allArgs != null);
+ Contract.Requires((2 <= allArgs.Length));
+ Contract.Requires(cce.NonNullElements(allArgs));
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(new VCExprStoreOp(allArgs.Length - 2, typeArgs.Length),
allArgs, typeArgs);
}
- public VCExpr! Store(List<VCExpr!>! allArgs, List<Type!>! typeArgs)
- requires 2 <= allArgs.Count;
- {
+ public VCExpr Store(List<VCExpr> allArgs, List<Type/*!*/>/*!*/ typeArgs) {
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(cce.NonNullElements(allArgs));
+ Contract.Requires((2 <= allArgs.Count));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(new VCExprStoreOp(allArgs.Count - 2, typeArgs.Count),
allArgs, typeArgs);
}
@@ -410,96 +528,132 @@ namespace Microsoft.Boogie // Labels
- public VCExprLabelOp! LabelOp(bool pos, string! l) {
+ public VCExprLabelOp LabelOp(bool pos, string l) {
+ Contract.Requires(l != null);
+ Contract.Ensures(Contract.Result<VCExprLabelOp>() != null);
return new VCExprLabelOp(pos, l);
}
- public VCExpr! LabelNeg(string! label, VCExpr! e) {
+ public VCExpr LabelNeg(string label, VCExpr e) {
+ Contract.Requires(e != null);
+ Contract.Requires(label != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
if (e.Equals(True)) {
return e; // don't bother putting negative labels around True (which will expose the True to further peephole optimizations)
}
return Function(LabelOp(false, label), e);
}
- public VCExpr! LabelPos(string! label, VCExpr! e) {
+ public VCExpr LabelPos(string label, VCExpr e) {
+ Contract.Requires(e != null);
+ Contract.Requires(label != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Function(LabelOp(true, label), e);
}
// Quantifiers
- public VCExpr! Quantify(Quantifier quan,
- List<TypeVariable!>! typeParams, List<VCExprVar!>! vars,
- List<VCTrigger!>! triggers, VCQuantifierInfos! infos,
- VCExpr! body) {
+ public VCExpr Quantify(Quantifier quan, List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCQuantifierInfos infos, VCExpr body) {
+ Contract.Requires(body != null);
+ Contract.Requires(infos != null);
+ Contract.Requires(cce.NonNullElements(triggers));
+ Contract.Requires(cce.NonNullElements(vars));
+ Contract.Requires(cce.NonNullElements(typeParams));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return new VCExprQuantifier(quan, typeParams, vars, triggers, infos, body);
}
- public VCExpr! Forall(List<TypeVariable!>! typeParams, List<VCExprVar!>! vars,
- List<VCTrigger!>! triggers, VCQuantifierInfos! infos,
- VCExpr! body) {
+ public VCExpr Forall(List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCQuantifierInfos infos, VCExpr body) {
+ Contract.Requires(body != null);
+ Contract.Requires(infos != null);
+ Contract.Requires(cce.NonNullElements(triggers));
+ Contract.Requires(cce.NonNullElements(vars));
+ Contract.Requires(cce.NonNullElements(typeParams));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Quantify(Quantifier.ALL, typeParams, vars, triggers, infos, body);
}
- public VCExpr! Forall(List<VCExprVar!>! vars,
- List<VCTrigger!>! triggers,
- string! qid, VCExpr! body) {
- return Quantify(Quantifier.ALL, new List<TypeVariable!> (), vars,
+ public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, string qid, VCExpr body){
+Contract.Requires(body != null);Contract.Requires(qid != null);Contract.Requires(cce.NonNullElements(triggers));Contract.Requires(cce.NonNullElements(vars));
+Contract.Ensures(Contract.Result<VCExpr>() != null);
+return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,
triggers, new VCQuantifierInfos (qid, -1, false, null), body);
}
- public VCExpr! Forall(List<VCExprVar!>! vars,
- List<VCTrigger!>! triggers,
- VCExpr! body) {
- return Quantify(Quantifier.ALL, new List<TypeVariable!> (), vars,
+ public VCExpr Forall(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body){
+Contract.Requires(body != null);Contract.Requires(cce.NonNullElements(triggers));Contract.Requires(cce.NonNullElements(vars));
+Contract.Ensures(Contract.Result<VCExpr>() != null);
+return Quantify(Quantifier.ALL, new List<TypeVariable/*!*/>(), vars,
triggers, new VCQuantifierInfos (null, -1, false, null), body);
}
- public VCExpr! Forall(VCExprVar! var, VCTrigger! trigger, VCExpr! body) {
+ public VCExpr Forall(VCExprVar var, VCTrigger trigger, VCExpr body) {
+ Contract.Requires(body != null);
+ Contract.Requires(trigger != null);
+ Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Forall(HelperFuns.ToNonNullList(var), HelperFuns.ToNonNullList(trigger), body);
}
- public VCExpr! Exists(List<TypeVariable!>! typeParams, List<VCExprVar!>! vars,
- List<VCTrigger!>! triggers, VCQuantifierInfos! infos,
- VCExpr! body) {
+ public VCExpr Exists(List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCQuantifierInfos infos, VCExpr body) {
+ Contract.Requires(body != null);
+ Contract.Requires(infos != null);
+ Contract.Requires(cce.NonNullElements(triggers));
+ Contract.Requires(cce.NonNullElements(vars));
+ Contract.Requires(cce.NonNullElements(typeParams));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Quantify(Quantifier.EX, typeParams, vars, triggers, infos, body);
}
- public VCExpr! Exists(List<VCExprVar!>! vars,
- List<VCTrigger!>! triggers,
- VCExpr! body) {
- return Quantify(Quantifier.EX, new List<TypeVariable!> (), vars,
+ public VCExpr Exists(List<VCExprVar/*!*/>/*!*/ vars, List<VCTrigger/*!*/>/*!*/ triggers, VCExpr body){
+Contract.Requires(body != null);
+ Contract.Requires(cce.NonNullElements(triggers));
+ Contract.Requires(cce.NonNullElements(vars));
+Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return Quantify(Quantifier.EX, new List<TypeVariable/*!*/> (), vars,
triggers, new VCQuantifierInfos (null, -1, false, null), body);
}
- public VCExpr! Exists(VCExprVar! var, VCTrigger! trigger, VCExpr! body) {
+ public VCExpr Exists(VCExprVar var, VCTrigger trigger, VCExpr body) {
+ Contract.Requires(body != null);
+ Contract.Requires(trigger != null);
+ Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
return Exists(HelperFuns.ToNonNullList(var), HelperFuns.ToNonNullList(trigger), body);
}
- public VCTrigger! Trigger(bool pos, List<VCExpr!>! exprs) {
+ public VCTrigger Trigger(bool pos, List<VCExpr> exprs) {
+ Contract.Requires(cce.NonNullElements(exprs));
+ Contract.Ensures(Contract.Result<VCTrigger>() != null);
return new VCTrigger(pos, exprs);
}
- public VCTrigger! Trigger(bool pos, params VCExpr[]! exprs)
- requires forall{int i in (0:exprs.Length); exprs[i] != null};
- {
+ public VCTrigger Trigger(bool pos, params VCExpr[] exprs) {
+ Contract.Requires(exprs != null);
+ Contract.Requires((Contract.ForAll(0, exprs.Length, i => exprs[i] != null)));
+ Contract.Ensures(Contract.Result<VCTrigger>() != null);
return Trigger(pos, HelperFuns.ToNonNullList(exprs));
}
// Reference to a bound or free variable
- public VCExprVar! Variable(string! name, Type! type) {
+ public VCExprVar Variable(string name, Type type) {
+ Contract.Requires(type != null);
+ Contract.Requires(name != null);
+ Contract.Ensures(Contract.Result<VCExprVar>() != null);
return new VCExprVar(name, type);
}
}
}
-namespace Microsoft.Boogie.VCExprAST
-{
+namespace Microsoft.Boogie.VCExprAST {
public class HelperFuns {
- public static bool SameElements(IEnumerable! a, IEnumerable! b) {
+ public static bool SameElements(IEnumerable a, IEnumerable b) {
+ Contract.Requires(b != null);
+ Contract.Requires(a != null);
IEnumerator ia = a.GetEnumerator();
IEnumerator ib = b.GetEnumerator();
while (true) {
if (ia.MoveNext()) {
if (ib.MoveNext()) {
- if (!((!)ia.Current).Equals(ib.Current))
+ if (!cce.NonNull(ia.Current).Equals(ib.Current))
return false;
} else {
- return false;
+ return false;
}
} else {
return !ib.MoveNext();
@@ -508,55 +662,81 @@ namespace Microsoft.Boogie.VCExprAST return true;
}
- public static int PolyHash(int init, int factor, IEnumerable! a) {
+ public static int PolyHash(int init, int factor, IEnumerable a) {
+ Contract.Requires(a != null);
int res = init;
- foreach(object x in a)
- res = res * factor + ((!)x).GetHashCode();
+ foreach (object x in a)
+ res = res * factor + (cce.NonNull(x)).GetHashCode();
return res;
}
- public static List<T>! ToList<T>(IEnumerable<T>! l) {
- List<T>! res = new List<T> ();
+ public static List<T> ToList<T>(IEnumerable<T> l) {
+ Contract.Requires(l != null);
+ Contract.Ensures(Contract.Result<List<T>>() != null);
+ List<T>/*!*/ res = new List<T>();
foreach (T x in l)
res.Add(x);
return res;
}
- public static TypeSeq! ToTypeSeq(VCExpr[]! exprs, int startIndex)
- requires forall{int i in (0:exprs.Length); exprs[i] != null};
- {
- TypeSeq! res = new TypeSeq ();
+ public static TypeSeq ToTypeSeq(VCExpr[] exprs, int startIndex){
+Contract.Requires(exprs != null);
+Contract.Requires((Contract.ForAll(0,exprs.Length, i=> exprs[i] != null)));
+Contract.Ensures(Contract.Result<TypeSeq>() != null);
+TypeSeq/*!*/ res = new TypeSeq();
for (int i = startIndex; i < exprs.Length; ++i)
- res.Add(((!)exprs[i]).Type);
+ res.Add(cce.NonNull(exprs[i]).Type);
return res;
}
- public static List<T!>! ToNonNullList<T> (params T[]! args) {
- List<T!>! res = new List<T!> (args.Length);
+ public static List<T/*!*/>/*!*/ ToNonNullList<T>(params T[] args) {
+ Contract.Requires(args != null);
+ List<T/*!*/>/*!*/ res = new List<T>(args.Length);
foreach (T t in args)
- res.Add((!)t);
+ res.Add(cce.NonNull(t));
return res;
}
- public static IDictionary<A, B>! Clone<A,B>(IDictionary<A,B>! dict) {
- IDictionary<A,B>! res = new Dictionary<A,B> (dict.Count);
- foreach (KeyValuePair<A,B> pair in dict)
+ public static IDictionary<A, B> Clone<A, B>(IDictionary<A, B> dict) {
+ Contract.Requires(dict != null);
+ Contract.Ensures(Contract.Result<IDictionary<A, B>>() != null);
+ IDictionary<A, B> res = new Dictionary<A, B>(dict.Count);
+ foreach (KeyValuePair<A, B> pair in dict)
res.Add(pair);
return res;
}
}
+ [ContractClassFor(typeof(VCExpr))]
+ public abstract class VCExprContracts : VCExpr {
+ public override Type Type {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ throw new NotImplementedException();
+ }
+
+ }
+ public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
+ throw new NotImplementedException();
+ }
+ }
+
+ [ContractClass(typeof(VCExprContracts))]
public abstract class VCExpr {
- public abstract Type! Type { get; }
+ public abstract Type Type {
+ get;
+ }
- public abstract Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg>! visitor, Arg arg);
+ public abstract Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg);
[Pure]
- public override string! ToString() {
- StringWriter! sw = new StringWriter();
- VCExprPrinter! printer = new VCExprPrinter ();
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ StringWriter sw = new StringWriter();
+ VCExprPrinter printer = new VCExprPrinter();
printer.Print(this, sw);
- return (!)sw.ToString();
+ return cce.NonNull(sw.ToString());
}
}
@@ -564,24 +744,34 @@ namespace Microsoft.Boogie.VCExprAST // Literal expressions
public class VCExprLiteral : VCExpr {
- private readonly Type! LitType;
- public override Type! Type { get { return LitType; } }
- internal VCExprLiteral(Type! type) {
+ private readonly Type LitType;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(LitType != null);
+ }
+
+ public override Type Type {
+ get {
+ return LitType;
+ }
+ }
+ internal VCExprLiteral(Type type) {
+ Contract.Requires(type != null);
this.LitType = type;
}
- public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg>! visitor, Arg arg) {
+ public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
return visitor.Visit(this, arg);
}
}
- public class VCExprIntLit : VCExprLiteral
- {
+ public class VCExprIntLit : VCExprLiteral {
public readonly BigNum Val;
- internal VCExprIntLit(BigNum val) {
- base(Type.Int);
+ internal VCExprIntLit(BigNum val) :base(Type.Int){
this.Val = val;
- }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
@@ -597,30 +787,79 @@ namespace Microsoft.Boogie.VCExprAST /////////////////////////////////////////////////////////////////////////////////
// Operator expressions with fixed arity
+ [ContractClassFor(typeof(VCExprNAry))]
+ public abstract class VCExprNAryContracts : VCExprNAry {
+ public VCExprNAryContracts()
+ : base(null) {
+ }
+ public override VCExpr this[int index] {
+ get {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ throw new NotImplementedException();
+ }
+ }
+ public override Type Type {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerable<VCExpr>>()));
+ throw new NotImplementedException();
+ }
+ }
+ }
+
+ [ContractClass(typeof(VCExprNAryContracts))]
+ public abstract class VCExprNAry : VCExpr, IEnumerable<VCExpr/*!*/> {
+ public readonly VCExprOp Op;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Op != null);
+ Contract.Invariant(cce.NonNullElements(EMPTY_TYPE_LIST));
+ Contract.Invariant(cce.NonNullElements(EMPTY_VCEXPR_LIST));
+ }
- public abstract class VCExprNAry : VCExpr, IEnumerable<VCExpr!> {
- public readonly VCExprOp! Op;
- public int Arity { get { return Op.Arity; } }
- public int TypeParamArity { get { return Op.TypeParamArity; } }
- public int Length { get { return Arity; } }
+ public int Arity {
+ get {
+ return Op.Arity;
+ }
+ }
+ public int TypeParamArity {
+ get {
+ return Op.TypeParamArity;
+ }
+ }
+ public int Length {
+ get {
+ return Arity;
+ }
+ }
// the sub-expressions of the expression
- public abstract VCExpr! this[int index] { get; }
+ public abstract VCExpr/*!*/ this[int index] {
+ get;
+ }
// the type arguments
- public abstract List<Type!>! TypeArguments { get; }
+ public abstract List<Type/*!*/>/*!*/ TypeArguments {
+ get;
+ }
- [Pure] [GlobalAccess(false)] [Escapes(true,false)]
- public IEnumerator<VCExpr!>! GetEnumerator() {
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ public IEnumerator<VCExpr/*!*/>/*!*/ GetEnumerator() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerator<VCExpr>>()));
for (int i = 0; i < Arity; ++i)
yield return this[i];
}
- [Pure] [GlobalAccess(false)] [Escapes(true,false)]
- IEnumerator! System.Collections.IEnumerable.GetEnumerator() {
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ IEnumerator System.Collections.IEnumerable.GetEnumerator() {
+ Contract.Ensures(Contract.Result<IEnumerator>() != null);
for (int i = 0; i < Arity; ++i)
yield return this[i];
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
@@ -648,7 +887,7 @@ namespace Microsoft.Boogie.VCExprAST if (!nextExprNAry0.Op.Equals(nextExprNAry1.Op))
return false;
} else {
- if (!((!)enum0.Current).Equals(enum1.Current))
+ if (!cce.NonNull(enum0.Current).Equals(enum1.Current))
return false;
}
}
@@ -661,66 +900,111 @@ namespace Microsoft.Boogie.VCExprAST 3, this);
}
- internal VCExprNAry(VCExprOp! op) {
+ internal VCExprNAry(VCExprOp op) {
+ Contract.Requires(op != null);
this.Op = op;
}
- public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg>! visitor, Arg arg) {
+ public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
return visitor.Visit(this, arg);
}
- public Result Accept<Result, Arg>(IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ public Result Accept<Result, Arg>(IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
return Op.Accept(this, visitor, arg);
}
- internal static readonly List<Type!>! EMPTY_TYPE_LIST = new List<Type!> ();
- internal static readonly List<VCExpr!>! EMPTY_VCEXPR_LIST = new List<VCExpr!> ();
+ internal static readonly List<Type/*!*/>/*!*/ EMPTY_TYPE_LIST = new List<Type/*!*/>();
+ internal static readonly List<VCExpr/*!*/>/*!*/ EMPTY_VCEXPR_LIST = new List<VCExpr/*!*/>();
+
}
// We give specialised implementations for nullary, unary and binary expressions
internal class VCExprNullary : VCExprNAry {
- private readonly Type! ExprType;
- public override Type! Type { get { return ExprType; } }
- public override VCExpr! this[int index] { get {
- assert false; // no arguments
- } }
+ private readonly Type ExprType;
+ [ContractInvariantMethod]
+ void loneinvariant() {
+ Contract.Invariant(ExprType != null);
+ }
+
+ public override Type Type {
+ get {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return ExprType;
+ }
+ }
+ public override VCExpr this[int index] {
+ get {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ Contract.Assert(false);
+ throw new cce.UnreachableException(); // no arguments
+ }
+ }
// the type arguments
- public override List<Type!>! TypeArguments { get {
- return EMPTY_TYPE_LIST;
- } }
+ public override List<Type/*!*/>/*!*/ TypeArguments {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
+ return EMPTY_TYPE_LIST;
+ }
+ }
- internal VCExprNullary(VCExprOp! op)
- requires op.Arity == 0 && op.TypeParamArity == 0; {
- base(op);
+ internal VCExprNullary(VCExprOp op):base(op) {
+ Contract.Requires(op != null);
+ Contract.Requires(op.Arity == 0 && op.TypeParamArity == 0);
this.ExprType = op.InferType(EMPTY_VCEXPR_LIST, EMPTY_TYPE_LIST);
}
}
internal class VCExprUnary : VCExprNAry {
- private readonly VCExpr! Argument;
- private readonly Type! ExprType;
- public override Type! Type { get { return ExprType; } }
- public override VCExpr! this[int index] { get {
- assume index == 0;
- return Argument;
- } }
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Argument != null);
+ Contract.Invariant(ExprType != null);
+
+ }
+
+ private readonly VCExpr/*!*/ Argument;
+ private readonly Type/*!*/ ExprType;
+ public override Type/*!*/ Type {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return ExprType;
+ }
+ }
+ public override VCExpr/*!*/ this[int index] {
+ get {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ Contract.Assume(index == 0);
+ return Argument;
+ }
+ }
// the type arguments
- public override List<Type!>! TypeArguments { get {
- return EMPTY_TYPE_LIST;
- } }
+ public override List<Type/*!*/>/*!*/ TypeArguments {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
+ return EMPTY_TYPE_LIST;
+ }
+ }
- internal VCExprUnary(VCExprOp! op, List<VCExpr!>! arguments)
- requires op.Arity == 1 && op.TypeParamArity == 0 && arguments.Count == 1; {
- base(op);
+ internal VCExprUnary(VCExprOp op, List<VCExpr> arguments) :base(op){
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(arguments));
+ Contract.Requires(op.Arity == 1 && op.TypeParamArity == 0 && arguments.Count == 1);
+
this.Argument = arguments[0];
this.ExprType =
op.InferType(arguments, EMPTY_TYPE_LIST);
}
-
- internal VCExprUnary(VCExprOp! op, VCExpr! argument)
- requires op.Arity == 1 && op.TypeParamArity == 0; {
- base(op);
+
+ internal VCExprUnary(VCExprOp op, VCExpr argument) :base(op){
+ Contract.Requires(argument != null);
+ Contract.Requires(op != null);
+ Contract.Requires(op.Arity == 1 && op.TypeParamArity == 0);
+
this.Argument = argument;
// PR: could be optimised so that the argument does
// not have to be boxed in an array each time
@@ -730,34 +1014,62 @@ namespace Microsoft.Boogie.VCExprAST }
internal class VCExprBinary : VCExprNAry {
- private readonly VCExpr! Argument0;
- private readonly VCExpr! Argument1;
- private readonly Type! ExprType;
- public override Type! Type { get { return ExprType; } }
- public override VCExpr! this[int index] { get {
- switch (index) {
- case 0: return Argument0;
- case 1: return Argument1;
- default: assert false;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Argument0 != null);
+ Contract.Invariant(Argument1 != null);
+ Contract.Invariant(ExprType != null);
+ }
+
+ private readonly VCExpr Argument0;
+ private readonly VCExpr Argument1;
+ private readonly Type ExprType;
+ public override Type Type {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return ExprType;
+ }
+ }
+ public override VCExpr this[int index] {
+ get {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ switch (index) {
+ case 0:
+ return Argument0;
+ case 1:
+ return Argument1;
+ default: {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ }
}
- } }
+ }
// the type arguments
- public override List<Type!>! TypeArguments { get {
- return EMPTY_TYPE_LIST;
- } }
+ public override List<Type/*!*/>/*!*/ TypeArguments {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
+ return EMPTY_TYPE_LIST;
+ }
+ }
- internal VCExprBinary(VCExprOp! op, List<VCExpr!>! arguments)
- requires op.Arity == 2 && op.TypeParamArity == 0 && arguments.Count == 2; {
- base(op);
+ internal VCExprBinary(VCExprOp op, List<VCExpr> arguments) :base(op){
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(arguments));
+ Contract.Requires(op.Arity == 2 && op.TypeParamArity == 0 && arguments.Count == 2);
+
this.Argument0 = arguments[0];
this.Argument1 = arguments[1];
this.ExprType = op.InferType(arguments, EMPTY_TYPE_LIST);
}
- internal VCExprBinary(VCExprOp! op, VCExpr! argument0, VCExpr! argument1)
- requires op.Arity == 2 && op.TypeParamArity == 0; {
- base(op);
+ internal VCExprBinary(VCExprOp op, VCExpr argument0, VCExpr argument1) :base(op){
+ Contract.Requires(argument1 != null);
+ Contract.Requires(argument0 != null);
+ Contract.Requires(op != null);
+ Contract.Requires(op.Arity == 2 && op.TypeParamArity == 0);
this.Argument0 = argument0;
this.Argument1 = argument1;
// PR: could be optimised so that the arguments do
@@ -769,30 +1081,55 @@ namespace Microsoft.Boogie.VCExprAST }
internal class VCExprMultiAry : VCExprNAry {
- private readonly List<VCExpr!>! Arguments;
- private readonly List<Type!>! TypeArgumentsAttr;
+ private readonly List<VCExpr/*!*/>/*!*/ Arguments;
+ private readonly List<Type/*!*/>/*!*/ TypeArgumentsAttr;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(Arguments));
+ Contract.Invariant(cce.NonNullElements(TypeArgumentsAttr));
+ Contract.Invariant(ExprType != null);
+ }
+
+
+ private readonly Type/*!*/ ExprType;
+ public override Type/*!*/ Type {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return ExprType;
+ }
+ }
+ public override VCExpr/*!*/ this[int index] {
+ get {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
- private readonly Type! ExprType;
- public override Type! Type { get { return ExprType; } }
- public override VCExpr! this[int index] { get {
- assume index >= 0 && index < Arity;
- return (!)Arguments[index];
- } }
+ Contract.Assume(index >= 0 && index < Arity);
+ return cce.NonNull(Arguments)[index];
+ }
+ }
// the type arguments
- public override List<Type!>! TypeArguments { get {
- return TypeArgumentsAttr;
- } }
-
- internal VCExprMultiAry(VCExprOp! op, List<VCExpr!>! arguments) {
- this(op, arguments, EMPTY_TYPE_LIST);
- }
- internal VCExprMultiAry(VCExprOp! op, List<VCExpr!>! arguments, List<Type!>! typeArguments)
- requires (arguments.Count > 2 || typeArguments.Count > 0);
- requires op.Arity == arguments.Count;
- requires op.TypeParamArity == typeArguments.Count;
- {
- base(op);
+ public override List<Type/*!*/>/*!*/ TypeArguments {
+ get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
+ return TypeArgumentsAttr;
+ }
+ }
+
+ internal VCExprMultiAry(VCExprOp op, List<VCExpr> arguments) :base(op){
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(arguments));
+ //this(op, arguments, EMPTY_TYPE_LIST);
+ this.Arguments = arguments;
+ this.TypeArgumentsAttr = EMPTY_TYPE_LIST;
+ this.ExprType = op.InferType(arguments, TypeArgumentsAttr);
+ }
+ internal VCExprMultiAry(VCExprOp op, List<VCExpr> arguments, List<Type/*!*/>/*!*/ typeArguments):base(op){
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(typeArguments));
+ Contract.Requires(cce.NonNullElements(arguments));
+ Contract.Requires(arguments.Count > 2 || typeArguments.Count > 0);
+ Contract.Requires(op.Arity == arguments.Count);
+ Contract.Requires(op.TypeParamArity == typeArguments.Count);
this.Arguments = arguments;
this.TypeArgumentsAttr = typeArguments;
this.ExprType = op.InferType(arguments, typeArguments);
@@ -801,86 +1138,119 @@ namespace Microsoft.Boogie.VCExprAST /////////////////////////////////////////////////////////////////////////////////
// The various operators available
-
+ [ContractClass(typeof(VCExprOpContracts))]
public abstract class VCExprOp {
// the number of value parameters
- public abstract int Arity { get; }
+ public abstract int Arity {
+ get;
+ }
// the number of type parameters
- public abstract int TypeParamArity { get; }
+ public abstract int TypeParamArity {
+ get;
+ }
- public abstract Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs);
+ public abstract Type/*!*/ InferType(List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs);
- public virtual Result Accept<Result, Arg>
- (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ public virtual Result Accept<Result, Arg>(VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
+ Contract.Requires(expr != null);
VCExpressionGenerator.SingletonOp op;
if (VCExpressionGenerator.SingletonOpDict.TryGetValue(this, out op)) {
- switch(op) {
- case VCExpressionGenerator.SingletonOp.NotOp:
- return visitor.VisitNotOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.EqOp:
- return visitor.VisitEqOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.NeqOp:
- return visitor.VisitNeqOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.AndOp:
- return visitor.VisitAndOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.OrOp:
- return visitor.VisitOrOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.ImpliesOp:
- return visitor.VisitImpliesOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.AddOp:
- return visitor.VisitAddOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.SubOp:
- return visitor.VisitSubOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.MulOp:
- return visitor.VisitMulOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.DivOp:
- return visitor.VisitDivOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.ModOp:
- return visitor.VisitModOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.LtOp:
- return visitor.VisitLtOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.LeOp:
- return visitor.VisitLeOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.GtOp:
- return visitor.VisitGtOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.GeOp:
- return visitor.VisitGeOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.SubtypeOp:
- return visitor.VisitSubtypeOp(expr, arg);
- case VCExpressionGenerator.SingletonOp.Subtype3Op:
- return visitor.VisitSubtype3Op(expr, arg);
- case VCExpressionGenerator.SingletonOp.BvConcatOp:
- return visitor.VisitBvConcatOp(expr, arg);
- default:
- assert false;
+ switch (op) {
+ case VCExpressionGenerator.SingletonOp.NotOp:
+ return visitor.VisitNotOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.EqOp:
+ return visitor.VisitEqOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.NeqOp:
+ return visitor.VisitNeqOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.AndOp:
+ return visitor.VisitAndOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.OrOp:
+ return visitor.VisitOrOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.ImpliesOp:
+ return visitor.VisitImpliesOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.AddOp:
+ return visitor.VisitAddOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.SubOp:
+ return visitor.VisitSubOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.MulOp:
+ return visitor.VisitMulOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.DivOp:
+ return visitor.VisitDivOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.ModOp:
+ return visitor.VisitModOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.LtOp:
+ return visitor.VisitLtOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.LeOp:
+ return visitor.VisitLeOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.GtOp:
+ return visitor.VisitGtOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.GeOp:
+ return visitor.VisitGeOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.SubtypeOp:
+ return visitor.VisitSubtypeOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.Subtype3Op:
+ return visitor.VisitSubtype3Op(expr, arg);
+ case VCExpressionGenerator.SingletonOp.BvConcatOp:
+ return visitor.VisitBvConcatOp(expr, arg);
+ default:
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
}
} else {
- assert false;
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
}
}
}
+ [ContractClassFor(typeof(VCExprOp))]
+ abstract class VCExprOpContracts : VCExprOp {
+ public override Type InferType(List<VCExpr> args, List<Type> typeArgs) {
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ throw new NotImplementedException();
+ }
+ }
public class VCExprNAryOp : VCExprOp {
- private readonly Type! OpType;
+ private readonly Type OpType;
private readonly int OpArity;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(OpType != null);
+ }
- public override int Arity { get { return OpArity; } }
- public override int TypeParamArity { get { return 0; } }
- public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ public override int Arity {
+ get {
+ return OpArity;
+ }
+ }
+ public override int TypeParamArity {
+ get {
+ return 0;
+ }
+ }
+ public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<Type>() != null);
return OpType;
}
- internal VCExprNAryOp(int arity, Type! type) {
+ internal VCExprNAryOp(int arity, Type type) {
+ Contract.Requires(type != null);
this.OpArity = arity;
this.OpType = type;
}
}
public class VCExprDistinctOp : VCExprNAryOp {
- internal VCExprDistinctOp(int arity) {
- base(arity, Type.Bool);
+ internal VCExprDistinctOp(int arity) :base(arity, Type.Bool){
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
@@ -893,27 +1263,45 @@ namespace Microsoft.Boogie.VCExprAST return Arity * 917632481;
}
public override Result Accept<Result, Arg>
- (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
+ Contract.Requires(expr != null);
return visitor.VisitDistinctOp(expr, arg);
}
}
public class VCExprLabelOp : VCExprOp {
- public override int Arity { get { return 1; } }
- public override int TypeParamArity { get { return 0; } }
- public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ public override int Arity {
+ get {
+ return 1;
+ }
+ }
+ public override int TypeParamArity {
+ get {
+ return 0;
+ }
+ }
+ public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<Type>() != null);
return args[0].Type;
}
-
+
public readonly bool pos;
- public readonly string! label;
+ public readonly string label;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(label != null);
+ }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
if (that is VCExprLabelOp) {
- VCExprLabelOp! thatOp = (VCExprLabelOp)that;
+ VCExprLabelOp/*!*/ thatOp = (VCExprLabelOp)that;
return this.pos == thatOp.pos && this.label.Equals(thatOp.label);
}
return false;
@@ -923,12 +1311,15 @@ namespace Microsoft.Boogie.VCExprAST return (pos ? 9817231 : 7198639) + label.GetHashCode();
}
- internal VCExprLabelOp(bool pos, string! l) {
+ internal VCExprLabelOp(bool pos, string l) {
+ Contract.Requires(l != null);
this.pos = pos;
this.label = pos ? "+" + l : "@" + l;
}
public override Result Accept<Result, Arg>
- (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
+ Contract.Requires(expr != null);
return visitor.VisitLabelOp(expr, arg);
}
}
@@ -936,19 +1327,31 @@ namespace Microsoft.Boogie.VCExprAST public class VCExprSelectOp : VCExprOp {
private readonly int MapArity;
private readonly int MapTypeParamArity;
- public override int Arity { get { return MapArity + 1; } }
- public override int TypeParamArity { get { return MapTypeParamArity; } }
+ public override int Arity {
+ get {
+ return MapArity + 1;
+ }
+ }
+ public override int TypeParamArity {
+ get {
+ return MapTypeParamArity;
+ }
+ }
- public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
- MapType! mapType = args[0].Type.AsMap;
- assert TypeParamArity == mapType.TypeParameters.Length;
- IDictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!> ();
+ public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs){
+Contract.Requires(cce.NonNullElements(typeArgs));
+Contract.Requires(cce.NonNullElements(args));
+Contract.Ensures(Contract.Result<Type>() != null);
+ MapType/*!*/ mapType = args[0].Type.AsMap;
+ Contract.Assert(TypeParamArity == mapType.TypeParameters.Length);
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>();
for (int i = 0; i < TypeParamArity; ++i)
subst.Add(mapType.TypeParameters[i], typeArgs[i]);
return mapType.Result.Substitute(subst);
}
-
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
@@ -962,14 +1365,15 @@ namespace Microsoft.Boogie.VCExprAST return Arity * 1212481 + TypeParamArity * 298741;
}
- internal VCExprSelectOp(int arity, int typeParamArity)
- requires 0 <= arity && 0 <= typeParamArity;
- {
+ internal VCExprSelectOp(int arity, int typeParamArity) {
+ Contract.Requires(0 <= arity && 0 <= typeParamArity);
this.MapArity = arity;
this.MapTypeParamArity = typeParamArity;
}
public override Result Accept<Result, Arg>
- (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
+ Contract.Requires(expr != null);
return visitor.VisitSelectOp(expr, arg);
}
}
@@ -977,16 +1381,28 @@ namespace Microsoft.Boogie.VCExprAST public class VCExprStoreOp : VCExprOp {
private readonly int MapArity;
private readonly int MapTypeParamArity;
- public override int Arity { get { return MapArity + 2; } }
+ public override int Arity {
+ get {
+ return MapArity + 2;
+ }
+ }
// stores never need explicit type parameters, because also the
// rhs is a value argument
- public override int TypeParamArity { get { return MapTypeParamArity; } }
+ public override int TypeParamArity {
+ get {
+ return MapTypeParamArity;
+ }
+ }
- public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<Type>() != null);
return args[0].Type;
}
-
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
@@ -999,26 +1415,39 @@ namespace Microsoft.Boogie.VCExprAST return Arity * 91361821;
}
- internal VCExprStoreOp(int arity, int typeParamArity)
- requires 0 <= arity && 0 <= typeParamArity;
- {
+ internal VCExprStoreOp(int arity, int typeParamArity) {
+ Contract.Requires(0 <= arity && 0 <= typeParamArity);
this.MapArity = arity;
this.MapTypeParamArity = typeParamArity;
}
public override Result Accept<Result, Arg>
- (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
+ Contract.Requires(expr != null);
return visitor.VisitStoreOp(expr, arg);
}
}
public class VCExprIfThenElseOp : VCExprOp {
- public override int Arity { get { return 3; } }
- public override int TypeParamArity { get { return 0; } }
- public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ public override int Arity {
+ get {
+ return 3;
+ }
+ }
+ public override int TypeParamArity {
+ get {
+ return 0;
+ }
+ }
+ public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<Type>() != null);
return args[1].Type;
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
@@ -1034,16 +1463,27 @@ namespace Microsoft.Boogie.VCExprAST internal VCExprIfThenElseOp() {
}
public override Result Accept<Result, Arg>
- (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
+ Contract.Requires(expr != null);
return visitor.VisitIfThenElseOp(expr, arg);
}
}
-
+
public class VCExprCustomOp : VCExprOp {
- public readonly string! Name;
+ public readonly string/*!*/ Name;
int arity;
- public readonly Type! Type;
- public VCExprCustomOp(string! name, int arity, Type! type) {
+ public readonly Type/*!*/ Type;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(Name!=null);
+ Contract.Invariant(Type != null);
+}
+
+ public VCExprCustomOp(string/*!*/ name, int arity, Type/*!*/ type) {
+ Contract.Requires(name != null);
+ Contract.Requires(type != null);
this.Name = name;
this.arity = arity;
this.Type = type;
@@ -1059,9 +1499,13 @@ namespace Microsoft.Boogie.VCExprAST }
public override int Arity { get { return arity; } }
public override int TypeParamArity { get { return 0; } }
- public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) { return Type; }
+ public override Type/*!*/ InferType(List<VCExpr/*!*/>/*!*/ args, List<Type/*!*/>/*!*/ typeArgs) {Contract.Requires((cce.NonNullElements(args)));
+Contract.Requires((cce.NonNullElements(typeArgs)));
+Contract.Ensures(Contract.Result<Type>() != null); return Type; }
public override Result Accept<Result, Arg>
- (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ (VCExprNAry/*!*/ expr, IVCExprOpVisitor<Result, Arg>/*!*/ visitor, Arg arg) {
+ Contract.Requires(expr != null);
+ Contract.Requires(visitor != null);
return visitor.VisitCustomOp(expr, arg);
}
}
@@ -1072,13 +1516,25 @@ namespace Microsoft.Boogie.VCExprAST public class VCExprBvOp : VCExprOp {
public readonly int Bits;
- public override int Arity { get { return 1; } }
- public override int TypeParamArity { get { return 0; } }
- public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ public override int Arity {
+ get {
+ return 1;
+ }
+ }
+ public override int TypeParamArity {
+ get {
+ return 0;
+ }
+ }
+ public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<Type>() != null);
return Type.GetBvType(Bits);
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
@@ -1095,7 +1551,9 @@ namespace Microsoft.Boogie.VCExprAST this.Bits = bits;
}
public override Result Accept<Result, Arg>
- (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
+ Contract.Requires(expr != null);
return visitor.VisitBvOp(expr, arg);
}
}
@@ -1105,18 +1563,30 @@ namespace Microsoft.Boogie.VCExprAST public readonly int End;
public readonly int Total; // the number of bits from which the End-Start bits are extracted
- public override int Arity { get { return 1; } }
- public override int TypeParamArity { get { return 0; } }
- public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+ public override int Arity {
+ get {
+ return 1;
+ }
+ }
+ public override int TypeParamArity {
+ get {
+ return 0;
+ }
+ }
+ public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<Type>() != null);
return Type.GetBvType(End - Start);
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
if (that is VCExprBvExtractOp) {
- VCExprBvExtractOp! thatExtract = (VCExprBvExtractOp)that;
+ VCExprBvExtractOp/*!*/ thatExtract = (VCExprBvExtractOp)that;
return this.Start == thatExtract.Start && this.End == thatExtract.End && this.Total == thatExtract.Total;
}
return false;
@@ -1126,15 +1596,16 @@ namespace Microsoft.Boogie.VCExprAST return Start * 81912 + End * 978132 + Total * 571289;
}
- internal VCExprBvExtractOp(int start, int end, int total)
- requires 0 <= start && start <= end && end <= total;
- {
+ internal VCExprBvExtractOp(int start, int end, int total) {
+ Contract.Requires(0 <= start && start <= end && end <= total);
this.Start = start;
this.End = end;
this.Total = total;
}
public override Result Accept<Result, Arg>
- (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
+ Contract.Requires(expr != null);
return visitor.VisitBvExtractOp(expr, arg);
}
}
@@ -1142,14 +1613,26 @@ namespace Microsoft.Boogie.VCExprAST public class VCExprBvConcatOp : VCExprOp {
public readonly int LeftSize;
public readonly int RightSize;
-
- public override int Arity { get { return 2; } }
- public override int TypeParamArity { get { return 0; } }
- public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
+
+ public override int Arity {
+ get {
+ return 2;
+ }
+ }
+ public override int TypeParamArity {
+ get {
+ return 0;
+ }
+ }
+ public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
+ Contract.Requires(cce.NonNullElements(typeArgs));
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<Type>() != null);
return Type.GetBvType(args[0].Type.BvBits + args[1].Type.BvBits);
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
@@ -1164,14 +1647,15 @@ namespace Microsoft.Boogie.VCExprAST return LeftSize * 81912 + RightSize * 978132;
}
- internal VCExprBvConcatOp(int leftSize, int rightSize)
- requires 0 <= leftSize && 0 <= rightSize;
- {
+ internal VCExprBvConcatOp(int leftSize, int rightSize) {
+ Contract.Requires(0 <= leftSize && 0 <= rightSize);
this.LeftSize = leftSize;
this.RightSize = rightSize;
}
public override Result Accept<Result, Arg>
- (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
+ Contract.Requires(expr != null);
return visitor.VisitBvConcatOp(expr, arg);
}
}
@@ -1180,21 +1664,38 @@ namespace Microsoft.Boogie.VCExprAST // References to user-defined Boogie functions
public class VCExprBoogieFunctionOp : VCExprOp {
- public readonly Function! Func;
+ public readonly Function Func;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Func != null);
+ }
+
- public override int Arity { get { return Func.InParams.Length; } }
- public override int TypeParamArity { get { return Func.TypeParameters.Length; } }
- public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) {
- assert TypeParamArity == Func.TypeParameters.Length;
+ public override int Arity {
+ get {
+ return Func.InParams.Length;
+ }
+ }
+ public override int TypeParamArity {
+ get {
+ return Func.TypeParameters.Length;
+ }
+ }
+ public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs){
+Contract.Requires(cce.NonNullElements(typeArgs));
+Contract.Requires(cce.NonNullElements(args));
+Contract.Ensures(Contract.Result<Type>() != null);
+ Contract.Assert(TypeParamArity == Func.TypeParameters.Length);
if (TypeParamArity == 0)
- return ((!)Func.OutParams[0]).TypedIdent.Type;
- IDictionary<TypeVariable!, Type!>! subst = new Dictionary<TypeVariable!, Type!> (TypeParamArity);
+ return cce.NonNull(Func.OutParams[0]).TypedIdent.Type;
+ IDictionary<TypeVariable/*!*/, Type/*!*/>/*!*/ subst = new Dictionary<TypeVariable/*!*/, Type/*!*/>(TypeParamArity);
for (int i = 0; i < TypeParamArity; ++i)
subst.Add(Func.TypeParameters[i], typeArgs[i]);
- return ((!)Func.OutParams[0]).TypedIdent.Type.Substitute(subst);
+ return cce.NonNull(Func.OutParams[0]).TypedIdent.Type.Substitute(subst);
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
@@ -1209,11 +1710,14 @@ namespace Microsoft.Boogie.VCExprAST // we require that the result type of the expression is specified, because we
// do not want to perform full type inference at this point
- internal VCExprBoogieFunctionOp(Function! func) {
+ internal VCExprBoogieFunctionOp(Function func) {
+ Contract.Requires(func != null);
this.Func = func;
}
public override Result Accept<Result, Arg>
- (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ (VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
+ Contract.Requires(expr != null);
return visitor.VisitBoogieFunctionOp(expr, arg);
}
}
@@ -1225,30 +1729,58 @@ namespace Microsoft.Boogie.VCExprAST public class VCExprVar : VCExpr {
// the name of the variable. Note that the name is not used for comparison,
// i.e., there can be two distinct variables with the same name
- public readonly string! Name;
- private readonly Type! VarType;
- public override Type! Type { get { return VarType; } }
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Name != null);
+ Contract.Invariant(VarType != null);
+ }
+
+ public readonly string/*!*/ Name;
+ private readonly Type/*!*/ VarType;
+ public override Type/*!*/ Type {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return VarType;
+ }
+ }
- internal VCExprVar(string! name, Type! type) {
+ internal VCExprVar(string name, Type type) {
+ Contract.Requires(type != null);
+ Contract.Requires(name != null);
this.Name = name;
this.VarType = type;
}
- public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg>! visitor, Arg arg) {
+ public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
return visitor.Visit(this, arg);
}
}
public abstract class VCExprBinder : VCExpr {
- public readonly VCExpr! Body;
- public readonly List<TypeVariable!>! TypeParameters;
- public readonly List<VCExprVar!>! BoundVars;
-
- public override Type! Type { get { return Body.Type; } }
-
- internal VCExprBinder(List<TypeVariable!>! typeParams,
- List<VCExprVar!>! boundVars,
- VCExpr! body)
- requires boundVars.Count + typeParams.Count > 0; { // only nontrivial binders ...
+ public readonly VCExpr/*!*/ Body;
+ public readonly List<TypeVariable/*!*/>/*!*/ TypeParameters;
+ public readonly List<VCExprVar/*!*/>/*!*/ BoundVars;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Body != null);
+ Contract.Invariant(cce.NonNullElements(TypeParameters));
+ Contract.Invariant(cce.NonNullElements(BoundVars));
+ }
+
+
+ public override Type/*!*/ Type {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ return Body.Type;
+ }
+ }
+
+ internal VCExprBinder(List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ boundVars, VCExpr body) {
+ Contract.Requires(body != null);
+ Contract.Requires(cce.NonNullElements(boundVars));
+ Contract.Requires(cce.NonNullElements(typeParams));
+ Contract.Requires(boundVars.Count + typeParams.Count > 0); // only nontrivial binders ...
this.TypeParameters = typeParams;
this.BoundVars = boundVars;
this.Body = body;
@@ -1257,14 +1789,20 @@ namespace Microsoft.Boogie.VCExprAST public class VCTrigger {
public readonly bool Pos;
- public readonly List<VCExpr!>! Exprs;
+ public readonly List<VCExpr/*!*/>/*!*/ Exprs;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Exprs != null);
+ }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
if (that is VCTrigger) {
- VCTrigger! thatTrigger = (VCTrigger)that;
+ VCTrigger/*!*/ thatTrigger = (VCTrigger)that;
return this.Pos == thatTrigger.Pos &&
HelperFuns.SameElements(this.Exprs, thatTrigger.Exprs);
}
@@ -1276,7 +1814,8 @@ namespace Microsoft.Boogie.VCExprAST HelperFuns.PolyHash(123, 7, this.Exprs);
}
- public VCTrigger(bool pos, List<VCExpr!>! exprs) {
+ public VCTrigger(bool pos, List<VCExpr> exprs) {
+ Contract.Requires(cce.NonNullElements(exprs));
this.Pos = pos;
this.Exprs = exprs;
}
@@ -1296,21 +1835,31 @@ namespace Microsoft.Boogie.VCExprAST }
}
- public enum Quantifier { ALL, EX };
+ public enum Quantifier {
+ ALL,
+ EX
+ };
public class VCExprQuantifier : VCExprBinder {
public readonly Quantifier Quan;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Infos != null);
+ Contract.Invariant(cce.NonNullElements(Triggers));
+ }
- public readonly List<VCTrigger!>! Triggers;
- public readonly VCQuantifierInfos! Infos;
+
+ public readonly List<VCTrigger/*!*/>/*!*/ Triggers;
+ public readonly VCQuantifierInfos Infos;
// Equality is /not/ modulo bound renaming at this point
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
if (that is VCExprQuantifier) {
- VCExprQuantifier! thatQuan = (VCExprQuantifier)that;
+ VCExprQuantifier/*!*/ thatQuan = (VCExprQuantifier)that;
return this.Quan == thatQuan.Quan &&
HelperFuns.SameElements(this.Triggers, thatQuan.Triggers) &&
HelperFuns.SameElements(this.TypeParameters, thatQuan.TypeParameters) &&
@@ -1327,18 +1876,19 @@ namespace Microsoft.Boogie.VCExprAST HelperFuns.PolyHash(123, 11, Triggers);
}
- internal VCExprQuantifier(Quantifier kind,
- List<TypeVariable!>! typeParams,
- List<VCExprVar!>! boundVars,
- List<VCTrigger!>! triggers,
- VCQuantifierInfos! infos,
- VCExpr! body) {
- base(typeParams, boundVars, body);
+ internal VCExprQuantifier(Quantifier kind, List<TypeVariable/*!*/>/*!*/ typeParams, List<VCExprVar/*!*/>/*!*/ boundVars, List<VCTrigger/*!*/>/*!*/ triggers, VCQuantifierInfos infos, VCExpr body) :base(typeParams, boundVars, body){
+ Contract.Requires(body != null);
+ Contract.Requires(infos != null);
+ Contract.Requires(cce.NonNullElements(triggers));
+ Contract.Requires(cce.NonNullElements(boundVars));
+ Contract.Requires(cce.NonNullElements(typeParams));
+
this.Quan = kind;
this.Triggers = triggers;
this.Infos = infos;
}
- public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg>! visitor, Arg arg) {
+ public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
return visitor.Visit(this, arg);
}
}
@@ -1347,15 +1897,22 @@ namespace Microsoft.Boogie.VCExprAST // Let-Bindings
public class VCExprLetBinding {
- public readonly VCExprVar! V;
- public readonly VCExpr! E;
+ public readonly VCExprVar V;
+ public readonly VCExpr E;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(V != null);
+ Contract.Invariant(E != null);
+ }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
if (that is VCExprLetBinding) {
- VCExprLetBinding! thatB = (VCExprLetBinding)that;
+ VCExprLetBinding/*!*/ thatB = (VCExprLetBinding)that;
return this.V.Equals(thatB.V) && this.E.Equals(thatB.E);
}
return false;
@@ -1364,28 +1921,44 @@ namespace Microsoft.Boogie.VCExprAST public override int GetHashCode() {
return V.GetHashCode() * 71261 + E.GetHashCode();
}
-
- internal VCExprLetBinding(VCExprVar! v, VCExpr! e) {
+
+ internal VCExprLetBinding(VCExprVar v, VCExpr e) {
+ Contract.Requires(e != null);
+ Contract.Requires(v != null);
this.V = v;
this.E = e;
- assert v.Type.Equals(e.Type);
+ Contract.Assert(v.Type.Equals(e.Type));
}
}
- public class VCExprLet : VCExprBinder, IEnumerable<VCExprLetBinding!> {
- private readonly List<VCExprLetBinding!>! Bindings;
+ public class VCExprLet : VCExprBinder, IEnumerable<VCExprLetBinding/*!*/> {
+ private readonly List<VCExprLetBinding/*!*/>/*!*/ Bindings;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(cce.NonNullElements(Bindings));
- public int Length { get { return Bindings.Count; } }
- public VCExprLetBinding! this[int index] { get {
- return Bindings[index];
- } }
+ }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+
+ public int Length {
+ get {
+ return Bindings.Count;
+ }
+ }
+ public VCExprLetBinding this[int index] {
+ get {
+ Contract.Ensures(Contract.Result<VCExprLetBinding>() != null);
+ return Bindings[index];
+ }
+ }
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
if (that is VCExprLet) {
- VCExprLet! thatLet = (VCExprLet)that;
+ VCExprLet/*!*/ thatLet = (VCExprLet)that;
return this.Body.Equals(thatLet.Body) &&
HelperFuns.SameElements(this, (VCExprLet)that);
}
@@ -1396,28 +1969,37 @@ namespace Microsoft.Boogie.VCExprAST return HelperFuns.PolyHash(Body.GetHashCode(), 9, Bindings);
}
- [Pure] [GlobalAccess(false)] [Escapes(true,false)]
- public IEnumerator<VCExprLetBinding!>! GetEnumerator() {
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ public IEnumerator<VCExprLetBinding/*!*/>/*!*/ GetEnumerator() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<IEnumerator<VCExprLetBinding>>()));
return Bindings.GetEnumerator();
}
- [Pure] [GlobalAccess(false)] [Escapes(true,false)]
- IEnumerator! System.Collections.IEnumerable.GetEnumerator() {
+ [Pure]
+ [GlobalAccess(false)]
+ [Escapes(true, false)]
+ IEnumerator System.Collections.IEnumerable.GetEnumerator() {
+ Contract.Ensures(Contract.Result<IEnumerator>() != null);
return Bindings.GetEnumerator();
}
- private static List<VCExprVar!>! toSeq(List<VCExprLetBinding!>! bindings) {
- List<VCExprVar!>! res = new List<VCExprVar!> ();
- foreach (VCExprLetBinding! b in bindings)
+ private static List<VCExprVar/*!*/>/*!*/ toSeq(List<VCExprLetBinding/*!*/>/*!*/ bindings){
+Contract.Requires(cce.NonNullElements(bindings));
+Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
+ List<VCExprVar> res = new List<VCExprVar> ();
+ foreach (VCExprLetBinding/*!*/ b in bindings)
res.Add(b.V);
return res;
}
- internal VCExprLet(List<VCExprLetBinding!>! bindings,
- VCExpr! body) {
- base(new List<TypeVariable!> (), toSeq(bindings), body);
+ internal VCExprLet(List<VCExprLetBinding/*!*/>/*!*/ bindings, VCExpr/*!*/ body) :base(new List<TypeVariable/*!*/>(), toSeq(bindings), body){
+ Contract.Requires(cce.NonNullElements(bindings));
+ Contract.Requires(body != null);
this.Bindings = bindings;
}
- public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg>! visitor, Arg arg) {
+ public override Result Accept<Result, Arg>(IVCExprVisitor<Result, Arg> visitor, Arg arg) {
+ Contract.Requires(visitor != null);
return visitor.Visit(this, arg);
}
}
|