diff options
| author |  tabarbe <unknown> | 2010-08-20 22:32:24 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-20 22:32:24 +0000 |
| commit | 72b39a6962d7f6c7ca1aab9919791238c7baba3f (patch) | |
| tree | 75bb9c1b956d1b368f4cf2983a20a913211dd350 /Source/Core/AbsyExpr.cs | |
| parent | 96d9624e9e22dbe9090e0bd7d538cafbf0a16463 (diff) | |
Boogie: Committing changed source files
Diffstat (limited to 'Source/Core/AbsyExpr.cs')
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 3080 |
1 files changed, 1922 insertions, 1158 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 250820ed..f5771f7f 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -7,17 +7,17 @@ // BoogiePL - Absy.cs
//---------------------------------------------------------------------------------------------
-namespace Microsoft.Boogie
-{
+namespace Microsoft.Boogie {
using System;
using System.Collections;
using System.Diagnostics;
using System.Collections.Generic;
using Microsoft.Boogie.AbstractInterpretation;
using AI = Microsoft.AbstractInterpretationFramework;
- using Microsoft.Contracts;
+ using Microsoft.AbstractInterpretationFramework;//DANGER: Added?
+ using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
-
+
//---------------------------------------------------------------------
// Expressions
@@ -28,26 +28,25 @@ namespace Microsoft.Boogie //---------------------------------------------------------------------
- public abstract class Expr : Absy
- {
- public Expr(IToken! tok)
- : base(tok)
- {
+ [ContractClass(typeof(ExprContracts))]
+ public abstract class Expr : Absy {
+ public Expr(IToken/*!*/ tok)
+ : base(tok) {
+ Contract.Requires(tok != null);
}
- public void Emit (TokenTextWriter! stream)
- {
+ public void Emit(TokenTextWriter stream) {
+ Contract.Requires(stream != null);
Emit(stream, 0, false);
}
- public abstract void Emit (TokenTextWriter! wr, int contextBindingStrength, bool fragileContext);
-
+ public abstract void Emit(TokenTextWriter/*!*/ wr, int contextBindingStrength, bool fragileContext);
+
[Pure]
- public override string! ToString ()
- {
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
System.IO.StringWriter buffer = new System.IO.StringWriter();
- using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false))
- {
+ using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
this.Emit(stream, 0, false);
}
return buffer.ToString();
@@ -56,7 +55,7 @@ namespace Microsoft.Boogie /// <summary>
/// Add to "freeVars" the free variables in the expression.
/// </summary>
- public abstract void ComputeFreeVariables(Set /*Variable*/! freeVars);
+ public abstract void ComputeFreeVariables(Set /*Variable*//*!*/ freeVars);
/// <summary>
/// Filled in by the Typecheck method. A value of "null" means a succeeding
@@ -66,138 +65,285 @@ namespace Microsoft.Boogie /// </summary>
public Type Type;
- public override void Typecheck (TypecheckingContext! tc)
- ensures Type != null;
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ Contract.Ensures(Type != null);
// This body is added only because C# insists on it. It should really be left out, as if TypeCheck still were abstract.
// The reason for mentioning the method here at all is to give TypeCheck a postcondition for all expressions.
- assert false;
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
}
/// <summary>
/// Returns the type of the expression, supposing that all its subexpressions are well typed.
/// </summary>
- public abstract Type! ShallowType { get; }
+ public abstract Type/*!*/ ShallowType {
+ get;
+ }
// Handy syntactic sugar follows:
- public static NAryExpr! Unary (IToken! x, UnaryOperator.Opcode op, Expr! e1)
- {
+ public static NAryExpr Unary(IToken x, UnaryOperator.Opcode op, Expr e1) {
+ Contract.Requires(e1 != null);
+ Contract.Requires(x != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
return new NAryExpr(x, new UnaryOperator(x, op), new ExprSeq(e1));
}
- public static NAryExpr! Binary (IToken! x, BinaryOperator.Opcode op, Expr! e0, Expr! e1)
- {
+ public static NAryExpr Binary(IToken x, BinaryOperator.Opcode op, Expr e0, Expr e1) {
+ Contract.Requires(e1 != null);
+ Contract.Requires(e0 != null);
+ Contract.Requires(x != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
return new NAryExpr(x, new BinaryOperator(x, op), new ExprSeq(e0, e1));
}
- public static NAryExpr! Binary (BinaryOperator.Opcode op, Expr! e0, Expr! e1)
- {
+ public static NAryExpr Binary(BinaryOperator.Opcode op, Expr e0, Expr e1) {
+ Contract.Requires(e1 != null);
+ Contract.Requires(e0 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
return Binary(Token.NoToken, op, e0, e1);
}
- public static NAryExpr! Eq (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Eq, e1, e2); }
- public static NAryExpr! Neq (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Neq, e1, e2); }
- public static NAryExpr! Le (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Le, e1, e2); }
- public static NAryExpr! Ge (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Ge, e1, e2); }
- public static NAryExpr! Lt (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Lt, e1, e2); }
- public static NAryExpr! Gt (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Gt, e1, e2); }
- public static Expr! And (Expr! e1, Expr! e2) {
- if (e1 == true_) { return e2; }
- else if (e2 == true_) { return e1; }
- else if (e1 == false_ || e2 == false_) { return false_; }
- else { return Binary(BinaryOperator.Opcode.And, e1, e2); }
- }
- public static Expr! Or (Expr! e1, Expr! e2) {
- if (e1 == false_) { return e2; }
- else if (e2 == false_) { return e1; }
- else if (e1 == true_ || e2 == true_) { return true_; }
- else { return Binary(BinaryOperator.Opcode.Or, e1, e2); }
- }
- public static Expr! Not (Expr! e1) {
- NAryExpr nary = e1 as NAryExpr;
-
- if (e1 == true_) { return false_; }
- else if (e1 == false_) { return true_; }
- else if (nary != null)
- {
- if (nary.Fun is UnaryOperator)
- {
- UnaryOperator op = (UnaryOperator)nary.Fun;
- if (op.Op == UnaryOperator.Opcode.Not) { return (!) nary.Args[0]; }
- }
- else if (nary.Fun is BinaryOperator)
- {
- BinaryOperator op = (BinaryOperator)nary.Fun;
- Expr arg0 = (!)nary.Args[0];
- Expr arg1 = (!)nary.Args[1];
- if (op.Op == BinaryOperator.Opcode.Eq) { return Neq(arg0, arg1); }
- else if (op.Op == BinaryOperator.Opcode.Neq) { return Eq(arg0, arg1); }
- else if (op.Op == BinaryOperator.Opcode.Lt) { return Ge(arg0, arg1); }
- else if (op.Op == BinaryOperator.Opcode.Le) { return Gt(arg0, arg1); }
- else if (op.Op == BinaryOperator.Opcode.Ge) { return Lt(arg0, arg1); }
- else if (op.Op == BinaryOperator.Opcode.Gt) { return Le(arg0, arg1); }
- }
+ public static NAryExpr Eq(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Eq, e1, e2);
+ }
+ public static NAryExpr Neq(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Neq, e1, e2);
+ }
+ public static NAryExpr Le(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Le, e1, e2);
+ }
+ public static NAryExpr Ge(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Ge, e1, e2);
+ }
+ public static NAryExpr Lt(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Lt, e1, e2);
+ }
+ public static NAryExpr Gt(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Gt, e1, e2);
+ }
+ public static Expr And(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ if (e1 == true_) {
+ return e2;
+ } else if (e2 == true_) {
+ return e1;
+ } else if (e1 == false_ || e2 == false_) {
+ return false_;
+ } else {
+ return Binary(BinaryOperator.Opcode.And, e1, e2);
+ }
+ }
+ public static Expr Or(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ if (e1 == false_) {
+ return e2;
+ } else if (e2 == false_) {
+ return e1;
+ } else if (e1 == true_ || e2 == true_) {
+ return true_;
+ } else {
+ return Binary(BinaryOperator.Opcode.Or, e1, e2);
+ }
+ }
+ public static Expr Not(Expr e1) {
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<Expr>() != null);
+ NAryExpr nary = e1 as NAryExpr;
+
+ if (e1 == true_) {
+ return false_;
+ } else if (e1 == false_) {
+ return true_;
+ } else if (nary != null) {
+ if (nary.Fun is UnaryOperator) {
+ UnaryOperator op = (UnaryOperator)nary.Fun;
+ if (op.Op == UnaryOperator.Opcode.Not) {
+ return cce.NonNull(nary.Args[0]);
+ }
+ } else if (nary.Fun is BinaryOperator) {
+ BinaryOperator op = (BinaryOperator)nary.Fun;
+ Expr arg0 = cce.NonNull(nary.Args[0]);
+ Expr arg1 = cce.NonNull(nary.Args[1]);
+ if (op.Op == BinaryOperator.Opcode.Eq) {
+ return Neq(arg0, arg1);
+ } else if (op.Op == BinaryOperator.Opcode.Neq) {
+ return Eq(arg0, arg1);
+ } else if (op.Op == BinaryOperator.Opcode.Lt) {
+ return Ge(arg0, arg1);
+ } else if (op.Op == BinaryOperator.Opcode.Le) {
+ return Gt(arg0, arg1);
+ } else if (op.Op == BinaryOperator.Opcode.Ge) {
+ return Lt(arg0, arg1);
+ } else if (op.Op == BinaryOperator.Opcode.Gt) {
+ return Le(arg0, arg1);
+ }
}
+ }
- return Unary(Token.NoToken, UnaryOperator.Opcode.Not, e1);
- }
- public static NAryExpr! Imp (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Imp, e1, e2); }
- public static NAryExpr! Iff (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Iff, e1, e2); }
- public static NAryExpr! Add (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Add, e1, e2); }
- public static NAryExpr! Sub (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Sub, e1, e2); }
- public static NAryExpr! Mul (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Mul, e1, e2); }
- public static NAryExpr! Div (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Div, e1, e2); }
- public static NAryExpr! Mod (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Mod, e1, e2); }
- public static NAryExpr! Subtype (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Subtype, e1, e2); }
-
- public static IdentifierExpr! Ident (string! name, Type! type)
- {
+ return Unary(Token.NoToken, UnaryOperator.Opcode.Not, e1);
+ }
+ public static NAryExpr Imp(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Imp, e1, e2);
+ }
+ public static NAryExpr Iff(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Iff, e1, e2);
+ }
+ public static NAryExpr Add(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Add, e1, e2);
+ }
+ public static NAryExpr Sub(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Sub, e1, e2);
+ }
+ public static NAryExpr Mul(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Mul, e1, e2);
+ }
+ public static NAryExpr Div(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Div, e1, e2);
+ }
+ public static NAryExpr Mod(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Mod, e1, e2);
+ }
+ public static NAryExpr Subtype(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Subtype, e1, e2);
+ }
+
+ public static IdentifierExpr Ident(string name, Type type) {
+ Contract.Requires(type != null);
+ Contract.Requires(name != null);
+ Contract.Ensures(Contract.Result<IdentifierExpr>() != null);
return new IdentifierExpr(Token.NoToken, name, type);
}
- public static IdentifierExpr! Ident (Variable! decl)
- {
+ public static IdentifierExpr Ident(Variable decl) {
+ Contract.Requires(decl != null);
+ Contract.Ensures(Contract.Result<IdentifierExpr>() != null);
IdentifierExpr result = new IdentifierExpr(Token.NoToken, decl);
return result;
}
- public static LiteralExpr! Literal (bool value) { return new LiteralExpr(Token.NoToken, value); }
- public static LiteralExpr! Literal (int value) { return new LiteralExpr(Token.NoToken, BigNum.FromInt(value)); }
- public static LiteralExpr! Literal (BigNum value) { return new LiteralExpr(Token.NoToken, value); }
+ public static LiteralExpr Literal(bool value) {
+ Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+ return new LiteralExpr(Token.NoToken, value);
+ }
+ public static LiteralExpr Literal(int value) {
+ Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+ return new LiteralExpr(Token.NoToken, BigNum.FromInt(value));
+ }
+ public static LiteralExpr Literal(BigNum value) {
+ Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+ return new LiteralExpr(Token.NoToken, value);
+ }
- private static LiteralExpr! true_ = Literal(true);
- public static LiteralExpr! True { get { return true_; } }
+ private static LiteralExpr/*!*/ true_ = Literal(true);
+ public static LiteralExpr/*!*/ True {
+ get {
+ Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+ return true_;
+ }
+ }
- private static LiteralExpr! false_ = Literal(false);
- public static LiteralExpr! False { get { return false_; } }
+ private static LiteralExpr/*!*/ false_ = Literal(false);
+ public static LiteralExpr/*!*/ False {
+ get {
+ Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+ return false_;
+ }
+ }
- public static NAryExpr! Select(Expr! map, params Expr[]! args) {
+ public static NAryExpr Select(Expr map, params Expr[] args) {
+ Contract.Requires(args != null);
+ Contract.Requires(map != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
return SelectTok(Token.NoToken, map, args);
}
- public static NAryExpr! Select(Expr! map, List<Expr!>! args) {
+ public static NAryExpr Select(Expr map, List<Expr/*!*/>/*!*/ args) {
+ Contract.Requires(map != null);
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
return Select(map, args.ToArray());
}
// use a different name for this variant of the method
// (-> some bug prevents overloading in this case)
- public static NAryExpr! SelectTok(IToken! x, Expr! map, params Expr[]! args)
- {
- ExprSeq! allArgs = new ExprSeq ();
+ public static NAryExpr SelectTok(IToken x, Expr map, params Expr[] args) {
+ Contract.Requires(args != null);
+ Contract.Requires(map != null);
+ Contract.Requires(x != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ ExprSeq/*!*/ allArgs = new ExprSeq();
allArgs.Add(map);
- foreach (Expr! a in args)
+ foreach (Expr/*!*/ a in args) {
+ Contract.Assert(a != null);
allArgs.Add(a);
+ }
return new NAryExpr(x, new MapSelect(Token.NoToken, args.Length), allArgs);
}
-
- public static NAryExpr! Store(Expr! map, params Expr[]! args) {
+
+ public static NAryExpr Store(Expr map, params Expr[] args) {
+ Contract.Requires(args != null);
+ Contract.Requires(map != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
return StoreTok(Token.NoToken, map, args);
}
- public static NAryExpr! Store(Expr! map, List<Expr!>! indexes, Expr! rhs) {
- Expr[]! allArgs = new Expr [indexes.Count + 1];
+ public static NAryExpr Store(Expr map, List<Expr/*!*/>/*!*/ indexes, Expr rhs) {
+ Contract.Requires(rhs != null);
+ Contract.Requires(map != null);
+ Contract.Requires(cce.NonNullElements(indexes));
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ Expr[]/*!*/ allArgs = new Expr[indexes.Count + 1];
for (int i = 0; i < indexes.Count; ++i)
allArgs[i] = indexes[i];
allArgs[indexes.Count] = rhs;
@@ -206,18 +352,28 @@ namespace Microsoft.Boogie // use a different name for this variant of the method
// (-> some bug prevents overloading in this case)
- public static NAryExpr! StoreTok(IToken! x, Expr! map, params Expr[]! args)
- requires args.Length > 0; // zero or more indices, plus the value
- {
- ExprSeq! allArgs = new ExprSeq ();
+ public static NAryExpr/*!*/ StoreTok(IToken x, Expr map, params Expr[] args) {
+ Contract.Requires(args != null);
+ Contract.Requires(map != null);
+ Contract.Requires(x != null);
+ Contract.Requires(args.Length > 0); // zero or more indices, plus the value
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+
+ ExprSeq/*!*/ allArgs = new ExprSeq();
allArgs.Add(map);
- foreach (Expr! a in args)
+ foreach (Expr/*!*/ a in args) {
+ Contract.Assert(a != null);
allArgs.Add(a);
+ }
return new NAryExpr(x, new MapStore(Token.NoToken, args.Length - 1), allArgs);
}
-
- public static NAryExpr! CoerceType(IToken! x, Expr! subexpr, Type! type) {
- ExprSeq! args = new ExprSeq ();
+
+ public static NAryExpr CoerceType(IToken x, Expr subexpr, Type type) {
+ Contract.Requires(type != null);
+ Contract.Requires(subexpr != null);
+ Contract.Requires(x != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ ExprSeq/*!*/ args = new ExprSeq();
args.Add(subexpr);
return new NAryExpr(x, new TypeCoercion(x, type), args);
}
@@ -231,23 +387,56 @@ namespace Microsoft.Boogie /// implement some proper subinterface of AI.IExpr).
/// The converse operations of this property are found in AbsInt\ExprFactories.ssc.
/// </summary>
- public abstract AI.IExpr! IExpr {
- [Peer] get;
+ public abstract AI.IExpr/*!*/ IExpr {
+ [Peer]
+ get;
}
}
-
- public class LiteralExpr : Expr, AI.IFunApp
- {
- public readonly object! Val; // false, true, a BigNum, or a BvConst
+ [ContractClassFor(typeof(Expr))]
+ public abstract class ExprContracts : Expr {
+ public ExprContracts() :base(null){
+
+ }
+ public override void Emit(TokenTextWriter wr, int contextBindingStrength, bool fragileContext) {
+ Contract.Requires(wr != null);
+ throw new NotImplementedException();
+ }
+ public override void ComputeFreeVariables(Set freeVars) {
+ Contract.Requires(freeVars != null);
+ throw new NotImplementedException();
+ }
+ public override Type ShallowType {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ throw new NotImplementedException();
+ }
+ }
+ public override Microsoft.AbstractInterpretationFramework.IExpr IExpr {
+ get {
+ Contract.Ensures(Contract.Result<Microsoft.AbstractInterpretationFramework.IExpr>() != null);
+
+ throw new NotImplementedException();
+ }
+ }
+ }
+
+ public class LiteralExpr : Expr, AI.IFunApp {
+ public readonly object/*!*/ Val; // false, true, a BigNum, or a BvConst
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Val != null);
+ }
+
/// <summary>
/// Creates a literal expression for the boolean value "b".
/// </summary>
/// <param name="tok"></param>
/// <param name="b"></param>
- public LiteralExpr(IToken! tok, bool b)
- : base(tok)
- {
+ public LiteralExpr(IToken/*!*/ tok, bool b)
+ : base(tok) {
+ Contract.Requires(tok != null);
Val = b;
}
/// <summary>
@@ -255,79 +444,76 @@ namespace Microsoft.Boogie /// </summary>
/// <param name="tok"></param>
/// <param name="v"></param>
- public LiteralExpr(IToken! tok, BigNum v)
- : base(tok)
- {
+ public LiteralExpr(IToken/*!*/ tok, BigNum v)
+ : base(tok) {
+ Contract.Requires(tok != null);
Val = v;
}
-
+
/// <summary>
/// Creates a literal expression for the bitvector value "v".
/// </summary>
- public LiteralExpr(IToken! tok, BigNum v, int b)
- : base(tok)
- {
+ public LiteralExpr(IToken/*!*/ tok, BigNum v, int b)
+ : base(tok) {
+ Contract.Requires(tok != null);
Val = new BvConst(v, b);
}
-
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is LiteralExpr)) return false;
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is LiteralExpr))
+ return false;
LiteralExpr other = (LiteralExpr)obj;
return object.Equals(this.Val, other.Val);
}
[Pure]
- public override int GetHashCode()
- {
+ public override int GetHashCode() {
return this.Val.GetHashCode();
}
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
stream.SetToken(this);
- if (this.Val is bool)
- {
+ if (this.Val is bool) {
stream.Write((bool)this.Val ? "true" : "false"); // correct capitalization
- }
- else
- {
- stream.Write((!) this.Val.ToString());
+ } else {
+ stream.Write(cce.NonNull(this.Val.ToString()));
}
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
// nothing to resolve
}
- public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
+ public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
+ //Contract.Requires(freeVars != null);
// no free variables to add
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
if (Val is BvConst && CommandLineOptions.Clo.Verify && CommandLineOptions.Clo.Bitvectors == CommandLineOptions.BvHandling.None)
tc.Error(this, "no bitvector handling specified, please use /bv:i or /bv:z flag");
this.Type = ShallowType;
}
- public override Type! ShallowType {
+ public override Type/*!*/ ShallowType {
get {
- if (Val is bool)
- {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ if (Val is bool) {
return Type.Bool;
- }
- else if (Val is BigNum)
- {
+ } else if (Val is BigNum) {
return Type.Int;
- }
- else if (Val is BvConst)
- {
+ } else if (Val is BvConst) {
return Type.GetBvType(((BvConst)Val).Bits);
- }
- else
- {
- assert false; // like, where did this value come from?!
+ } else {
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // like, where did this value come from?!
}
}
}
@@ -342,231 +528,250 @@ namespace Microsoft.Boogie return Val is bool && ((bool)Val) == true;
}
}
- public override AI.IExpr! IExpr {
- get {
- return this;
- }
+ public override AI.IExpr/*!*/ IExpr {
+ get {
+ Contract.Ensures(Contract.Result<AI.IExpr>() != null);
+ return this;
+ }
}
// should be eliminated after converting everything to BigNums
private int asInt {
- get {
- return asBigNum.ToIntSafe;
- }
- }
+ get {
+ return asBigNum.ToIntSafe;
+ }
+ }
public bool isBigNum {
- get {
- return Val is BigNum;
- }
- }
+ get {
+ return Val is BigNum;
+ }
+ }
public BigNum asBigNum {
- get {
- assert isBigNum;
- return (BigNum)(!)Val;
- }
+ get {
+ Contract.Assert(isBigNum);
+ return (BigNum)cce.NonNull(Val);
+ }
}
public bool isBool {
- get {
- return Val is bool;
- }
- }
+ get {
+ return Val is bool;
+ }
+ }
public bool asBool {
- get {
- assert isBool;
- return (bool)(!)Val;
- }
+ get {
+ Contract.Assert(isBool);
+ return (bool)cce.NonNull(Val);
+ }
}
- public AI.IFunctionSymbol! FunctionSymbol {
- get {
- if (Val is bool)
- {
- if ((bool)Val)
- {
- return AI.Prop.True;
- }
- else
- {
- return AI.Prop.False;
- }
- }
- else if (Val is BigNum)
- {
- return AI.Int.Const((BigNum)Val);
- }
- else if (Val is BvConst)
- {
- return AI.Bv.Const(((BvConst)Val).Value, ((BvConst)Val).Bits);
- }
- else
- {
- assert false; // like, where did this value come from?!
- }
+ public AI.IFunctionSymbol/*!*/ FunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+
+ if (Val is bool) {
+ if ((bool)Val) {
+ return AI.Prop.True;
+ } else {
+ return AI.Prop.False;
+ }
+ } else if (Val is BigNum) {
+ return AI.Int.Const((BigNum)Val);
+ } else if (Val is BvConst) {
+ return AI.Bv.Const(((BvConst)Val).Value, ((BvConst)Val).Bits);
+ } else {
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // like, where did this value come from?!
}
+ }
}
- public IList/*<AI.IExpr!>*/! Arguments {
- get {
- return ArrayList.ReadOnly(new AI.IExpr[0]);
- }
+ public IList/*<AI.IExpr!>*//*!*/ Arguments {
+ get {
+ Contract.Ensures(Contract.Result<IList>() != null);
+
+ return ArrayList.ReadOnly(new AI.IExpr[0]);
+ }
}
- public Microsoft.AbstractInterpretationFramework.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args) {
- assert args.Count == 0;
- return this;
+ public Microsoft.AbstractInterpretationFramework.IFunApp CloneWithArguments(IList/*<AI.IExpr!>*/ args) {
+ Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<Microsoft.AbstractInterpretationFramework.IFunApp>() != null);
+ Contract.Assert(args.Count == 0);
+ return this;
}
- public AI.AIType! AIType {
- get {
- if (Val is bool) {
- return AI.Prop.Type;
- } else if (Val is BigNum) {
- return AI.Int.Type;
- } else if (Val is BvConst) {
- return AI.Bv.Type;
- } else {
- assert false; // like, where did this value come from?!
- }
+ public AI.AIType/*!*/ AIType {
+ get {
+ Contract.Requires(AIType != null);
+ if (Val is bool) {
+ return AI.Prop.Type;
+ } else if (Val is BigNum) {
+ return AI.Int.Type;
+ } else if (Val is BvConst) {
+ return AI.Bv.Type;
+ } else {
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // like, where did this value come from?!
}
+ }
}
[Pure]
- public object DoVisit(AI.ExprVisitor! visitor)
- {
+ public object DoVisit(AI.ExprVisitor visitor) {
+ Contract.Requires(visitor != null);
return visitor.VisitFunApp(this);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitLiteralExpr(this);
}
}
- public class BvConst
- {
+ public class BvConst {
public BigNum Value;
public int Bits;
-
- public BvConst(BigNum v, int b)
- {
- assert v.Signum >= 0;
- Value = v;
- Bits = b;
- }
-
+
+ public BvConst(BigNum v, int b) {
+ Contract.Assert(v.Signum >= 0);
+ Value = v;
+ Bits = b;
+ }
+
[Pure]
- public override string! ToString()
- {
- return Value + "bv" + Bits;
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return Value + "bv" + Bits;
}
-
+
[Pure]
- public string! ToReadableString()
- {
- if (Value > BigNum.FromInt(10000)) {
- string! val = (!)Value.ToString("x");
- int pos = val.Length % 4;
- string! res = "0x" + val.Substring(0, pos);
- while (pos < val.Length) {
- res += "." + val.Substring(pos, 4);
- pos += 4;
- }
- return res + ".bv" + Bits;
- } else
- return ToString();
- }
-
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
+ public string ToReadableString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ if (Value > BigNum.FromInt(10000)) {
+ string val = cce.NonNull(Value.ToString("x"));
+ int pos = val.Length % 4;
+ string res = "0x" + val.Substring(0, pos);
+ Contract.Assert(res != null);
+ while (pos < val.Length) {
+ res += "." + val.Substring(pos, 4);
+ pos += 4;
+ }
+ return res + ".bv" + Bits;
+ } else
+ return ToString();
+ }
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
BvConst other = obj as BvConst;
- if (other == null) return false;
+ if (other == null)
+ return false;
return Bits == other.Bits && Value == other.Value;
}
-
- [Pure]
- public override int GetHashCode()
- {
+
+ [Pure]
+ public override int GetHashCode() {
unchecked {
return Value.GetHashCode() ^ Bits;
}
}
}
- public class AIVariableExpr : Expr
- {
-
+ public class AIVariableExpr : Expr {
+
public string Name; // identifier symbol
- public AI.IVariable! Decl; // identifier declaration
+ public AI.IVariable/*!*/ Decl; // identifier declaration
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Decl != null);
+ }
+
/// <summary>
/// Creates an unresolved identifier expression.
/// </summary>
/// <param name="tok"></param>
/// <param name="name"></param>
- public AIVariableExpr(IToken! tok, AI.IVariable! var)
- : base(tok)
- {
+ public AIVariableExpr(IToken/*!*/ tok, AI.IVariable/*!*/ var)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(var != null);
Name = var.ToString();
Decl = var;
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is AIVariableExpr)) return false;
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is AIVariableExpr))
+ return false;
AIVariableExpr other = (AIVariableExpr)obj;
return object.Equals(this.Name, other.Name) && object.Equals(this.Decl, other.Decl);
}
- [Pure]
- public override int GetHashCode()
- {
- int h = this.Name == null ? 0 : this.Name.GetHashCode();
- h ^= this.Decl == null ? 0 : this.Decl.GetHashCode();
+ [Pure]
+ public override int GetHashCode() {
+ int h = this.Name == null ? 0 : this.Name.GetHashCode();
+ h ^= this.Decl == null ? 0 : this.Decl.GetHashCode();
return h;
}
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
- if (CommandLineOptions.Clo.PrintWithUniqueASTIds)
- {
- stream.Write("{0}^^", this.Decl == null ? "NoDecl" : "h"+this.Decl.GetHashCode());
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
+ stream.Write("{0}^^", this.Decl == null ? "NoDecl" : "h" + this.Decl.GetHashCode());
}
stream.Write(this, "{0}", this.Name);
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
}
- public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
+ public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
+ //Contract.Requires(freeVars != null);
if (Decl is Variable) {
freeVars.Add((Variable)Decl);
}
}
- public override void Typecheck(TypecheckingContext! tc)
- {
- throw new System.NotImplementedException();
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ throw new System.NotImplementedException();
}
- public override Type! ShallowType
- {
- get { throw new System.NotImplementedException(); }
+ public override Type/*!*/ ShallowType {
+ get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+ throw new System.NotImplementedException();
+ }
}
- public override AI.IExpr! IExpr {
- get {
- return Decl;
- }
+ public override AI.IExpr/*!*/ IExpr {
+ get {
+ Contract.Ensures(Contract.Result<AI.IExpr>() != null);
+
+ return Decl;
+ }
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitAIVariableExpr(this);
}
}
-
- public class IdentifierExpr : Expr
- {
- public string! Name; // identifier symbol
+
+ public class IdentifierExpr : Expr {
+ public string/*!*/ Name; // identifier symbol
public Variable Decl; // identifier declaration
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Name != null);
+ }
+
/// <summary>
/// Creates an unresolved identifier expression. This constructor is intended to be called
@@ -575,9 +780,10 @@ namespace Microsoft.Boogie /// </summary>
/// <param name="tok"></param>
/// <param name="name"></param>
- internal IdentifierExpr(IToken! tok, string! name)
- : base(tok)
- {
+ internal IdentifierExpr(IToken/*!*/ tok, string/*!*/ name)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
Name = name;
// base(tok);
}
@@ -587,55 +793,57 @@ namespace Microsoft.Boogie /// <param name="tok"></param>
/// <param name="name"></param>
/// <param name="type"></param>
- public IdentifierExpr(IToken! tok, string! name, Type! type)
- : base(tok)
- {
+ public IdentifierExpr(IToken/*!*/ tok, string/*!*/ name, Type/*!*/ type)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(type != null);
Name = name;
Type = type;
// base(tok);
}
-
+
/// <summary>
/// Creates a resolved identifier expression.
/// </summary>
/// <param name="tok"></param>
/// <param name="d"></param>
- public IdentifierExpr(IToken! tok, Variable! d)
- : base(tok)
- {
- Name = (!) d.Name;
+ public IdentifierExpr(IToken/*!*/ tok, Variable/*!*/ d)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(d != null);
+ Name = cce.NonNull(d.Name);
Decl = d;
Type = d.TypedIdent.Type;
// base(tok);
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is IdentifierExpr)) return false;
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is IdentifierExpr))
+ return false;
IdentifierExpr other = (IdentifierExpr)obj;
return object.Equals(this.Name, other.Name) && object.Equals(this.Decl, other.Decl);
}
- [Pure]
- public override int GetHashCode()
- {
- int h = this.Name == null ? 0 : this.Name.GetHashCode();
- h ^= this.Decl == null ? 0 : this.Decl.GetHashCode();
+ [Pure]
+ public override int GetHashCode() {
+ int h = this.Name == null ? 0 : this.Name.GetHashCode();
+ h ^= this.Decl == null ? 0 : this.Decl.GetHashCode();
return h;
}
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
- if (CommandLineOptions.Clo.PrintWithUniqueASTIds)
- {
- stream.Write("{0}^^", this.Decl == null ? "NoDecl" : "h"+this.Decl.GetHashCode());
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
+ if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
+ stream.Write("{0}^^", this.Decl == null ? "NoDecl" : "h" + this.Decl.GetHashCode());
}
stream.Write(this, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name));
}
- public override void Resolve(ResolutionContext! rc)
- {
- if (Decl != null)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ if (Decl != null) {
// already resolved, but re-resolve type just in case it came from an unresolved type
if (Type != null) {
Type = Type.ResolveType(rc);
@@ -652,155 +860,201 @@ namespace Microsoft.Boogie Type = Type.ResolveType(rc);
}
}
- public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
- assume this.Decl != null;
+ public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
+ //Contract.Requires(freeVars != null);
+ Contract.Assume(this.Decl != null);
freeVars.Add(Decl);
}
- public override void Typecheck(TypecheckingContext! tc)
- {
- if (this.Decl != null)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ if (this.Decl != null) {
// sanity check
if (Type != null && !Type.Equals(Decl.TypedIdent.Type)) {
- tc.Error(this, "internal error, shallow-type assignment was done incorrectly, {0}:{1} != {2}",
+ tc.Error(this, "internal error, shallow-type assignment was done incorrectly, {0}:{1} != {2}",
Name, Type, Decl.TypedIdent.Type);
- assert false;
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
}
Type = Decl.TypedIdent.Type;
}
}
- public override Type! ShallowType {
+ public override Type/*!*/ ShallowType {
get {
- assert Type != null;
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ Contract.Assert(Type != null);
return Type;
}
}
-
- public sealed class ConstantFunApp : AI.IFunApp
- {
- private IdentifierExpr! identifierExpr;
- public IdentifierExpr! IdentifierExpr { get { return identifierExpr; } }
-
- private AI.IFunctionSymbol! symbol;
- public AI.IFunctionSymbol! FunctionSymbol { get { return symbol; } }
-
- private static IList! emptyArgs = ArrayList.ReadOnly((IList!)new ArrayList());
- public IList! Arguments { get { return emptyArgs; } }
-
- public AI.IFunApp! CloneWithArguments(IList! newargs) { return this; }
-
- [Pure]
- public object DoVisit(AI.ExprVisitor! visitor) { return visitor.VisitFunApp(this); }
-
- public ConstantFunApp(IdentifierExpr! ie, Constant! c)
- {
- this.identifierExpr = ie;
- this.symbol =
- new AI.NamedSymbol(c.TypedIdent.Name, BoogieFactory.Type2AIType(c.TypedIdent.Type));
- // base();
+
+ public sealed class ConstantFunApp : AI.IFunApp {
+ private IdentifierExpr/*!*/ identifierExpr;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(identifierExpr != null);
+ Contract.Invariant(symbol != null);
+ Contract.Invariant(emptyArgs != null);
+ }
+
+ public IdentifierExpr/*!*/ IdentifierExpr {
+ get {
+ Contract.Requires(IdentifierExpr != null);
+ return identifierExpr;
+ }
+ }
+
+ private AI.IFunctionSymbol/*!*/ symbol;
+ public AI.IFunctionSymbol/*!*/ FunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+ return symbol;
+ }
+ }
+
+ private static IList/*!*/ emptyArgs = ArrayList.ReadOnly(cce.NonNull((IList/*!*/)new ArrayList()));
+ public IList/*!*/ Arguments {
+ get {
+ Contract.Ensures(Contract.Result<IList>() != null);
+ return emptyArgs;
}
-
+ }
+
+ public AI.IFunApp CloneWithArguments(IList newargs) {
+ Contract.Requires(newargs != null);
+ Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
+ return this;
+ }
+
+ [Pure]
+ public object DoVisit(AI.ExprVisitor visitor) {
+ Contract.Requires(visitor != null);
+ return visitor.VisitFunApp(this);
+ }
+
+ public ConstantFunApp(IdentifierExpr ie, Constant c) {
+ Contract.Requires(c != null);
+ Contract.Requires(ie != null);
+ this.identifierExpr = ie;
+ this.symbol =
+ new AI.NamedSymbol(c.TypedIdent.Name, BoogieFactory.Type2AIType(c.TypedIdent.Type));
+ // base();
+ }
+
}
private AI.IExpr iexprCache = null;
- public override AI.IExpr! IExpr {
- get
- {
- if (iexprCache == null)
- {
- if (Decl is Constant)
- iexprCache = new ConstantFunApp(this, (Constant)Decl);
- else{
- assume this.Decl != null;
- iexprCache = Decl;
- }
- }
- return iexprCache;
+ public override AI.IExpr/*!*/ IExpr {
+ get {
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+
+ if (iexprCache == null) {
+ if (Decl is Constant)
+ iexprCache = new ConstantFunApp(this, (Constant)Decl);
+ else {
+ Contract.Assume(this.Decl != null);
+ iexprCache = Decl;
+ }
}
+ return iexprCache;
+ }
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitIdentifierExpr(this);
}
}
- public class OldExpr : Expr
- , AI.IFunApp // HACK
+ public class OldExpr : Expr, AI.IFunApp // HACK
{
- public Expr! Expr;
- public OldExpr(IToken! tok, Expr! expr)
- : base(tok)
- {
+ public Expr/*!*/ Expr;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Expr != null);
+ }
+
+ public OldExpr(IToken/*!*/ tok, Expr/*!*/ expr)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(expr != null);
Expr = expr;
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is OldExpr)) return false;
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is OldExpr))
+ return false;
OldExpr other = (OldExpr)obj;
return object.Equals(this.Expr, other.Expr);
}
- [Pure]
- public override int GetHashCode()
- {
+ [Pure]
+ public override int GetHashCode() {
return this.Expr == null ? 0 : this.Expr.GetHashCode();
}
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
stream.Write(this, "old(");
this.Expr.Emit(stream);
stream.Write(")");
}
- public override void Resolve(ResolutionContext! rc)
- {
- if (rc.StateMode != ResolutionContext.State.Two)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
+ if (rc.StateMode != ResolutionContext.State.Two) {
rc.Error(this, "old expressions allowed only in two-state contexts");
}
Expr.Resolve(rc);
}
- public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
+ public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
+ //Contract.Requires(freeVars != null);
Expr.ComputeFreeVariables(freeVars);
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
Expr.Typecheck(tc);
Type = Expr.Type;
}
- public override Type! ShallowType {
+ public override Type/*!*/ ShallowType {
get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
return Expr.ShallowType;
}
}
- public override AI.IExpr! IExpr {
- get {
-// Put back these lines when "HACK" removed
-// // An Old expression has no AI.IExpr representation
-// assert false;
-// throw new System.Exception(); // make compiler shut up
- return this; // HACK
- }
+ public override AI.IExpr/*!*/ IExpr {
+ get {
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+
+ // Put back these lines when "HACK" removed
+ // // An Old expression has no AI.IExpr representation
+ // {Contract.Assert(false);throw new cce.UnreachableException();}
+ return this; // HACK
+ }
}
[Pure]
- public object DoVisit(AI.ExprVisitor! visitor)
- {
+ public object DoVisit(AI.ExprVisitor visitor) {
+ Contract.Requires(visitor != null);
return visitor.VisitFunApp(this);
}
- public AI.IFunApp! CloneWithArguments(IList/*<IExpr!>*/! args)
- {
- assume args.Count == 1;
- AI.IExpr! iexpr = (AI.IExpr!)args[0];
+ public AI.IFunApp CloneWithArguments(IList/*<IExpr!>*/ args) {
+ Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
+ Contract.Assume(args.Count == 1);
+ AI.IExpr/*!*/ iexpr = (AI.IExpr)cce.NonNull(args[0]);
return new OldExpr(Token.NoToken, BoogieFactory.IExpr2Expr(iexpr));
}
private IList/*?*/ argCache = null;
- public IList/*<IExpr!*/! Arguments
- {
+ public IList/*<IExpr!*//*!*/ Arguments {
+
get {
- if (argCache == null)
- {
+ Contract.Ensures(Contract.Result<IList>() != null);
+
+ if (argCache == null) {
IList l = new ArrayList(1);
l.Add(Expr.IExpr);
argCache = ArrayList.ReadOnly(l);
@@ -808,46 +1062,101 @@ namespace Microsoft.Boogie return argCache;
}
}
- private sealed class OldFunctionSymbol : AI.IFunctionSymbol
- {
- private static AI.AIType! aitype = new AI.FunctionType(AI.Value.Type, AI.Value.Type);
- public AI.AIType! AIType { get { return aitype; } }
- private OldFunctionSymbol() { }
- internal static OldFunctionSymbol! Sym = new OldFunctionSymbol();
+ private sealed class OldFunctionSymbol : AI.IFunctionSymbol {
+ private static AI.AIType/*!*/ aitype = new AI.FunctionType(AI.Value.Type, AI.Value.Type);
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(aitype != null);
+ Contract.Invariant(Sym != null);
+ }
+
+ public AI.AIType/*!*/ AIType {
+ get {
+ Contract.Ensures(Contract.Result<AIType>() != null);
+ return aitype;
+ }
+ }
+ private OldFunctionSymbol() {
+ }
+ internal static OldFunctionSymbol/*!*/ Sym = new OldFunctionSymbol();
+
[Pure]
- public override string! ToString() { return "old"; }
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return "old";
+ }
}
- public AI.IFunctionSymbol! FunctionSymbol
- {
- get { return OldFunctionSymbol.Sym; }
+ public AI.IFunctionSymbol/*!*/ FunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+ return OldFunctionSymbol.Sym;
+ }
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitOldExpr(this);
}
}
-
+ [ContractClass(typeof(IAppliableVisitorContracts<>))]
public interface IAppliableVisitor<T> {
-
- T Visit(UnaryOperator! unaryOperator);
-
- T Visit(BinaryOperator! binaryOperator);
-
- T Visit(FunctionCall! functionCall);
-
- T Visit(MapSelect! mapSelect);
-
- T Visit(MapStore! mapStore);
-
- T Visit(TypeCoercion! typeCoercion);
-
- T Visit(IfThenElse! ifThenElse);
+ T Visit(UnaryOperator/*!*/ unaryOperator);
+ T Visit(BinaryOperator/*!*/ binaryOperator);
+ T Visit(FunctionCall/*!*/ functionCall);
+ T Visit(MapSelect/*!*/ mapSelect);
+ T Visit(MapStore/*!*/ mapStore);
+ T Visit(TypeCoercion/*!*/ typeCoercion);
+ T Visit(IfThenElse/*!*/ ifThenElse);
}
+ [ContractClassFor(typeof(IAppliableVisitor<>))]
+ public abstract class IAppliableVisitorContracts<T> : IAppliableVisitor<T> {
- public interface IAppliable
- {
- string! FunctionName { get; }
+ #region IAppliableVisitor<T> Members
+
+ public T Visit(UnaryOperator unaryOperator) {
+ Contract.Requires(unaryOperator != null);
+ throw new NotImplementedException();
+ }
+
+ public T Visit(BinaryOperator binaryOperator) {
+ Contract.Requires(binaryOperator != null);
+ throw new NotImplementedException();
+ }
+
+ public T Visit(FunctionCall functionCall) {
+ Contract.Requires(functionCall != null);
+ throw new NotImplementedException();
+ }
+
+ public T Visit(MapSelect mapSelect) {
+ Contract.Requires(mapSelect != null);
+ throw new NotImplementedException();
+ }
+
+ public T Visit(MapStore mapStore) {
+ Contract.Requires(mapStore != null);
+ throw new NotImplementedException();
+ }
+
+ public T Visit(TypeCoercion typeCoercion) {
+ Contract.Requires(typeCoercion != null);
+ throw new NotImplementedException();
+ }
+
+ public T Visit(IfThenElse ifThenElse) {
+ Contract.Requires(ifThenElse != null);
+ throw new NotImplementedException();
+ }
+
+ #endregion
+ }
+
+ [ContractClass(typeof(IAppliableContracts))]
+ public interface IAppliable {
+ string/*!*/ FunctionName {
+ get;
+ }
/// <summary>
/// Emits to "stream" the operator applied to the given arguments.
@@ -858,14 +1167,16 @@ namespace Microsoft.Boogie /// <param name="stream"></param>
/// <param name="contextBindingStrength"></param>
/// <param name="fragileContext"></param>
- void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext);
+ void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream, int contextBindingStrength, bool fragileContext);
- void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting);
+ void Resolve(ResolutionContext/*!*/ rc, Expr/*!*/ subjectForErrorReporting);
/// <summary>
/// Requires the object to have been properly resolved.
/// </summary>
- int ArgumentCount { get; }
+ int ArgumentCount {
+ get;
+ }
/// <summary>
/// Typechecks the arguments "args" for the Appliable. If the arguments are
@@ -879,251 +1190,426 @@ namespace Microsoft.Boogie /// </summary>
/// <param name="args"></param>
/// <param name="tc"></param>
- Type Typecheck(ref ExprSeq! args, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc);
- ensures args.Length == old(args.Length);
- // requires Microsoft.SpecSharp.Collections.Reductions.Forall{Expr! arg in args; arg.Type != null};
-
+ Type Typecheck(ref ExprSeq/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/ tc);
+
+ // Contract.Requires( Microsoft.SpecSharp.Collections.Reductions.Forall{Expr! arg in args; arg.Type != null});
+
/// <summary>
/// Returns the result type of the IAppliable, supposing the argument are of the correct types.
/// </summary>
- Type! ShallowType(ExprSeq! args);
-
- AI.IFunctionSymbol! AIFunctionSymbol { get; }
-
- T Dispatch<T>(IAppliableVisitor<T>! visitor);
+ Type/*!*/ ShallowType(ExprSeq/*!*/ args);
+
+ AI.IFunctionSymbol/*!*/ AIFunctionSymbol {
+ get;
+ }
+
+ T Dispatch<T>(IAppliableVisitor<T>/*!*/ visitor);
}
-
- public interface IOverloadedAppliable
- {
- void ResolveOverloading(NAryExpr! expr);
+ [ContractClassFor(typeof(IAppliable))]
+ abstract class IAppliableContracts : IAppliable {
+
+ #region IAppliable Members
+
+ public string FunctionName {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+ throw new NotImplementedException();
+ }
+ }
+
+ public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ Contract.Requires(args != null);
+ Contract.Requires(stream != null);
+ throw new NotImplementedException();
+ }
+
+ public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
+ Contract.Requires(rc != null);
+ Contract.Requires(subjectForErrorReporting != null);
+ throw new NotImplementedException();
+ }
+
+ public int ArgumentCount {
+ get {
+ throw new NotImplementedException();
+ }
+ }
+
+ public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+ Contract.Requires(args != null);
+ Contract.Requires(tc != null);
+ Contract.Ensures(Contract.ValueAtReturn(out args) != null);
+ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+ Contract.Ensures(args.Length == Contract.OldValue(args.Length));
+ throw new NotImplementedException();
+ }
+
+ public Type ShallowType(ExprSeq args) {
+ Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+
+ throw new NotImplementedException();
+ }
+
+ public IFunctionSymbol AIFunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+ throw new NotImplementedException();
+ }
+ }
+
+ public T Dispatch<T>(IAppliableVisitor<T> visitor) {
+ Contract.Requires(visitor != null);
+ throw new NotImplementedException();
+ }
+
+ #endregion
}
-
- public class UnaryOperator : IAppliable
- {
- private IToken! tok;
- public enum Opcode { Not };
+
+
+ [ContractClass(typeof(IOverloadedAppliableContracts))]
+ public interface IOverloadedAppliable {
+ void ResolveOverloading(NAryExpr/*!*/ expr);
+ }
+ [ContractClassFor(typeof(IOverloadedAppliable))]
+ public abstract class IOverloadedAppliableContracts : IOverloadedAppliable {
+
+ #region IOverloadedAppliable Members
+
+ void IOverloadedAppliable.ResolveOverloading(NAryExpr expr) {
+ Contract.Requires(expr != null);
+ throw new NotImplementedException();
+ }
+
+ #endregion
+ }
+
+ public class UnaryOperator : IAppliable {
+ private IToken/*!*/ tok;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(tok != null);
+ }
+
+ public enum Opcode {
+ Not
+ };
private Opcode op;
- public Opcode Op { get { return op; } }
- public UnaryOperator (IToken! tok, Opcode op) { this.tok = tok; this.op = op; }
+ public Opcode Op {
+ get {
+ return op;
+ }
+ }
+ public UnaryOperator(IToken tok, Opcode op) {
+ Contract.Requires(tok != null);
+ this.tok = tok;
+ this.op = op;
+ }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is UnaryOperator)) return false;
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is UnaryOperator))
+ return false;
UnaryOperator other = (UnaryOperator)obj;
return object.Equals(this.op, other.op);
}
- [Pure]
- public override int GetHashCode()
- {
- return (int) this.op;
+ [Pure]
+ public override int GetHashCode() {
+ return (int)this.op;
}
- public string! FunctionName
- {
- get
- {
- switch (this.op)
- {
- case Opcode.Not: return "!";
+ public string/*!*/ FunctionName {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ switch (this.op) {
+ case Opcode.Not:
+ return "!";
}
System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString());
throw new Exception();
}
}
- public AI.IFunctionSymbol! AIFunctionSymbol {
- get {
- switch (this.op) {
- case Opcode.Not: return AI.Prop.Not;
- }
- System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString());
- throw new Exception();
+ public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+
+ switch (this.op) {
+ case Opcode.Not:
+ return AI.Prop.Not;
}
+ System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString());
+ throw new Exception();
+ }
}
- public void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
+ public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
+ //Contract.Requires(args != null);
stream.SetToken(ref this.tok);
- assert args.Length == 1;
+ Contract.Assert(args.Length == 1);
// determine if parens are needed
int opBindingStrength = 0x60;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
- if (parensNeeded)
- {
+ if (parensNeeded) {
stream.Write("(");
}
stream.Write(FunctionName);
- ((!)args[0]).Emit(stream, opBindingStrength, false);
- if (parensNeeded)
- {
+ cce.NonNull(args[0]).Emit(stream, opBindingStrength, false);
+ if (parensNeeded) {
stream.Write(")");
}
}
- public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting)
- {
+ public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
+ //Contract.Requires(subjectForErrorReporting != null);
+ //Contract.Requires(rc != null);
if (rc.TriggerMode && this.op == Opcode.Not) {
rc.Error(subjectForErrorReporting, "boolean operators are not allowed in triggers");
}
}
- public int ArgumentCount
- {
- get
- {
+ public int ArgumentCount {
+ get {
return 1;
}
}
- public Type Typecheck(ref ExprSeq! args, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
- {
- assume args.Length == 1;
+ public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ //Contract.Requires(args != null);
+ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+ Contract.Ensures(Contract.ValueAtReturn(out args) != null);
+
+ Contract.Assume(args.Length == 1);
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- Type arg0type = (!)((!)args[0]).Type;
- switch (this.op)
- {
+ Type arg0type = cce.NonNull(cce.NonNull(args[0]).Type);
+ switch (this.op) {
case Opcode.Not:
- if (arg0type.Unify(Type.Bool))
- {
+ if (arg0type.Unify(Type.Bool)) {
return Type.Bool;
}
goto BAD_TYPE;
}
System.Diagnostics.Debug.Fail("unknown unary operator: " + op.ToString());
- assert false;
- BAD_TYPE:
- tc.Error(this.tok, "invalid argument type ({1}) to unary operator {0}",
- this.FunctionName, arg0type);
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ BAD_TYPE:
+ tc.Error(this.tok, "invalid argument type ({1}) to unary operator {0}",
+ this.FunctionName, arg0type);
return null;
}
- public Type! ShallowType(ExprSeq! args) {
+ public Type ShallowType(ExprSeq args) {
+ //Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
switch (this.op) {
case Opcode.Not:
return Type.Bool;
- default:
- assert false; // unexpected unary operator
+ default: {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // unexpected unary operator
}
}
- public object Evaluate (object argument)
- {
- if (argument == null) { return null; }
- switch (this.op)
- {
+ public object Evaluate(object argument) {
+ if (argument == null) {
+ return null;
+ }
+ switch (this.op) {
case Opcode.Not:
- if (argument is bool) { return ! ((bool)argument); }
+ if (argument is bool) {
+ return !((bool)argument);
+ }
throw new System.InvalidOperationException("unary Not only applies to bool");
}
return null; // unreachable
}
-
- public T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+
+ public T Dispatch<T>(IAppliableVisitor<T> visitor) {
+ //Contract.Requires(visitor != null);
return visitor.Visit(this);
}
}
- public class BinaryOperator : IAppliable, IOverloadedAppliable
- {
- private IToken! tok;
- public enum Opcode { Add, Sub, Mul, Div, Mod, Eq, Neq, Gt, Ge, Lt, Le, And, Or, Imp, Iff, Subtype };
+ public class BinaryOperator : IAppliable, IOverloadedAppliable {
+ private IToken/*!*/ tok;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(tok != null);
+ }
+
+ public enum Opcode {
+ Add,
+ Sub,
+ Mul,
+ Div,
+ Mod,
+ Eq,
+ Neq,
+ Gt,
+ Ge,
+ Lt,
+ Le,
+ And,
+ Or,
+ Imp,
+ Iff,
+ Subtype
+ };
private Opcode op;
- public Opcode Op { get { return op; } }
- public BinaryOperator (IToken! tok, Opcode op) { this.tok = tok; this.op = op; }
+ public Opcode Op {
+ get {
+ return op;
+ }
+ }
+ public BinaryOperator(IToken tok, Opcode op) {
+ Contract.Requires(tok != null);
+ this.tok = tok;
+ this.op = op;
+ }
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is BinaryOperator)) return false;
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is BinaryOperator))
+ return false;
BinaryOperator other = (BinaryOperator)obj;
return object.Equals(this.op, other.op);
}
- [Pure]
- public override int GetHashCode()
- {
- return (int) this.op << 1;
+ [Pure]
+ public override int GetHashCode() {
+ return (int)this.op << 1;
}
- public string! FunctionName
- {
- get
- {
- switch (this.op)
- {
- case Opcode.Add: return "+";
- case Opcode.Sub: return "-";
- case Opcode.Mul: return "*";
- case Opcode.Div: return "/";
- case Opcode.Mod: return "%";
- case Opcode.Eq: return "==";
- case Opcode.Neq: return "!=";
- case Opcode.Gt: return ">";
- case Opcode.Ge: return ">=";
- case Opcode.Lt: return "<";
- case Opcode.Le: return "<=";
- case Opcode.And: return "&&";
- case Opcode.Or: return "||";
- case Opcode.Imp: return "==>";
- case Opcode.Iff: return "<==>";
- case Opcode.Subtype: return "<:";
+ public string/*!*/ FunctionName {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ switch (this.op) {
+ case Opcode.Add:
+ return "+";
+ case Opcode.Sub:
+ return "-";
+ case Opcode.Mul:
+ return "*";
+ case Opcode.Div:
+ return "/";
+ case Opcode.Mod:
+ return "%";
+ case Opcode.Eq:
+ return "==";
+ case Opcode.Neq:
+ return "!=";
+ case Opcode.Gt:
+ return ">";
+ case Opcode.Ge:
+ return ">=";
+ case Opcode.Lt:
+ return "<";
+ case Opcode.Le:
+ return "<=";
+ case Opcode.And:
+ return "&&";
+ case Opcode.Or:
+ return "||";
+ case Opcode.Imp:
+ return "==>";
+ case Opcode.Iff:
+ return "<==>";
+ case Opcode.Subtype:
+ return "<:";
}
System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString());
throw new Exception();
}
}
- public AI.IFunctionSymbol! AIFunctionSymbol {
- get {
- switch (this.op) {
- case Opcode.Add: return AI.Int.Add;
- case Opcode.Sub: return AI.Int.Sub;
- case Opcode.Mul: return AI.Int.Mul;
- case Opcode.Div: return AI.Int.Div;
- case Opcode.Mod: return AI.Int.Mod;
- case Opcode.Eq: return AI.Value.Eq;
- case Opcode.Neq: return AI.Value.Neq;
- case Opcode.Gt: return AI.Int.Greater;
- case Opcode.Ge: return AI.Int.AtLeast;
- case Opcode.Lt: return AI.Int.Less;
- case Opcode.Le: return AI.Int.AtMost;
- case Opcode.And: return AI.Prop.And;
- case Opcode.Or: return AI.Prop.Or;
- case Opcode.Imp: return AI.Prop.Implies;
- case Opcode.Iff: return AI.Value.Eq;
- case Opcode.Subtype: return AI.Value.Subtype;
- }
- System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString());
- throw new Exception();
+ public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+
+ switch (this.op) {
+
+ case Opcode.Add:
+ return AI.Int.Add;
+ case Opcode.Sub:
+ return AI.Int.Sub;
+ case Opcode.Mul:
+ return AI.Int.Mul;
+ case Opcode.Div:
+ return AI.Int.Div;
+ case Opcode.Mod:
+ return AI.Int.Mod;
+ case Opcode.Eq:
+ return AI.Value.Eq;
+ case Opcode.Neq:
+ return AI.Value.Neq;
+ case Opcode.Gt:
+ return AI.Int.Greater;
+ case Opcode.Ge:
+ return AI.Int.AtLeast;
+ case Opcode.Lt:
+ return AI.Int.Less;
+ case Opcode.Le:
+ return AI.Int.AtMost;
+ case Opcode.And:
+ return AI.Prop.And;
+ case Opcode.Or:
+ return AI.Prop.Or;
+ case Opcode.Imp:
+ return AI.Prop.Implies;
+ case Opcode.Iff:
+ return AI.Value.Eq;
+ case Opcode.Subtype:
+ return AI.Value.Subtype;
}
+ System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString());
+ throw new Exception();
+ }
}
- public void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
+ public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
+ //Contract.Requires(args != null);
stream.SetToken(ref this.tok);
- assert args.Length == 2;
+ Contract.Assert(args.Length == 2);
// determine if parens are needed
int opBindingStrength;
bool fragileLeftContext = false; // false means "allow same binding power on left without parens"
bool fragileRightContext = false; // false means "allow same binding power on right without parens"
- switch (this.op)
- {
+ switch (this.op) {
case Opcode.Add:
- opBindingStrength = 0x40; break;
+ opBindingStrength = 0x40;
+ break;
case Opcode.Sub:
- opBindingStrength = 0x40; fragileRightContext = true; break;
+ opBindingStrength = 0x40;
+ fragileRightContext = true;
+ break;
case Opcode.Mul:
- opBindingStrength = 0x50; break;
+ opBindingStrength = 0x50;
+ break;
case Opcode.Div:
- opBindingStrength = 0x50; fragileRightContext = true; break;
+ opBindingStrength = 0x50;
+ fragileRightContext = true;
+ break;
case Opcode.Mod:
- opBindingStrength = 0x50; fragileRightContext = true; break;
+ opBindingStrength = 0x50;
+ fragileRightContext = true;
+ break;
case Opcode.Eq:
case Opcode.Neq:
case Opcode.Gt:
@@ -1135,13 +1621,18 @@ namespace Microsoft.Boogie fragileLeftContext = fragileRightContext = true;
break;
case Opcode.And:
- opBindingStrength = 0x20; break;
+ opBindingStrength = 0x20;
+ break;
case Opcode.Or:
- opBindingStrength = 0x21; break;
+ opBindingStrength = 0x21;
+ break;
case Opcode.Imp:
- opBindingStrength = 0x10; fragileLeftContext = true; break;
+ opBindingStrength = 0x10;
+ fragileLeftContext = true;
+ break;
case Opcode.Iff:
- opBindingStrength = 0x00; break;
+ opBindingStrength = 0x00;
+ break;
default:
System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString());
opBindingStrength = -1; // to please compiler, which refuses to consider whether or not all enumeration cases have been considered!
@@ -1152,23 +1643,21 @@ namespace Microsoft.Boogie bool parensNeeded = opBS < ctxtBS ||
(opBS == ctxtBS && (opBindingStrength != contextBindingStrength || fragileContext));
- if (parensNeeded)
- {
+ if (parensNeeded) {
stream.Write("(");
}
- ((!)args[0]).Emit(stream, opBindingStrength, fragileLeftContext);
+ cce.NonNull(args[0]).Emit(stream, opBindingStrength, fragileLeftContext);
stream.Write(" {0} ", FunctionName);
- ((!)args[1]).Emit(stream, opBindingStrength, fragileRightContext);
- if (parensNeeded)
- {
+ cce.NonNull(args[1]).Emit(stream, opBindingStrength, fragileRightContext);
+ if (parensNeeded) {
stream.Write(")");
}
}
- public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting)
- {
+ public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
+ //Contract.Requires(subjectForErrorReporting != null);
+ //Contract.Requires(rc != null);
if (rc.TriggerMode) {
- switch (this.op)
- {
+ switch (this.op) {
case Opcode.Add:
case Opcode.Sub:
case Opcode.Mul:
@@ -1203,25 +1692,25 @@ namespace Microsoft.Boogie }
}
}
- public int ArgumentCount
- {
- get
- {
+ public int ArgumentCount {
+ get {
return 2;
}
}
- public Type Typecheck(ref ExprSeq! args, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
- {
- assert args.Length == 2;
+ public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ //Contract.Requires(args != null);
+ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+ Contract.Ensures(args != null);
+ Contract.Assert(args.Length == 2);
// the default; the only binary operator with a type parameter is equality, but right
// we don't store this parameter because it does not appear necessary
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- Expr arg0 = (!)args[0];
- Expr arg1 = (!)args[1];
- Type arg0type = (!)arg0.Type;
- Type arg1type = (!)arg1.Type;
- switch (this.op)
- {
+ Expr arg0 = cce.NonNull(args[0]);
+ Expr arg1 = cce.NonNull(args[1]);
+ Type arg0type = cce.NonNull(arg0.Type);
+ Type arg1type = cce.NonNull(arg1.Type);
+ switch (this.op) {
case Opcode.Add:
case Opcode.Sub:
case Opcode.Mul:
@@ -1229,7 +1718,7 @@ namespace Microsoft.Boogie case Opcode.Mod:
if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) {
return Type.Int;
- }
+ }
goto BAD_TYPE;
case Opcode.Eq:
case Opcode.Neq:
@@ -1240,11 +1729,11 @@ namespace Microsoft.Boogie // quick path
return Type.Bool;
}
- TypeVariableSeq! unifiable = new TypeVariableSeq ();
+ TypeVariableSeq/*!*/ unifiable = new TypeVariableSeq();
unifiable.AddRange(arg0type.FreeVariables);
unifiable.AddRange(arg1type.FreeVariables);
- if (arg0type.Unify(arg1type, unifiable, new Dictionary<TypeVariable!, Type!> ()))
+ if (arg0type.Unify(arg1type, unifiable, new Dictionary<TypeVariable/*!*/, Type/*!*/>()))
return Type.Bool;
goto BAD_TYPE;
case Opcode.Gt:
@@ -1253,7 +1742,7 @@ namespace Microsoft.Boogie case Opcode.Le:
if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) {
return Type.Bool;
- }
+ }
goto BAD_TYPE;
case Opcode.And:
case Opcode.Or:
@@ -1261,27 +1750,30 @@ namespace Microsoft.Boogie case Opcode.Iff:
if (arg0type.Unify(Type.Bool) && arg1type.Unify(Type.Bool)) {
return Type.Bool;
- }
+ }
goto BAD_TYPE;
case Opcode.Subtype:
// Subtype is polymorphically typed and can compare things of
// arbitrary types (but both arguments must have the same type)
- if (arg0type.Unify(arg1type))
- {
+ if (arg0type.Unify(arg1type)) {
return Type.Bool;
}
goto BAD_TYPE;
}
System.Diagnostics.Debug.Fail("unknown binary operator: " + op.ToString());
- assert false;
- BAD_TYPE:
- tc.Error(this.tok, "invalid argument types ({1} and {2}) to binary operator {0}", this.FunctionName, arg0type, arg1type);
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ BAD_TYPE:
+ tc.Error(this.tok, "invalid argument types ({1} and {2}) to binary operator {0}", this.FunctionName, arg0type, arg1type);
return null;
}
-
- public Type! ShallowType(ExprSeq! args) {
- switch (this.op)
- {
+
+ public Type ShallowType(ExprSeq args) {
+ //Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ switch (this.op) {
case Opcode.Add:
case Opcode.Sub:
case Opcode.Mul:
@@ -1302,26 +1794,25 @@ namespace Microsoft.Boogie case Opcode.Subtype:
return Type.Bool;
- default:
- assert false; // unexpected binary operator
+ default: {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // unexpected binary operator
}
}
- public void ResolveOverloading(NAryExpr! expr)
- {
- Expr arg0 = (!) expr.Args[0];
- Expr arg1 = (!) expr.Args[1];
- switch (op)
- {
+ public void ResolveOverloading(NAryExpr expr) {
+ //Contract.Requires(expr != null);
+ Expr arg0 = cce.NonNull(expr.Args[0]);
+ Expr arg1 = cce.NonNull(expr.Args[1]);
+ switch (op) {
case Opcode.Eq:
- if (arg0.Type != null && arg0.Type.IsBool && arg1.Type != null && arg1.Type.IsBool)
- {
+ if (arg0.Type != null && arg0.Type.IsBool && arg1.Type != null && arg1.Type.IsBool) {
expr.Fun = new BinaryOperator(tok, Opcode.Iff);
}
break;
case Opcode.Neq:
- if (arg0.Type != null && arg0.Type.IsBool && arg1.Type != null && arg1.Type.IsBool)
- {
+ if (arg0.Type != null && arg0.Type.IsBool && arg1.Type != null && arg1.Type.IsBool) {
expr.Fun = new BinaryOperator(tok, Opcode.Iff);
arg1 = new NAryExpr(expr.tok, new UnaryOperator(tok, UnaryOperator.Opcode.Not), new ExprSeq(arg1));
@@ -1335,140 +1826,199 @@ namespace Microsoft.Boogie break;
}
}
-
- public object Evaluate (object e1, object e2)
- {
- if (e1 == null || e2 == null) { return null; }
- switch (this.op)
- {
- case Opcode.Add:
- if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)+((BigNum)e2); }
+ public object Evaluate(object e1, object e2) {
+ if (e1 == null || e2 == null) {
+ return null;
+ }
+
+ switch (this.op) {
+ case Opcode.Add:
+ if (e1 is BigNum && e2 is BigNum) {
+ return ((BigNum)e1) + ((BigNum)e2);
+ }
break;
- case Opcode.Sub:
- if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)-((BigNum)e2); }
+ case Opcode.Sub:
+ if (e1 is BigNum && e2 is BigNum) {
+ return ((BigNum)e1) - ((BigNum)e2);
+ }
break;
- case Opcode.Mul:
- if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)*((BigNum)e2); }
+ case Opcode.Mul:
+ if (e1 is BigNum && e2 is BigNum) {
+ return ((BigNum)e1) * ((BigNum)e2);
+ }
break;
- case Opcode.Div:
- if (e1 is BigNum && e2 is BigNum) { return /* TODO: right semantics? */ ((BigNum)e1)/((BigNum)e2); }
+ case Opcode.Div:
+ if (e1 is BigNum && e2 is BigNum) {
+ return /* TODO: right semantics? */ ((BigNum)e1) / ((BigNum)e2);
+ }
break;
- case Opcode.Mod:
- if (e1 is BigNum && e2 is BigNum) { return /* TODO: right semantics? */ ((BigNum)e1)%((BigNum)e2); }
+ case Opcode.Mod:
+ if (e1 is BigNum && e2 is BigNum) {
+ return /* TODO: right semantics? */ ((BigNum)e1) % ((BigNum)e2);
+ }
break;
- case Opcode.Lt:
- if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)<((BigNum)e2); }
+ case Opcode.Lt:
+ if (e1 is BigNum && e2 is BigNum) {
+ return ((BigNum)e1) < ((BigNum)e2);
+ }
break;
- case Opcode.Le:
- if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)<=((BigNum)e2); }
+ case Opcode.Le:
+ if (e1 is BigNum && e2 is BigNum) {
+ return ((BigNum)e1) <= ((BigNum)e2);
+ }
break;
- case Opcode.Gt:
- if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)>((BigNum)e2); }
+ case Opcode.Gt:
+ if (e1 is BigNum && e2 is BigNum) {
+ return ((BigNum)e1) > ((BigNum)e2);
+ }
break;
- case Opcode.Ge:
- if (e1 is BigNum && e2 is BigNum) { return ((BigNum)e1)>=((BigNum)e2); }
+ case Opcode.Ge:
+ if (e1 is BigNum && e2 is BigNum) {
+ return ((BigNum)e1) >= ((BigNum)e2);
+ }
break;
- case Opcode.And: if (e1 is bool && e2 is bool) { return (bool)e1 && (bool)e2; } break;
- case Opcode.Or: if (e1 is bool && e2 is bool) { return (bool)e1 || (bool)e2; } break;
- case Opcode.Imp: if (e1 is bool && e2 is bool) { return ! (bool)e1 || (bool)e2; } break;
- case Opcode.Iff: if (e1 is bool && e2 is bool) { return e1 == e2; } break;
+ case Opcode.And:
+ if (e1 is bool && e2 is bool) {
+ return (bool)e1 && (bool)e2;
+ }
+ break;
+ case Opcode.Or:
+ if (e1 is bool && e2 is bool) {
+ return (bool)e1 || (bool)e2;
+ }
+ break;
+ case Opcode.Imp:
+ if (e1 is bool && e2 is bool) {
+ return !(bool)e1 || (bool)e2;
+ }
+ break;
+ case Opcode.Iff:
+ if (e1 is bool && e2 is bool) {
+ return e1 == e2;
+ }
+ break;
- case Opcode.Eq: return Equals(e1,e2);
- case Opcode.Neq: return ! Equals(e1,e2);
+ case Opcode.Eq:
+ return Equals(e1, e2);
+ case Opcode.Neq:
+ return !Equals(e1, e2);
- case Opcode.Subtype: throw new System.NotImplementedException();
+ case Opcode.Subtype:
+ throw new System.NotImplementedException();
}
throw new System.InvalidOperationException("bad types to binary operator " + this.op);
}
-
- public T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+
+ public T Dispatch<T>(IAppliableVisitor<T> visitor) {
+ //Contract.Requires(visitor != null);
return visitor.Visit(this);
}
}
- public class FunctionCall : IAppliable, AI.IFunctionSymbol
- {
- private IdentifierExpr! name;
+ public class FunctionCall : IAppliable, AI.IFunctionSymbol {
+ private IdentifierExpr/*!*/ name;
public Function Func;
- public FunctionCall(IdentifierExpr! name) { this.name = name; }
- public FunctionCall(Function! f) { this.Func = f; this.name = new IdentifierExpr(Token.NoToken, f.Name); }
- public string! FunctionName { get { return this.name.Name; } }
+ public FunctionCall(IdentifierExpr name) {
+ Contract.Requires(name != null);
+ this.name = name;
+ }
+ public FunctionCall(Function f) {
+ Contract.Requires(f != null);
+ this.Func = f;
+ this.name = new IdentifierExpr(Token.NoToken, f.Name);
+ }
+ public string/*!*/ FunctionName {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return this.name.Name;
+ }
+ }
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(name != null);
+ }
- public AI.IFunctionSymbol! AIFunctionSymbol {
- get {
- if (name.Name == "$typeof") {
- return AI.Value.Typeof;
- } else if (name.Name == "$allocated") {
- return AI.FieldName.Allocated;
- } else {
- return this;
- }
+
+ public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+
+ if (name.Name == "$typeof") {
+ return AI.Value.Typeof;
+ } else if (name.Name == "$allocated") {
+ return AI.FieldName.Allocated;
+ } else {
+ return this;
}
+ }
}
[Pure]
- public override string! ToString() {
- return name.Name;
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return name.Name;
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
public override bool Equals(object other) {
- FunctionCall fc = other as FunctionCall;
- return fc != null && this.Func == fc.Func;
- }
- [Pure]
- public override int GetHashCode()
- {
- assume this.Func != null;
- return Func.GetHashCode();
- }
-
- public AI.AIType! AIType {
- get
- {
- assume this.Func != null;
- return AI.Value.FunctionType(this.Func.InParams.Length);
- }
+ FunctionCall fc = other as FunctionCall;
+ return fc != null && this.Func == fc.Func;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ Contract.Assume(this.Func != null);
+ return Func.GetHashCode();
}
- virtual public void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
+ public AI.AIType/*!*/ AIType {
+ get {
+ Contract.Ensures(Contract.Result<AIType>() != null);
+
+ Contract.Assume(this.Func != null);
+ return AI.Value.FunctionType(this.Func.InParams.Length);
+ }
+ }
+
+ virtual public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
+ Contract.Requires(args != null);
this.name.Emit(stream, 0xF0, false);
stream.Write("(");
args.Emit(stream);
stream.Write(")");
}
- public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting)
- {
- if (Func != null)
- {
+ public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
+ //Contract.Requires(subjectForErrorReporting != null);
+ Contract.Requires(rc != null);
+ if (Func != null) {
// already resolved
return;
}
Func = rc.LookUpProcedure(name.Name) as Function;
- if (Func == null)
- {
+ if (Func == null) {
rc.Error(this.name, "use of undeclared function: {0}", name.Name);
}
}
- public virtual int ArgumentCount
- {
- get
- {
- assume Func != null; // ArgumentCount requires object to be properly resolved.
+ public virtual int ArgumentCount {
+ get {
+ Contract.Assume(Func != null); // ArgumentCount requires object to be properly resolved.
return Func.InParams.Length;
}
}
- public virtual Type Typecheck(ref ExprSeq! actuals, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
- {
- assume this.Func != null;
- assume actuals.Length == Func.InParams.Length;
- assume Func.OutParams.Length == 1;
+ public virtual Type Typecheck(ref ExprSeq actuals, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ //Contract.Requires(actuals != null);
+ Contract.Ensures(Contract.ValueAtReturn(out actuals) != null);
+ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+ Contract.Assume(this.Func != null);
+ Contract.Assume(actuals.Length == Func.InParams.Length);
+ Contract.Assume(Func.OutParams.Length == 1);
- List<Type!>! resultingTypeArgs;
+ List<Type/*!*/>/*!*/ resultingTypeArgs;
TypeSeq actualResultType =
Type.CheckArgumentTypes(Func.TypeParameters,
out resultingTypeArgs,
@@ -1476,177 +2026,221 @@ namespace Microsoft.Boogie actuals,
Func.OutParams.ToTypeSeq,
null,
- // we need some token to report a possibly wrong number of
- // arguments
- actuals.Length > 0 ? ((!)actuals[0]).tok : Token.NoToken,
+ // we need some token to report a possibly wrong number of
+ // arguments
+ actuals.Length > 0 ? cce.NonNull(actuals[0]).tok : Token.NoToken,
"application of " + name.Name,
tc);
-
+
if (actualResultType == null) {
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
return null;
} else {
- assert actualResultType.Length == 1;
+ Contract.Assert(actualResultType.Length == 1);
tpInstantiation =
SimpleTypeParamInstantiation.From(Func.TypeParameters, resultingTypeArgs);
return actualResultType[0];
}
}
- public Type! ShallowType(ExprSeq! args) {
- assume name.Type != null;
+ public Type ShallowType(ExprSeq args) {
+ //Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ Contract.Assume(name.Type != null);
return name.Type;
}
-
- public virtual T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+
+ public virtual T Dispatch<T>(IAppliableVisitor<T> visitor) {
+ //Contract.Requires(visitor != null);
return visitor.Visit(this);
}
}
-
+
public class TypeCoercion : IAppliable {
- private IToken! tok;
- public Type! Type;
-
- public TypeCoercion(IToken! tok, Type! type) {
+ private IToken/*!*/ tok;
+ public Type/*!*/ Type;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(tok != null);
+ }
+
+ public TypeCoercion(IToken tok, Type type) {
+ Contract.Requires(type != null);
+ Contract.Requires(tok != null);
this.tok = tok;
this.Type = type;
}
- public string! FunctionName { get {
- return ":";
- } }
+ public string/*!*/ FunctionName {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
- public void Emit(ExprSeq! args, TokenTextWriter! stream,
+ return ":";
+ }
+ }
+
+ public void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream,
int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(args != null);
+ //Contract.Requires(stream != null);
stream.SetToken(ref this.tok);
- assert args.Length == 1;
+ Contract.Assert(args.Length == 1);
// determine if parens are needed
int opBindingStrength = 0x90;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
- if (parensNeeded)
+ if (parensNeeded)
stream.Write("(");
- ((!)args[0]).Emit(stream, opBindingStrength, false);
+ cce.NonNull(args[0]).Emit(stream, opBindingStrength, false);
stream.Write("{0} ", FunctionName);
Type.Emit(stream, 0);
- if (parensNeeded)
+ if (parensNeeded)
stream.Write(")");
}
-
- public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting) {
+
+ public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
+ //Contract.Requires(subjectForErrorReporting != null);
+ //Contract.Requires(rc != null);
this.Type = this.Type.ResolveType(rc);
}
- public int ArgumentCount { get {
- return 1;
- } }
+ public int ArgumentCount {
+ get {
+ return 1;
+ }
+ }
+
+ public Type Typecheck(ref ExprSeq/*!*/ args,
+ out TypeParamInstantiation/*!*/ tpInstantiation,
+ TypecheckingContext/*!*/ tc) {
+ //Contract.Requires(args != null);
+ //Contract.Requires(tc != null);
+ Contract.Ensures(args != null);
- public Type Typecheck(ref ExprSeq! args,
- out TypeParamInstantiation! tpInstantiation,
- TypecheckingContext! tc) {
- assume args.Length == 1;
+ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+
+ Contract.Assume(args.Length == 1);
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- if (!this.Type.Unify((!)((!)args[0]).Type))
+ if (!this.Type.Unify(cce.NonNull(cce.NonNull(args[0]).Type)))
tc.Error(this.tok, "{0} cannot be coerced to {1}",
- ((!)args[0]).Type, this.Type);
+ cce.NonNull(args[0]).Type, this.Type);
return this.Type;
}
- public Type! ShallowType(ExprSeq! args) {
+ public Type ShallowType(ExprSeq args) {
+ //Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
return this.Type;
}
- public AI.IFunctionSymbol! AIFunctionSymbol { get {
- // not really clear what should be returned here ...
- // should the operation be completely invisible for the abstract interpretation?
- return AI.Heap.UnsupportedHeapOp;
- } }
-
- public T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+ public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+
+ // not really clear what should be returned here ...
+ // should the operation be completely invisible for the abstract interpretation?
+ return AI.Heap.UnsupportedHeapOp;
+ }
+ }
+
+ public T Dispatch<T>(IAppliableVisitor<T> visitor) {
+ //Contract.Requires(visitor != null);
return visitor.Visit(this);
}
}
- public class NAryExpr : Expr, AI.IFunApp
- {
- [Additive] [Peer]
- public IAppliable! Fun;
- public ExprSeq! Args;
+ public class NAryExpr : Expr, AI.IFunApp {
+ [Additive]
+ [Peer]
+ public IAppliable/*!*/ Fun;
+ public ExprSeq/*!*/ Args;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Fun != null);
+ Contract.Invariant(Args != null);
+ }
+
// The instantiation of type parameters that is determined during type checking.
// Which type parameters are available depends on the IAppliable
public TypeParamInstantiation TypeParameters = null;
[Captured]
- public NAryExpr(IToken! tok, IAppliable! fun, ExprSeq! args)
- : base(tok)
- {
+ public NAryExpr(IToken/*!*/ tok, IAppliable/*!*/ fun, ExprSeq/*!*/ args)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(fun != null);
+ Contract.Requires(args != null);
Fun = fun;
Args = args;
- assert forall{Expr arg in args; arg != null};
+ Contract.Assert(Contract.ForAll(0, args.Length, index => args[index] != null));
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is NAryExpr)) return false;
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is NAryExpr))
+ return false;
NAryExpr other = (NAryExpr)obj;
return object.Equals(this.Fun, other.Fun) && object.Equals(this.Args, other.Args);
}
- [Pure]
- public override int GetHashCode()
- {
+ [Pure]
+ public override int GetHashCode() {
int h = this.Fun.GetHashCode();
h ^= this.Args.GetHashCode();
return h;
}
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
stream.SetToken(this);
Fun.Emit(Args, stream, contextBindingStrength, fragileContext);
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
Fun.Resolve(rc, this);
- foreach (Expr! e in Args)
- {
+ foreach (Expr/*!*/ e in Args) {
+ Contract.Assert(e != null);
e.Resolve(rc);
}
}
- public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
- foreach (Expr! e in Args) {
+ public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
+ //Contract.Requires(freeVars != null);
+ foreach (Expr/*!*/ e in Args) {
+ Contract.Assert(e != null);
e.ComputeFreeVariables(freeVars);
}
// also add the free type variables
if (TypeParameters != null) {
- foreach (TypeVariable! var in TypeParameters.FormalTypeParams)
- foreach (TypeVariable! w in TypeParameters[var].FreeVariables)
+ foreach (TypeVariable/*!*/ var in TypeParameters.FormalTypeParams) {
+ Contract.Assert(var != null);
+ foreach (TypeVariable/*!*/ w in TypeParameters[var].FreeVariables) {
+ Contract.Assert(w != null);
freeVars.Add(w);
+ }
+ }
}
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
int prevErrorCount = tc.ErrorCount;
- foreach (Expr! e in Args)
- {
+ foreach (Expr/*!*/ e in Args) {
+ Contract.Assert(e != null);
e.Typecheck(tc);
}
- if (Fun.ArgumentCount != Args.Length)
- {
+ if (Fun.ArgumentCount != Args.Length) {
tc.Error(this, "wrong number of arguments to function: {0} ({1} instead of {2})",
Fun.FunctionName, Args.Length, Fun.ArgumentCount);
- }
- else if (tc.ErrorCount == prevErrorCount &&
- // if the type parameters are set, this node has already been
- // typechecked and does not need to be checked again
- TypeParameters == null)
- {
- TypeParamInstantiation! tpInsts;
+ } else if (tc.ErrorCount == prevErrorCount &&
+ // if the type parameters are set, this node has already been
+ // typechecked and does not need to be checked again
+ TypeParameters == null) {
+ TypeParamInstantiation tpInsts;
Type = Fun.Typecheck(ref Args, out tpInsts, tc);
if (Type != null && Type.IsBv && CommandLineOptions.Clo.Verify && CommandLineOptions.Clo.Bitvectors == CommandLineOptions.BvHandling.None) {
tc.Error(this, "no bitvector handling specified, please use /bv:i or /bv:z flag");
@@ -1654,8 +2248,7 @@ namespace Microsoft.Boogie TypeParameters = tpInsts;
}
IOverloadedAppliable oa = Fun as IOverloadedAppliable;
- if (oa != null)
- {
+ if (oa != null) {
oa.ResolveOverloading(this);
}
if (Type == null) {
@@ -1663,43 +2256,55 @@ namespace Microsoft.Boogie Type = new TypeProxy(this.tok, "type_checking_error");
}
}
- public override Type! ShallowType {
+ public override Type/*!*/ ShallowType {
get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
return Fun.ShallowType(Args);
}
}
-
- public override AI.IExpr! IExpr {
- get {
- return this;
- }
+
+ public override AI.IExpr/*!*/ IExpr {
+ get {
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+
+ return this;
+ }
}
- public AI.IFunctionSymbol! FunctionSymbol {
- get {
- return Fun.AIFunctionSymbol;
- }
+ public AI.IFunctionSymbol/*!*/ FunctionSymbol {
+ get {
+
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+
+ return Fun.AIFunctionSymbol;
+ }
}
- public IList/*<AI.IExpr!>*/! Arguments {
- get {
- AI.IExpr[] a = new AI.IExpr[Args.Length];
- for (int i = 0; i < Args.Length; i++) {
- a[i] = ((!)Args[i]).IExpr;
- }
- return ArrayList.ReadOnly(a);
+ public IList/*<AI.IExpr!>*//*!*/ Arguments {
+ get {
+ Contract.Ensures(Contract.Result<IList>() != null);
+
+ AI.IExpr[] a = new AI.IExpr[Args.Length];
+ for (int i = 0; i < Args.Length; i++) {
+ a[i] = cce.NonNull(Args[i]).IExpr;
}
+ return ArrayList.ReadOnly(a);
+ }
}
- public AI.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args) {
- return new NAryExpr(this.tok, this.Fun, BoogieFactory.IExprArray2ExprSeq(args));
+ public AI.IFunApp CloneWithArguments(IList/*<AI.IExpr!>*/ args) {
+ Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
+ return new NAryExpr(this.tok, this.Fun, BoogieFactory.IExprArray2ExprSeq(args));
}
[Pure]
- public object DoVisit(AI.ExprVisitor! visitor)
- {
+ public object DoVisit(AI.ExprVisitor visitor) {
+ Contract.Requires(visitor != null);
return visitor.VisitFunApp(this);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitNAryExpr(this);
}
}
@@ -1707,50 +2312,63 @@ namespace Microsoft.Boogie public class MapSelect : IAppliable, AI.IFunctionSymbol {
public readonly int Arity;
- private readonly IToken! tok;
+ private readonly IToken/*!*/ tok;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(tok != null);
+ }
+
- public MapSelect(IToken! tok, int arity) {
+ public MapSelect(IToken tok, int arity) {
+ Contract.Requires(tok != null);
this.tok = tok;
this.Arity = arity;
}
- public string! FunctionName { get {
- return "MapSelect";
- } }
+ public string/*!*/ FunctionName {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (!(obj is MapSelect)) return false;
+ return "MapSelect";
+ }
+ }
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (!(obj is MapSelect))
+ return false;
MapSelect other = (MapSelect)obj;
return this.Arity == other.Arity;
}
- [Pure]
- public override int GetHashCode()
- {
+ [Pure]
+ public override int GetHashCode() {
return Arity.GetHashCode() * 2823;
}
- public void Emit(ExprSeq! args, TokenTextWriter! stream,
+ public void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream,
int contextBindingStrength, bool fragileContext) {
- assume args.Length == Arity + 1;
+ //Contract.Requires(args != null);
+ //Contract.Requires(stream != null);
+ Contract.Assume(args.Length == Arity + 1);
Emit(args, stream, contextBindingStrength, fragileContext, false);
}
- public static void Emit(ExprSeq! args, TokenTextWriter! stream,
+ public static void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream,
int contextBindingStrength, bool fragileContext,
bool withRhs) {
+ Contract.Requires(args != null);
+ Contract.Requires(stream != null);
const int opBindingStrength = 0x70;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
- if (parensNeeded)
- {
+ if (parensNeeded) {
stream.Write("(");
}
- ((!)args[0]).Emit(stream, opBindingStrength, false);
+ cce.NonNull(args[0]).Emit(stream, opBindingStrength, false);
stream.Write("[");
string sep = "";
@@ -1758,45 +2376,56 @@ namespace Microsoft.Boogie for (int i = 1; i < lastIndex; ++i) {
stream.Write(sep);
sep = ", ";
- ((!)args[i]).Emit(stream);
+ cce.NonNull(args[i]).Emit(stream);
}
if (withRhs) {
stream.Write(" := ");
- ((!)args.Last()).Emit(stream);
+ cce.NonNull(args.Last()).Emit(stream);
}
stream.Write("]");
- if (parensNeeded)
- {
+ if (parensNeeded) {
stream.Write(")");
- }
+ }
}
- public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting) {
+ public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
+ //Contract.Requires(subjectForErrorReporting != null);
+ //Contract.Requires(rc != null);
// PR: nothing?
}
- public int ArgumentCount { get {
- return Arity + 1;
- } }
+ public int ArgumentCount {
+ get {
+ return Arity + 1;
+ }
+ }
// it is assumed that each of the arguments has already been typechecked
- public static Type Typecheck(Type! mapType,
- // we just pass an Absy, because in
- // the AssignCmd maps can also be
- // represented by non-expressions
- Absy! map,
- ExprSeq! indexes,
- // the type parameters, in this context, are the parameters of the
- // potentially polymorphic map type. Because it might happen that
- // the whole map type is unknown and represented using a MapTypeProxy,
- // the instantiations given in the following out-parameter are subject
- // to change if further unifications are done.
- out TypeParamInstantiation! tpInstantiation,
- TypecheckingContext! tc,
- IToken! typeCheckingSubject,
- string! opName) {
+ public static Type Typecheck(Type/*!*/ mapType,
+ // we just pass an Absy, because in
+ // the AssignCmd maps can also be
+ // represented by non-expressions
+ Absy/*!*/ map,
+ ExprSeq/*!*/ indexes,
+ // the type parameters, in this context, are the parameters of the
+ // potentially polymorphic map type. Because it might happen that
+ // the whole map type is unknown and represented using a MapTypeProxy,
+ // the instantiations given in the following out-parameter are subject
+ // to change if further unifications are done.
+ out TypeParamInstantiation/*!*/ tpInstantiation,
+ TypecheckingContext/*!*/ tc,
+ IToken/*!*/ typeCheckingSubject,
+ string/*!*/ opName) {
+ Contract.Requires(mapType != null);
+ Contract.Requires(map != null);
+ Contract.Requires(indexes != null);
+ Contract.Requires(tc != null);
+ Contract.Requires(typeCheckingSubject != null);
+ Contract.Requires(opName != null);
+ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+
mapType = mapType.Expanded;
if (mapType.IsMap && mapType.MapArity != indexes.Length) {
tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1} instead of {2}",
@@ -1821,54 +2450,69 @@ namespace Microsoft.Boogie }
}
- public Type Typecheck(ref ExprSeq! args, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
- {
- assume args.Length == Arity + 1;
+ public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ //Contract.Requires(args != null);
+ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+ Contract.Assume(args.Length == Arity + 1);
- ExprSeq actualArgs = new ExprSeq ();
+ ExprSeq actualArgs = new ExprSeq();
for (int i = 1; i < args.Length; ++i)
actualArgs.Add(args[i]);
- return Typecheck((!)((!)args[0]).Type, (!)args[0],
+ return Typecheck(cce.NonNull(cce.NonNull(args[0]).Type), cce.NonNull(args[0]),
actualArgs, out tpInstantiation, tc, this.tok, "map select");
}
/// <summary>
/// Returns the result type of the IAppliable, supposing the argument are of the correct types.
/// </summary>
- public Type! ShallowType(ExprSeq! args) {
- Expr a0 = (!)args[0];
+ public Type ShallowType(ExprSeq args) {
+ //Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ Expr a0 = cce.NonNull(args[0]);
Type a0Type = a0.ShallowType;
if (a0Type == null || !a0Type.IsMap) {
// we are unable to determine the type of the select, so just return an arbitrary type
return Type.Int;
}
MapType mapType = a0Type.AsMap;
- TypeSeq actualArgTypes = new TypeSeq ();
+ TypeSeq actualArgTypes = new TypeSeq();
for (int i = 1; i < args.Length; ++i) {
- actualArgTypes.Add(((!)args[i]).ShallowType);
+ actualArgTypes.Add(cce.NonNull(args[i]).ShallowType);
}
return Type.InferValueType(mapType.TypeParameters, mapType.Arguments, mapType.Result, actualArgTypes);
}
- public AI.IFunctionSymbol! AIFunctionSymbol { get {
+ public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+
switch (Arity) {
- case 1: return AI.Heap.Select1;
- case 2: return AI.Heap.Select2;
- default:
- // Maps with Arity arguments are not fully supported yet
- return AI.Heap.UnsupportedHeapOp;
+ case 1:
+ return AI.Heap.Select1;
+ case 2:
+ return AI.Heap.Select2;
+ default:
+ // Maps with Arity arguments are not fully supported yet
+ return AI.Heap.UnsupportedHeapOp;
}
- } }
-
- public AI.AIType! AIType {
- [Rep][ResultNotNewlyAllocated]
+ }
+ }
+
+ public AI.AIType/*!*/ AIType {
+ [Rep]
+ [ResultNotNewlyAllocated]
get {
+ Contract.Ensures(Contract.Result<AIType>() != null);
+
return AI.Prop.Type; // THAT is a type? PR: no idea whether this makes sense,
- // but it is the type of select1
- } }
+ // but it is the type of select1
+ }
+ }
- public T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+ public T Dispatch<T>(IAppliableVisitor<T> visitor) {
+ //Contract.Requires(visitor != null);
return visitor.Visit(this);
}
}
@@ -1876,57 +2520,79 @@ namespace Microsoft.Boogie public class MapStore : IAppliable, AI.IFunctionSymbol {
public readonly int Arity;
- public readonly IToken! tok;
+ public readonly IToken/*!*/ tok;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(tok != null);
+ }
+
- public MapStore(IToken! tok, int arity) {
+ public MapStore(IToken tok, int arity) {
+ Contract.Requires(tok != null);
this.tok = tok;
this.Arity = arity;
}
- public string! FunctionName { get {
- return "MapStore";
- } }
+ public string/*!*/ FunctionName {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (!(obj is MapStore)) return false;
+ return "MapStore";
+ }
+ }
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (!(obj is MapStore))
+ return false;
MapStore other = (MapStore)obj;
return this.Arity == other.Arity;
}
- [Pure]
- public override int GetHashCode()
- {
+ [Pure]
+ public override int GetHashCode() {
return Arity.GetHashCode() * 28231;
}
- public void Emit(ExprSeq! args, TokenTextWriter! stream,
+ public void Emit(ExprSeq/*!*/ args, TokenTextWriter/*!*/ stream,
int contextBindingStrength, bool fragileContext) {
- assert args.Length == Arity + 2;
+ //Contract.Requires(args != null);
+ //Contract.Requires(stream != null);
+ Contract.Assert(args.Length == Arity + 2);
MapSelect.Emit(args, stream, contextBindingStrength, fragileContext, true);
}
- public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting) {
+ public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
+ //Contract.Requires(subjectForErrorReporting != null);
+ //Contract.Requires(rc != null);
// PR: nothing?
}
- public int ArgumentCount { get {
- return Arity + 2;
- } }
+ public int ArgumentCount {
+ get {
+ return Arity + 2;
+ }
+ }
// it is assumed that each of the arguments has already been typechecked
- public static Type Typecheck(ExprSeq! args, out TypeParamInstantiation! tpInstantiation,
- TypecheckingContext! tc,
- IToken! typeCheckingSubject,
- string! opName) {
+ public static Type Typecheck(ExprSeq/*!*/ args, out TypeParamInstantiation/*!*/ tpInstantiation,
+ TypecheckingContext/*!*/ tc,
+ IToken/*!*/ typeCheckingSubject,
+ string/*!*/ opName) {
+ Contract.Requires(args != null);
+ Contract.Requires(tc != null);
+ Contract.Requires(typeCheckingSubject != null);
+ Contract.Requires(opName != null);
+ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+
// part of the type checking works exactly as for MapSelect
- ExprSeq! selectArgs = new ExprSeq ();
+ ExprSeq selectArgs = new ExprSeq();
for (int i = 1; i < args.Length - 1; ++i)
selectArgs.Add(args[i]);
Type resultType =
- MapSelect.Typecheck((!)((!)args[0]).Type, (!)args[0],
+ MapSelect.Typecheck(cce.NonNull(cce.NonNull(args[0]).Type), cce.NonNull(args[0]),
selectArgs, out tpInstantiation, tc, typeCheckingSubject, opName);
// check the the rhs has the right type
@@ -1934,49 +2600,65 @@ namespace Microsoft.Boogie // error messages have already been created by MapSelect.Typecheck
return null;
}
- Type rhsType = (!)((!)args.Last()).Type;
+ Type rhsType = cce.NonNull(cce.NonNull(args.Last()).Type);
if (!resultType.Unify(rhsType)) {
- tc.Error(((!)args.Last()).tok,
+ tc.Error(cce.NonNull(args.Last()).tok,
"right-hand side in {0} with wrong type: {1} (expected: {2})",
opName, rhsType, resultType);
return null;
}
-
- return ((!)args[0]).Type;
+
+ return cce.NonNull(args[0]).Type;
}
- public Type Typecheck(ref ExprSeq! args,
- out TypeParamInstantiation! tpInstantiation,
- TypecheckingContext! tc)
- {
- assert args.Length == Arity + 2;
+ public Type Typecheck(ref ExprSeq/*!*/ args,
+ out TypeParamInstantiation/*!*/ tpInstantiation,
+ TypecheckingContext/*!*/ tc) {
+ //Contract.Requires(args != null);
+ //Contract.Requires(tc != null);
+ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+ Contract.Ensures(Contract.ValueAtReturn(out args) != null);
+ Contract.Assert(args.Length == Arity + 2);
return Typecheck(args, out tpInstantiation, tc, this.tok, "map store");
}
/// <summary>
/// Returns the result type of the IAppliable, supposing the argument are of the correct types.
/// </summary>
- public Type! ShallowType(ExprSeq! args) {
- return ((!)args[0]).ShallowType;
+ public Type ShallowType(ExprSeq args) {
+ //Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return cce.NonNull(args[0]).ShallowType;
}
- public AI.IFunctionSymbol! AIFunctionSymbol { get {
+ public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+
switch (Arity) {
- case 1: return AI.Heap.Update1;
- case 2: return AI.Heap.Update2;
- default:
- // Maps with Arity arguments are not fully supported yet
- return AI.Heap.UnsupportedHeapOp;
+ case 1:
+ return AI.Heap.Update1;
+ case 2:
+ return AI.Heap.Update2;
+ default:
+ // Maps with Arity arguments are not fully supported yet
+ return AI.Heap.UnsupportedHeapOp;
}
- } }
-
- public AI.AIType! AIType {
- [Rep][ResultNotNewlyAllocated]
+ }
+ }
+
+ public AI.AIType/*!*/ AIType {
+ [Rep]
+ [ResultNotNewlyAllocated]
get {
+ Contract.Ensures(Contract.Result<AIType>() != null);
+
return AI.Heap.Type;
- } }
-
- public T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+ }
+ }
+
+ public T Dispatch<T>(IAppliableVisitor<T> visitor) {
+ //Contract.Requires(visitor != null);
return visitor.Visit(this);
}
}
@@ -1984,63 +2666,81 @@ namespace Microsoft.Boogie public class IfThenElse : IAppliable, AI.IFunctionSymbol {
- public IToken! tok;
+ public IToken/*!*/ tok;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(tok != null);
+ }
+
- public IfThenElse(IToken! tok) {
+ public IfThenElse(IToken tok) {
+ Contract.Requires(tok != null);
this.tok = tok;
}
- public string! FunctionName { get {
- return "if-then-else";
- } }
+ public string/*!*/ FunctionName {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (!(obj is IfThenElse)) return false;
+ return "if-then-else";
+ }
+ }
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (!(obj is IfThenElse))
+ return false;
return true;
}
- [Pure]
- public override int GetHashCode()
- {
+ [Pure]
+ public override int GetHashCode() {
return 1;
}
- public void Emit(ExprSeq! args, TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
+ public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
+ //Contract.Requires(args != null);
stream.SetToken(ref this.tok);
- assert args.Length == 3;
+ Contract.Assert(args.Length == 3);
stream.Write("(if ");
- ((!)args[0]).Emit(stream, 0x00, false);
+ cce.NonNull(args[0]).Emit(stream, 0x00, false);
stream.Write(" then ");
- ((!)args[1]).Emit(stream, 0x00, false);
+ cce.NonNull(args[1]).Emit(stream, 0x00, false);
stream.Write(" else ");
- ((!)args[2]).Emit(stream, 0x00, false);
+ cce.NonNull(args[2]).Emit(stream, 0x00, false);
stream.Write(")");
}
- public void Resolve(ResolutionContext! rc, Expr! subjectForErrorReporting) {
+ public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
+ //Contract.Requires(subjectForErrorReporting != null);
+ Contract.Requires(rc != null);
// PR: nothing?
}
- public int ArgumentCount { get {
- return 3;
- } }
+ public int ArgumentCount {
+ get {
+ return 3;
+ }
+ }
- public Type Typecheck(ref ExprSeq! args, out TypeParamInstantiation! tpInstantiation, TypecheckingContext! tc)
- {
- assert args.Length == 3;
+ public Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ //Contract.Requires(args != null);
+ Contract.Ensures(args != null);
+ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+ Contract.Assert(args.Length == 3);
// the default; the only binary operator with a type parameter is equality, but right
// we don't store this parameter because it does not appear necessary
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- Expr arg0 = (!)args[0];
- Expr arg1 = (!)args[1];
- Expr arg2 = (!)args[2];
+ Expr arg0 = cce.NonNull(args[0]);
+ Expr arg1 = cce.NonNull(args[1]);
+ Expr arg2 = cce.NonNull(args[2]);
- if (!((!)arg0.Type).Unify(Type.Bool)) {
+ if (!cce.NonNull(arg0.Type).Unify(Type.Bool)) {
tc.Error(this.tok, "the first argument to if-then-else should be bool, not {0}", arg0.Type);
- } else if (!((!)arg1.Type).Unify((!)arg2.Type)) {
+ } else if (!cce.NonNull(arg1.Type).Unify(cce.NonNull(arg2.Type))) {
tc.Error(this.tok, "branches of if-then-else have incompatible types {0} and {1}", arg1.Type, arg2.Type);
} else {
return arg1.Type;
@@ -2052,60 +2752,87 @@ namespace Microsoft.Boogie /// <summary>
/// Returns the result type of the IAppliable, supposing the argument are of the correct types.
/// </summary>
- public Type! ShallowType(ExprSeq! args) {
- return ((!)args[1]).ShallowType;
+ public Type ShallowType(ExprSeq args) {
+ //Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return cce.NonNull(args[1]).ShallowType;
}
- public AI.IFunctionSymbol! AIFunctionSymbol { get { return this; } }
-
- public AI.AIType! AIType {
- [Rep][ResultNotNewlyAllocated]
+ public AI.IFunctionSymbol/*!*/ AIFunctionSymbol {
get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+ return this;
+ }
+ }
+
+ public AI.AIType/*!*/ AIType {
+ [Rep]
+ [ResultNotNewlyAllocated]
+ get {
+ Contract.Ensures(Contract.Result<AIType>() != null);
+
return AI.Value.FunctionType(3);
- } }
-
- public T Dispatch<T>(IAppliableVisitor<T>! visitor) {
+ }
+ }
+
+ public T Dispatch<T>(IAppliableVisitor<T> visitor) {
+ //Contract.Requires(visitor != null);
return visitor.Visit(this);
}
}
-
- public class CodeExpr : Expr, AI.IUnknown
- {
- public VariableSeq! LocVars;
+
+ public class CodeExpr : Expr, AI.IUnknown {
+ public VariableSeq/*!*/ LocVars;
[Rep]
- public List<Block!>! Blocks;
- public CodeExpr(VariableSeq! localVariables, List<Block!>! blocks)
- : base(Token.NoToken)
- requires 0 < blocks.Count;
- {
+ public List<Block/*!*/>/*!*/ Blocks;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(LocVars != null);
+ Contract.Invariant(cce.NonNullElements(Blocks));
+ }
+
+ public CodeExpr(VariableSeq/*!*/ localVariables, List<Block/*!*/>/*!*/ blocks)
+ : base(Token.NoToken) {
+ Contract.Requires(localVariables != null);
+ Contract.Requires(cce.NonNullElements(blocks));
+ Contract.Requires(0 < blocks.Count);
LocVars = localVariables;
Blocks = blocks;
}
- public override AI.IExpr! IExpr { get { return this; } }
- [Pure] public object DoVisit(AI.ExprVisitor! visitor) { return this; }
-
- public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
+ public override AI.IExpr/*!*/ IExpr {
+ get {
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ return this;
+ }
+ }
+ [Pure]
+ public object DoVisit(AI.ExprVisitor visitor) {
+ Contract.Requires(visitor != null);
+ return this;
+ }
+
+ public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
+ //Contract.Requires(freeVars != null);
// Treat a BlockEexpr as if it has no free variables at all
}
- public override void Emit (TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
//level++;
int level = 0;
stream.WriteLine(level, "|{");
- if (this.LocVars.Length > 0)
- {
+ if (this.LocVars.Length > 0) {
stream.Write(level + 1, "var ");
this.LocVars.Emit(stream);
stream.WriteLine(";");
}
- foreach (Block! b in this.Blocks)
- {
- b.Emit(stream, level+1);
+ foreach (Block/*!*/ b in this.Blocks) {
+ Contract.Assert(b != null);
+ b.Emit(stream, level + 1);
}
stream.WriteLine();
@@ -2115,114 +2842,123 @@ namespace Microsoft.Boogie stream.WriteLine();
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
rc.PushVarContext();
- foreach (Variable! v in LocVars)
- {
+ foreach (Variable/*!*/ v in LocVars) {
+ Contract.Assert(v != null);
v.Register(rc);
v.Resolve(rc);
}
rc.PushProcedureContext();
- foreach (Block! b in Blocks)
- {
+ foreach (Block/*!*/ b in Blocks) {
+ Contract.Assert(b != null);
b.Register(rc);
}
-
- foreach (Block! b in Blocks)
- {
+
+ foreach (Block/*!*/ b in Blocks) {
+ Contract.Assert(b != null);
b.Resolve(rc);
}
-
+
rc.PopProcedureContext();
rc.PopVarContext();
}
- public override void Typecheck(TypecheckingContext! tc){
- foreach (Variable! v in LocVars){
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ foreach (Variable/*!*/ v in LocVars) {
+ Contract.Assert(v != null);
v.Typecheck(tc);
}
- foreach (Block! b in Blocks){
+ foreach (Block/*!*/ b in Blocks) {
+ Contract.Assert(b != null);
b.Typecheck(tc);
}
this.Type = Type.Bool;
}
- public override Type! ShallowType {
+ public override Type/*!*/ ShallowType {
get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
return Type.Bool;
}
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitCodeExpr(this);
}
}
+ public class BvExtractExpr : Expr, AI.IFunApp {
+ public /*readonly--except in StandardVisitor*/ Expr/*!*/ Bitvector;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Bitvector != null);
+ }
-
- public class BvExtractExpr : Expr, AI.IFunApp
- {
- public /*readonly--except in StandardVisitor*/ Expr! Bitvector;
public readonly int Start, End;
-
- public BvExtractExpr(IToken! tok, Expr! bv, int end, int start)
- : base(tok)
- {
+
+ public BvExtractExpr(IToken/*!*/ tok, Expr/*!*/ bv, int end, int start)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(bv != null);
Bitvector = bv;
Start = start;
End = end;
// base(tok);
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is BvExtractExpr)) return false;
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is BvExtractExpr))
+ return false;
BvExtractExpr other = (BvExtractExpr)obj;
return object.Equals(this.Bitvector, other.Bitvector) &&
this.Start.Equals(other.Start) && this.End.Equals(other.End);
}
- [Pure]
- public override int GetHashCode()
- {
+ [Pure]
+ public override int GetHashCode() {
int h = this.Bitvector.GetHashCode();
h ^= Start * 17 ^ End * 13;
return h;
}
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
stream.SetToken(this);
int opBindingStrength = 0x70;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
- if (parensNeeded)
- {
+ if (parensNeeded) {
stream.Write("(");
}
Bitvector.Emit(stream, opBindingStrength, false);
stream.Write("[" + End + ":" + Start + "]");
- if (parensNeeded)
- {
+ if (parensNeeded) {
stream.Write(")");
}
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
Bitvector.Resolve(rc);
}
- public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
+ public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
+ //Contract.Requires(freeVars != null);
Bitvector.ComputeFreeVariables(freeVars);
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
Bitvector.Typecheck(tc);
- assert Bitvector.Type != null; // follows from postcondition of Expr.Typecheck
+ Contract.Assert(Bitvector.Type != null); // follows from postcondition of Expr.Typecheck
if (Start < 0) {
tc.Error(this, "start index in extract must not be negative");
@@ -2242,24 +2978,33 @@ namespace Microsoft.Boogie Type = new TypeProxy(this.tok, "type_checking_error");
}
}
-
- public override Type! ShallowType {
+
+ public override Type/*!*/ ShallowType {
get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
return Type.GetBvType(End - Start);
}
}
-
- public override AI.IExpr! IExpr {
+
+ public override AI.IExpr/*!*/ IExpr {
get {
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+
return this;
}
}
- public AI.IFunctionSymbol! FunctionSymbol {
- get { return AI.Bv.Extract;
+ public AI.IFunctionSymbol/*!*/ FunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+
+ return AI.Bv.Extract;
}
}
- public IList/*<AI.IExpr!>*/! Arguments {
+ public IList/*<AI.IExpr!>*//*!*/ Arguments {
get {
+ Contract.Ensures(Contract.Result<IList>() != null);
+
AI.IExpr[] a = new AI.IExpr[3];
a[0] = Bitvector.IExpr;
a[1] = new LiteralExpr(Token.NoToken, BigNum.FromInt(End));
@@ -2267,72 +3012,81 @@ namespace Microsoft.Boogie return ArrayList.ReadOnly(a);
}
}
- public AI.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args)
- {
- AI.IFunApp! retFun;
-
- if(args.Count == 3)
- {
+ public AI.IFunApp CloneWithArguments(IList/*<AI.IExpr!>*/ args) {
+ Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
+ AI.IFunApp retFun;
+
+ if (args.Count == 3) {
retFun = new BvExtractExpr(this.tok,
- BoogieFactory.IExpr2Expr((AI.IExpr!)args[0]),
- ((LiteralExpr!)args[1]).asBigNum.ToIntSafe,
- ((LiteralExpr!)args[2]).asBigNum.ToIntSafe);
- }
- else
- {
- assert false; // If we are something wrong is happended
+ BoogieFactory.IExpr2Expr(cce.NonNull((AI.IExpr)args[0])),
+ cce.NonNull((LiteralExpr/*!*/)args[1]).asBigNum.ToIntSafe,
+ cce.NonNull((LiteralExpr/*!*/)args[2]).asBigNum.ToIntSafe);
+ } else {
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // If we are something wrong is happended
}
return retFun;
}
[Pure]
- public object DoVisit(AI.ExprVisitor! visitor)
- {
+ public object DoVisit(AI.ExprVisitor visitor) {
+ Contract.Requires(visitor != null);
return visitor.VisitFunApp(this);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitBvExtractExpr(this);
}
}
- public class BvConcatExpr : Expr, AI.IFunApp
- {
- public /*readonly--except in StandardVisitor*/ Expr! E0, E1;
-
- public BvConcatExpr(IToken! tok, Expr! e0, Expr! e1)
- : base(tok)
- {
+ public class BvConcatExpr : Expr, AI.IFunApp {
+ public /*readonly--except in StandardVisitor*/ Expr/*!*/ E0, E1;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(E0 != null);
+ Contract.Invariant(E1 != null);
+ }
+
+
+ public BvConcatExpr(IToken/*!*/ tok, Expr/*!*/ e0, Expr/*!*/ e1)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
E0 = e0;
E1 = e1;
// base(tok);
}
- [Pure][Reads(ReadsAttribute.Reads.Nothing)]
- public override bool Equals(object obj)
- {
- if (obj == null) return false;
- if (!(obj is BvConcatExpr)) return false;
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object obj) {
+ if (obj == null)
+ return false;
+ if (!(obj is BvConcatExpr))
+ return false;
BvConcatExpr other = (BvConcatExpr)obj;
return object.Equals(this.E0, other.E0) && object.Equals(this.E1, other.E1);
}
- [Pure]
- public override int GetHashCode()
- {
+ [Pure]
+ public override int GetHashCode() {
int h = this.E0.GetHashCode() ^ this.E1.GetHashCode() * 17;
return h;
}
- public override void Emit(TokenTextWriter! stream, int contextBindingStrength, bool fragileContext)
- {
+ public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
stream.SetToken(this);
int opBindingStrength = 0x32;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
- if (parensNeeded)
- {
+ if (parensNeeded) {
stream.Write("(");
}
E0.Emit(stream, opBindingStrength, false);
@@ -2340,26 +3094,26 @@ namespace Microsoft.Boogie // while this operator is associative, our incomplete axioms in int translation don't
// make much use of it, so better stick to the actual tree shape
E1.Emit(stream, opBindingStrength, true);
- if (parensNeeded)
- {
+ if (parensNeeded) {
stream.Write(")");
}
}
- public override void Resolve(ResolutionContext! rc)
- {
+ public override void Resolve(ResolutionContext rc) {
+ //Contract.Requires(rc != null);
E0.Resolve(rc);
E1.Resolve(rc);
}
- public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
+ public override void ComputeFreeVariables(Set /*Variable*/ freeVars) {
+ //Contract.Requires(freeVars != null);
E0.ComputeFreeVariables(freeVars);
E1.ComputeFreeVariables(freeVars);
}
- public override void Typecheck(TypecheckingContext! tc)
- {
+ public override void Typecheck(TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
E0.Typecheck(tc);
- assert E0.Type != null; // follows from postcondition of Expr.Typecheck
+ Contract.Assert(E0.Type != null); // follows from postcondition of Expr.Typecheck
E1.Typecheck(tc);
- assert E1.Type != null; // follows from postcondition of Expr.Typecheck
+ Contract.Assert(E1.Type != null); // follows from postcondition of Expr.Typecheck
if (E0.Type.Unify(new BvTypeProxy(this.tok, "concat0", 0)) && E1.Type.Unify(new BvTypeProxy(this.tok, "concat1", 0))) {
Type = new BvTypeProxy(this.tok, "concat", E0.Type, E1.Type);
@@ -2370,9 +3124,11 @@ namespace Microsoft.Boogie Type = new TypeProxy(this.tok, "type_checking_error");
}
}
-
- public override Type! ShallowType {
+
+ public override Type/*!*/ ShallowType {
get {
+ Contract.Ensures(Contract.Result<Type>() != null);
+
Type t0 = E0.ShallowType;
Type t1 = E1.ShallowType;
int len0 = t0.IsBv ? t0.BvBits : /*expression is not type correct, so just pick an arbitrary number of bits*/0;
@@ -2380,49 +3136,57 @@ namespace Microsoft.Boogie return Type.GetBvType(len0 + len1);
}
}
-
- public override AI.IExpr! IExpr {
- get {
- return this;
- }
+
+ public override AI.IExpr/*!*/ IExpr {
+ get {
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+
+ return this;
+ }
}
- public AI.IFunctionSymbol! FunctionSymbol {
- get { return AI.Bv.Concat;
- }
+ public AI.IFunctionSymbol/*!*/ FunctionSymbol {
+ get {
+ Contract.Ensures(Contract.Result<IFunctionSymbol>() != null);
+ return AI.Bv.Concat;
+ }
}
- public IList/*<AI.IExpr!>*/! Arguments {
- get {
- AI.IExpr[] a = new AI.IExpr[2];
- a[0] = E0.IExpr;
- a[1] = E1.IExpr;
- return ArrayList.ReadOnly(a);
- }
+ public IList/*<AI.IExpr!>*//*!*/ Arguments {
+ get {
+ Contract.Ensures(Contract.Result<IList>() != null);
+
+ AI.IExpr[] a = new AI.IExpr[2];
+ a[0] = E0.IExpr;
+ a[1] = E1.IExpr;
+ return ArrayList.ReadOnly(a);
+ }
}
- public AI.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args)
- {
- AI.IFunApp! retFun;
-
- if(args.Count == 2)
- {
+ public AI.IFunApp CloneWithArguments(IList/*<AI.IExpr!>*/ args) {
+ Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
+ AI.IFunApp/*!*/ retFun;
+
+ if (args.Count == 2) {
retFun = new BvConcatExpr(this.tok,
- BoogieFactory.IExpr2Expr((AI.IExpr!)args[0]),
- BoogieFactory.IExpr2Expr((AI.IExpr!)args[1]));
- }
- else
- {
- assert false; // If we are something wrong is happended
+ BoogieFactory.IExpr2Expr(cce.NonNull((AI.IExpr/*!*/)args[0])),
+ BoogieFactory.IExpr2Expr(cce.NonNull((AI.IExpr/*!*/)args[1])));
+ } else {
+ {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // If we are something wrong is happended
}
return retFun;
}
[Pure]
- public object DoVisit(AI.ExprVisitor! visitor)
- {
+ public object DoVisit(AI.ExprVisitor visitor) {
+ //Contract.Requires(visitor != null);
return visitor.VisitFunApp(this);
}
- public override Absy! StdDispatch(StandardVisitor! visitor)
- {
+ public override Absy StdDispatch(StandardVisitor visitor) {
+ //Contract.Requires(visitor != null);
+ Contract.Ensures(Contract.Result<Absy>() != null);
return visitor.VisitBvConcatExpr(this);
}
}
|