diff options
| -rw-r--r-- | Source/Core/Absy.cs | 36 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 30 | ||||
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 6 | ||||
| -rw-r--r-- | Source/Core/AbsyQuant.cs | 37 | ||||
| -rw-r--r-- | Source/Core/AbsyType.cs | 20 | ||||
| -rw-r--r-- | Source/Core/BoogiePL.atg | 4 | ||||
| -rw-r--r-- | Source/Core/DeadVarElim.cs | 10 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 10 | ||||
| -rw-r--r-- | Source/Core/LoopUnroll.cs | 3 | ||||
| -rw-r--r-- | Source/Core/OOLongUtil.cs | 3 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 4 | ||||
| -rw-r--r-- | Source/Core/PureCollections.cs | 6 | ||||
| -rw-r--r-- | Source/Core/ResolutionContext.cs | 6 | ||||
| -rw-r--r-- | Source/Core/Util.cs | 16 | ||||
| -rw-r--r-- | Source/Core/VCExp.cs | 3 | ||||
| -rw-r--r-- | Source/Graph/Graph.cs | 3 | ||||
| -rw-r--r-- | Source/ParserHelper/ParserHelper.cs | 3 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprAST.cs | 1 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 2 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.cs | 1 |
20 files changed, 55 insertions, 149 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index c5534aba..8020f799 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -46,7 +46,6 @@ namespace Microsoft.Boogie.AbstractInterpretation { public ProcedureSummaryEntry() {
this.ReturnPoints = new HashSet<CallSite>();
- // base();
}
} // class
@@ -105,7 +104,6 @@ namespace Microsoft.Boogie { Contract.Requires(tok != null);
this.tok = tok;
this.uniqueId = AbsyNodeCount++;
- // base();
}
private static int AbsyNodeCount = 0;
@@ -187,7 +185,6 @@ namespace Microsoft.Boogie { public Program()
: base(Token.NoToken) {
this.TopLevelDeclarations = new List<Declaration>();
- // base(Token.NoToken);
}
public void Emit(TokenTextWriter stream) {
@@ -1062,23 +1059,20 @@ namespace Microsoft.Boogie { : this(tok, expr, null) {
Contract.Requires(expr != null);
Contract.Requires(tok != null);
- //:this(tok, expr, null);//BASEMOVEA
}
public Axiom(IToken/*!*/ tok, Expr/*!*/ expr, string comment)
- : base(tok) {//BASEMOVE DANGER
+ : base(tok) {
Contract.Requires(tok != null);
Contract.Requires(expr != null);
Expr = expr;
Comment = comment;
- // :base(tok);
}
public Axiom(IToken tok, Expr expr, string comment, QKeyValue kv)
- : this(tok, expr, comment) {//BASEMOVEA
+ : this(tok, expr, comment) {
Contract.Requires(expr != null);
Contract.Requires(tok != null);
- //:this(tok, expr, comment);
this.Attributes = kv;
}
@@ -1145,7 +1139,6 @@ namespace Microsoft.Boogie { Contract.Requires(tok != null);
Contract.Requires(name != null);
this.name = name;
- // base(tok);
}
[Pure]
public override string ToString() {
@@ -1377,7 +1370,6 @@ namespace Microsoft.Boogie { Contract.Requires(tok != null);
Contract.Requires(typedIdent != null);
this.TypedIdent = typedIdent;
- // base(tok, typedIdent.Name);
}
public Variable(IToken/*!*/ tok, TypedIdent/*!*/ typedIdent, QKeyValue kv)
@@ -1385,7 +1377,6 @@ namespace Microsoft.Boogie { Contract.Requires(tok != null);
Contract.Requires(typedIdent != null);
this.TypedIdent = typedIdent;
- // base(tok, typedIdent.Name);
this.Attributes = kv;
}
@@ -1480,7 +1471,6 @@ namespace Microsoft.Boogie { Contract.Requires(typedIdent != null);
Contract.Requires(typedIdent.Name != null && (!typedIdent.HasName || typedIdent.Name.Length > 0));
Contract.Requires(typedIdent.WhereExpr == null);
- // base(tok, typedIdent);
this.Unique = true;
this.Parents = null;
this.ChildrenComplete = false;
@@ -1491,7 +1481,6 @@ namespace Microsoft.Boogie { Contract.Requires(typedIdent != null);
Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);
Contract.Requires(typedIdent.WhereExpr == null);
- // base(tok, typedIdent);
this.Unique = unique;
this.Parents = null;
this.ChildrenComplete = false;
@@ -1506,7 +1495,6 @@ namespace Microsoft.Boogie { Contract.Requires(parents == null || cce.NonNullElements(parents));
Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);
Contract.Requires(typedIdent.WhereExpr == null);
- // base(tok, typedIdent);
this.Unique = unique;
this.Parents = parents;
this.ChildrenComplete = childrenComplete;
@@ -1668,16 +1656,14 @@ namespace Microsoft.Boogie { }
public class LocalVariable : Variable {
public LocalVariable(IToken tok, TypedIdent typedIdent, QKeyValue kv)
- : base(tok, typedIdent, kv) {//BASEMOVEA
+ : base(tok, typedIdent, kv) {
Contract.Requires(typedIdent != null);
Contract.Requires(tok != null);
- //:base(tok, typedIdent, kv);
}
public LocalVariable(IToken tok, TypedIdent typedIdent)
- : base(tok, typedIdent, null) {//BASEMOVEA
+ : base(tok, typedIdent, null) {
Contract.Requires(typedIdent != null);
Contract.Requires(tok != null);
- //:base(tok, typedIdent, null);
}
public override bool IsMutable {
get {
@@ -1709,11 +1695,10 @@ namespace Microsoft.Boogie { }
public class BoundVariable : Variable {
public BoundVariable(IToken tok, TypedIdent typedIdent)
- : base(tok, typedIdent) {//BASEMOVEA
+ : base(tok, typedIdent) {
Contract.Requires(typedIdent != null);
Contract.Requires(tok != null);
Contract.Requires(typedIdent.WhereExpr == null);
- //:base(tok, typedIdent); // here for aesthetic reasons
}
public override bool IsMutable {
get {
@@ -1754,7 +1739,6 @@ namespace Microsoft.Boogie { this.TypeParameters = typeParams;
this.InParams = inParams;
this.OutParams = outParams;
- // base(tok, name);
}
protected DeclWithFormals(DeclWithFormals that)
@@ -1763,7 +1747,6 @@ namespace Microsoft.Boogie { this.TypeParameters = that.TypeParameters;
this.InParams = that.InParams;
this.OutParams = that.OutParams;
- // base(that.tok, (!) that.Name);
}
protected void EmitSignature(TokenTextWriter stream, bool shortRet) {
@@ -1955,7 +1938,6 @@ namespace Microsoft.Boogie { Contract.Requires(name != null);
Contract.Requires(tok != null);
Comment = comment;
- // base(tok, name, args, new VariableSeq(result));
}
public Function(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq args, Variable result,
string comment, QKeyValue kv)
@@ -2102,7 +2084,6 @@ namespace Microsoft.Boogie { this.Condition = condition;
this.Comment = comment;
this.Attributes = kv;
- // base(token);
}
public Requires(IToken token, bool free, Expr condition, string comment)
@@ -2198,7 +2179,6 @@ namespace Microsoft.Boogie { this.Condition = condition;
this.Comment = comment;
this.Attributes = kv;
- // base(token);
}
public Ensures(IToken token, bool free, Expr condition, string comment)
@@ -2560,8 +2540,6 @@ namespace Microsoft.Boogie { BlockPredecessorsComputed = false;
scc = null;
Attributes = kv;
-
- // base(tok, name, inParams, outParams);
}
public Implementation(IToken tok, string name, TypeVariableSeq typeParams, VariableSeq inParams, VariableSeq outParams, VariableSeq localVariables, [Captured] List<Block/*!*/> block)
@@ -2595,8 +2573,6 @@ namespace Microsoft.Boogie { BlockPredecessorsComputed = false;
scc = null;
Attributes = kv;
-
- //base(tok, name, inParams, outParams);
}
public override void Emit(TokenTextWriter stream, int level) {
@@ -3021,7 +2997,6 @@ namespace Microsoft.Boogie { this.Name = name;
this.Type = type;
this.WhereExpr = whereExpr;
- // base(tok);
}
public bool HasName {
get {
@@ -3619,7 +3594,6 @@ namespace Microsoft.Boogie { public Choice(RESeq operands) {
Contract.Requires(operands != null);
rs = operands;
- // base();
}
public override void Emit(TokenTextWriter stream, int level) {
//Contract.Requires(stream != null);
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 607848ed..b1c213fa 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -689,7 +689,6 @@ namespace Microsoft.Boogie { this.thn = thn;
this.elseIf = elseIf;
this.elseBlock = elseBlock;
- // base(tok);
}
public override void Emit(TokenTextWriter stream, int level) {
@@ -742,7 +741,6 @@ namespace Microsoft.Boogie { this.Guard = guard;
this.Invariants = invariants;
this.Body = body;
- /// base(tok);
}
public override void Emit(TokenTextWriter stream, int level) {
@@ -779,7 +777,6 @@ namespace Microsoft.Boogie { : base(tok) {
Contract.Requires(tok != null);
this.Label = label;
- // base(tok);
}
public override void Emit(TokenTextWriter stream, int level) {
@@ -855,7 +852,6 @@ namespace Microsoft.Boogie { this.liveVarsBefore = null;
this.TraversingStatus = VisitState.ToVisit;
this.iterations = 0;
- // base(tok);
}
public void Emit(TokenTextWriter stream, int level) {
@@ -1076,7 +1072,6 @@ namespace Microsoft.Boogie { : base(Token.NoToken) {
Contract.Requires(c != null);
Comment = c;
- // base(Token.NoToken);
}
public override void Emit(TokenTextWriter stream, int level) {
@@ -1116,11 +1111,10 @@ namespace Microsoft.Boogie { public AssignCmd(IToken tok, List<AssignLhs/*!*/>/*!*/ lhss, List<Expr/*!*/>/*!*/ rhss)
- : base(tok) {//BASEMOVEA
+ : base(tok) {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(rhss));
Contract.Requires(cce.NonNullElements(lhss));
- //base(tok);
Lhss = lhss;
Rhss = rhss;
}
@@ -1333,7 +1327,6 @@ namespace Microsoft.Boogie { : base(tok) {
Contract.Requires(assignedVariable != null);
Contract.Requires(tok != null);
- //base(tok);
AssignedVariable = assignedVariable;
}
public override void Resolve(ResolutionContext rc) {
@@ -1413,8 +1406,7 @@ namespace Microsoft.Boogie { }
public MapAssignLhs(IToken tok, AssignLhs map, List<Expr/*!*/>/*!*/ indexes)
- : base(tok) {//BASEMOVEA
- //:base(tok);
+ : base(tok) {
Contract.Requires(map != null);
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(indexes));
@@ -1516,7 +1508,6 @@ namespace Microsoft.Boogie { Contract.Requires(tok != null);
this.Locals = locals;
this.Cmds = cmds;
- // base(tok);
}
public override void Resolve(ResolutionContext rc) {
@@ -1639,7 +1630,6 @@ namespace Microsoft.Boogie { protected CallCommonality(IToken tok, QKeyValue kv)
: base(tok) {
Contract.Requires(tok != null);
- //base(tok);
Attributes = kv;
}
@@ -1736,27 +1726,23 @@ namespace Microsoft.Boogie { //foreach (IdentifierExpr e in outs)
// if(e!=null)
// outsList.Add(e);
- //this(tok, callee, insList, outsList);
-
}
public CallCmd(IToken tok, string callee, List<Expr> ins, List<IdentifierExpr> outs)
- : base(tok, null) {//BASEMOVE DANGER
+ : base(tok, null) {
Contract.Requires(outs != null);
Contract.Requires(ins != null);
Contract.Requires(callee != null);
Contract.Requires(tok != null);
- //base(tok, null);
this.callee = callee;
this.Ins = ins;
this.Outs = outs;
}
public CallCmd(IToken tok, string callee, List<Expr> ins, List<IdentifierExpr> outs, QKeyValue kv)
- : base(tok, kv) {//BASEMOVE DANGER
+ : base(tok, kv) {
Contract.Requires(outs != null);
Contract.Requires(ins != null);
Contract.Requires(callee != null);
Contract.Requires(tok != null);
- //base(tok, kv);
this.callee = callee;
this.Ins = ins;
this.Outs = outs;
@@ -2212,20 +2198,18 @@ namespace Microsoft.Boogie { public TypeSeq InstantiatedTypes;
public CallForallCmd(IToken tok, string callee, List<Expr> ins)
- : base(tok, null) {//BASEMOVEA
+ : base(tok, null) {
Contract.Requires(ins != null);
Contract.Requires(callee != null);
Contract.Requires(tok != null);
- //:base(tok, null);
this.callee = callee;
this.Ins = ins;
}
public CallForallCmd(IToken tok, string callee, List<Expr> ins, QKeyValue kv)
- : base(tok, kv) {//BASEMOVEA
+ : base(tok, kv) {
Contract.Requires(ins != null);
Contract.Requires(callee != null);
Contract.Requires(tok != null);
- //:base(tok, kv);
this.callee = callee;
this.Ins = ins;
}
@@ -2681,7 +2665,6 @@ namespace Microsoft.Boogie { Contract.Requires(requires != null);
this.Call = call;
this.Requires = requires;
- // base(call.tok, @requires.Condition);
}
public override Absy StdDispatch(StandardVisitor visitor) {
@@ -2706,7 +2689,6 @@ namespace Microsoft.Boogie { : base(ens.tok, ens.Condition) {
Contract.Requires(ens != null);
this.Ensures = ens;
- // base(ens.tok, ens.Condition);
}
public override Absy StdDispatch(StandardVisitor visitor) {
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 5d7a404e..f8e64402 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -665,7 +665,6 @@ namespace Microsoft.Boogie { Contract.Requires(tok != null);
Contract.Requires(name != null);
Name = name;
- // base(tok);
}
/// <summary>
/// Creates an unresolved identifier expression.
@@ -680,7 +679,6 @@ namespace Microsoft.Boogie { Contract.Requires(type != null);
Name = name;
Type = type;
- // base(tok);
}
/// <summary>
@@ -695,7 +693,6 @@ namespace Microsoft.Boogie { Name = cce.NonNull(d.Name);
Decl = d;
Type = d.TypedIdent.Type;
- // base(tok);
}
[Pure]
[Reads(ReadsAttribute.Reads.Nothing)]
@@ -797,7 +794,6 @@ namespace Microsoft.Boogie { Contract.Requires(c != null);
Contract.Requires(ie != null);
this.identifierExpr = ie;
- // base();
}
}
@@ -2671,7 +2667,6 @@ namespace Microsoft.Boogie { Bitvector = bv;
Start = start;
End = end;
- // base(tok);
}
[Pure]
@@ -2771,7 +2766,6 @@ namespace Microsoft.Boogie { Contract.Requires(e1 != null);
E0 = e0;
E1 = e1;
- // base(tok);
}
[Pure]
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 05fdb7e4..2a9f8414 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -59,14 +59,13 @@ namespace Microsoft.Boogie { public BinderExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParameters,
VariableSeq/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)
- : base(tok)//BASEMOVEA
+ : base(tok)
{
Contract.Requires(tok != null);
Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
Contract.Requires(dummies.Length + typeParameters.Length > 0);
- //base(tok);
TypeParameters = typeParameters;
Dummies = dummies;
Attributes = kv;
@@ -217,11 +216,10 @@ namespace Microsoft.Boogie { public QKeyValue(IToken tok, string key, [Captured] List<object/*!*/>/*!*/ parameters, QKeyValue next)
- : base(tok) {//BASEMOVEA
+ : base(tok) {
Contract.Requires(key != null);
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(parameters));
- //:base(tok);
Key = key;
Params = parameters;
Next = next;
@@ -338,12 +336,11 @@ namespace Microsoft.Boogie { public Trigger Next;
public Trigger(IToken tok, bool pos, ExprSeq tr)
- : this(tok, pos, tr, null) {//BASEMOVEA
+ : this(tok, pos, tr, null) {
Contract.Requires(tr != null);
Contract.Requires(tok != null);
Contract.Requires(1 <= tr.Length);
Contract.Requires(pos || tr.Length == 1);
- //:this(tok, pos, tr, null);
}
public Trigger(IToken/*!*/ tok, bool pos, ExprSeq/*!*/ tr, Trigger next)
@@ -355,7 +352,6 @@ namespace Microsoft.Boogie { this.Pos = pos;
this.Tr = tr;
this.Next = next;
- // base(tok);
}
public void Emit(TokenTextWriter stream) {
@@ -426,38 +422,34 @@ namespace Microsoft.Boogie { public class ForallExpr : QuantifierExpr {
public ForallExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParams,
VariableSeq/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)
- : base(tok, typeParams, dummies, kv, triggers, body) {//BASEMOVEA
+ : base(tok, typeParams, dummies, kv, triggers, body) {
Contract.Requires(tok != null);
Contract.Requires(typeParams != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
Contract.Requires(dummies.Length + typeParams.Length > 0);
- //:base(tok, typeParams, dummies, kv, triggers, body); // here for aesthetic reasons
}
public ForallExpr(IToken tok, VariableSeq dummies, Trigger triggers, Expr body)
- : base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {//BASEMOVEA
+ : base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(tok != null);
Contract.Requires(dummies.Length > 0);
- //:base(tok, new TypeVariableSeq(), dummies, null, triggers, body); // here for aesthetic reasons
}
public ForallExpr(IToken tok, VariableSeq dummies, Expr body)
- : base(tok, new TypeVariableSeq(), dummies, null, null, body) {//BASEMOVEA
+ : base(tok, new TypeVariableSeq(), dummies, null, null, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(tok != null);
Contract.Requires(dummies.Length > 0);
- //:base(tok, new TypeVariableSeq(), dummies, null, null, body); // here for aesthetic reasons
}
public ForallExpr(IToken tok, TypeVariableSeq typeParams, VariableSeq dummies, Expr body)
- : base(tok, typeParams, dummies, null, null, body) {//BASEMOVEA
+ : base(tok, typeParams, dummies, null, null, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(typeParams != null);
Contract.Requires(tok != null);
Contract.Requires(dummies.Length + typeParams.Length > 0);
- //:base(tok, typeParams, dummies, null, null, body); // here for aesthetic reasons
}
public override Absy StdDispatch(StandardVisitor visitor) {
@@ -476,29 +468,26 @@ namespace Microsoft.Boogie { public class ExistsExpr : QuantifierExpr {
public ExistsExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ dummies,
QKeyValue kv, Trigger triggers, Expr/*!*/ body)
- : base(tok, typeParams, dummies, kv, triggers, body) {//BASEMOVEA
+ : base(tok, typeParams, dummies, kv, triggers, body) {
Contract.Requires(tok != null);
Contract.Requires(typeParams != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
Contract.Requires(dummies.Length + typeParams.Length > 0);
- //:base(tok, typeParams, dummies, kv, triggers, body); // here for aesthetic reasons
}
public ExistsExpr(IToken tok, VariableSeq dummies, Trigger triggers, Expr body)
- : base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {//BASEMOVEA
+ : base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(tok != null);
Contract.Requires(dummies.Length > 0);
- //:base(tok, new TypeVariableSeq(), dummies, null, triggers, body); // here for aesthetic reasons
}
public ExistsExpr(IToken tok, VariableSeq dummies, Expr body)
- : base(tok, new TypeVariableSeq(), dummies, null, null, body) {//BASEMOVEA
+ : base(tok, new TypeVariableSeq(), dummies, null, null, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(tok != null);
Contract.Requires(dummies.Length > 0);
- //:base(tok, new TypeVariableSeq(), dummies, null, null, body); // here for aesthetic reasons
}
public override Absy StdDispatch(StandardVisitor visitor) {
@@ -527,13 +516,12 @@ namespace Microsoft.Boogie { public QuantifierExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParameters,
VariableSeq/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body)
- : base(tok, typeParameters, dummies, kv, body) {//BASEMOVEA
+ : base(tok, typeParameters, dummies, kv, body) {
Contract.Requires(tok != null);
Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
Contract.Requires(dummies.Length + typeParameters.Length > 0);
- //:base(tok, typeParameters, dummies, kv, body);
Contract.Assert((this is ForallExpr) || (this is ExistsExpr));
@@ -709,13 +697,12 @@ namespace Microsoft.Boogie { public class LambdaExpr : BinderExpr {
public LambdaExpr(IToken/*!*/ tok, TypeVariableSeq/*!*/ typeParameters,
VariableSeq/*!*/ dummies, QKeyValue kv, Expr/*!*/ body)
- : base(tok, typeParameters, dummies, kv, body) {//BASEMOVEA
+ : base(tok, typeParameters, dummies, kv, body) {
Contract.Requires(tok != null);
Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
Contract.Requires(dummies.Length + typeParameters.Length > 0);
- //:base(tok, typeParameters, dummies, kv, body);
}
public override BinderKind Kind {
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index d78e0d34..8c355f72 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -831,12 +831,10 @@ namespace Microsoft.Boogie { : base(token) {
Contract.Requires(token != null);
T = t;
- // base(token);
}
public BasicType(SimpleType t)
: base(Token.NoToken) {
T = t;
- // base(Token.NoToken);
}
//----------- Cloning ----------------------------------
@@ -1687,13 +1685,12 @@ Contract.Requires(that != null); }
protected TypeProxy(IToken token, string givenName, string kind)
- : base(token) {//BASEMOVE DANGER
+ : base(token) {
Contract.Requires(kind != null);
Contract.Requires(givenName != null);
Contract.Requires(token != null);
Name = givenName + "$" + kind + "#" + proxies;
proxies++;
- //:base(token);
}
private Type proxyFor;
@@ -2047,10 +2044,9 @@ Contract.Requires(that != null); }
public BvTypeProxy(IToken token, string name, int minBits)
- : base(token, name, "bv" + minBits + "proxy") {//BASEMOVEA
+ : base(token, name, "bv" + minBits + "proxy") {
Contract.Requires(name != null);
Contract.Requires(token != null);
- //base(token, name, "bv" + minBits + "proxy");
this.MinBits = minBits;
}
@@ -2059,13 +2055,12 @@ Contract.Requires(that != null); /// be constructed.
/// </summary>
public BvTypeProxy(IToken token, string name, Type t0, Type t1)
- : base(token, name, "bvproxy") {//BASEMOVEA
+ : base(token, name, "bvproxy") {
Contract.Requires(t1 != null);
Contract.Requires(t0 != null);
Contract.Requires(name != null);
Contract.Requires(token != null);
Contract.Requires(t0.IsBv && t1.IsBv);
- //:base(token, name, "bvproxy");
t0 = FollowProxy(t0);
t1 = FollowProxy(t1);
this.MinBits = MinBitsFor(t0) + MinBitsFor(t1);
@@ -2078,19 +2073,17 @@ Contract.Requires(that != null); /// Construct a BvTypeProxy like p, but with minBits.
/// </summary>
private BvTypeProxy(BvTypeProxy p, int minBits)
- : base(p.tok, p.Name, "") {//BASEMOVEA
+ : base(p.tok, p.Name, "") {
Contract.Requires(p != null);
- //:base(p.tok, p.Name, "");
this.MinBits = minBits;
this.constraints = p.constraints;
}
private BvTypeProxy(IToken token, string name, int minBits, List<BvTypeConstraint/*!*/> constraints)
- : base(token, name, "") {//BASEMOVEA
+ : base(token, name, "") {
Contract.Requires(cce.NonNullElements(constraints, true));
Contract.Requires(name != null);
Contract.Requires(token != null);
- //:base(token, name, "");
this.MinBits = minBits;
this.constraints = constraints;
}
@@ -2331,11 +2324,10 @@ Contract.Requires(that != null); }
public MapTypeProxy(IToken token, string name, int arity)
- : base(token, name, "mapproxy") {//BASEMOVEA
+ : base(token, name, "mapproxy") {
Contract.Requires(name != null);
Contract.Requires(token != null);
Contract.Requires(0 <= arity);
- //:base(token, name, "mapproxy");
this.Arity = arity;
}
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 96ba9824..d5a1df2d 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -97,9 +97,9 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation) private class BvBounds : Expr {
public BigNum Lower;
public BigNum Upper;
- public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper) :base(tok){//BASEMOVE
+ public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper)
+ : base(tok) {
Contract.Requires(tok != null);
- //:base(tok);
this.Lower = lower;
this.Upper = upper;
}
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 5bf306b6..d51fcdb3 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -14,7 +14,7 @@ namespace Microsoft.Boogie { }
private UnusedVarEliminator()
- : base() {//BasemoveA
+ : base() {
}
@@ -670,7 +670,7 @@ namespace Microsoft.Boogie { [NotDelayed]
- public ICFG(Implementation impl) {//BASEMOVE DANGER
+ public ICFG(Implementation impl) {
Contract.Requires(impl != null);
this.graph = new Graph<Block/*!*/>();
this.procsCalled = new Dictionary<string/*!*/, List<Block/*!*/>/*!*/>();
@@ -691,8 +691,6 @@ namespace Microsoft.Boogie { summary = GenKillWeight.zero();
this.impl = impl;
- //:base();
-
Initialize(impl);
}
@@ -836,7 +834,7 @@ namespace Microsoft.Boogie { [NotDelayed]
- public InterProcGenKill(Implementation impl, Program program) {//BASEMOVE DANGER
+ public InterProcGenKill(Implementation impl, Program program) {
Contract.Requires(program != null);
Contract.Requires(impl != null);
this.program = program;
@@ -854,8 +852,6 @@ namespace Microsoft.Boogie { varsLiveAtEntry.Clear();
varsLiveSummary.Clear();
- //base();
-
foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {
Contract.Assert(decl != null);
if (decl is Implementation) {
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 0445be1a..36f54402 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -375,9 +375,9 @@ namespace Microsoft.Boogie { }
public CreateSubstitutionClosure(Hashtable/*Variable!->Expr!*/ map)
- : base() {//BASEMOVE DANGER
+ : base() {
Contract.Requires(map != null);
- this.map = map; //:base();
+ this.map = map;
}
public Expr/*?*/ Method(Variable v) {
Contract.Requires(v != null);
@@ -447,10 +447,9 @@ namespace Microsoft.Boogie { }
public NormalSubstituter(Substitution subst)
- : base() {//BASEMOVE DANGER
+ : base() {
Contract.Requires(subst != null);
this.subst = subst;
- //:base();
}
public override Expr VisitIdentifierExpr(IdentifierExpr node) {
@@ -471,12 +470,11 @@ namespace Microsoft.Boogie { }
public ReplacingOldSubstituter(Substitution always, Substitution forold)
- : base() {//BASEMOVE DANGER
+ : base() {
Contract.Requires(forold != null);
Contract.Requires(always != null);
this.always = always;
this.forold = forold;
- //:base();
}
private bool insideOldExpr = false;
diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs index ed523840..403f6ff4 100644 --- a/Source/Core/LoopUnroll.cs +++ b/Source/Core/LoopUnroll.cs @@ -187,14 +187,13 @@ namespace Microsoft.Boogie { [NotDelayed]
private LoopUnroll(int unrollMaxDepth, bool soundLoopUnrolling, Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>>/*!*/ scc, List<Block/*!*/>/*!*/ newBlockSeqGlobal)
- : base() {//BASEMOVE DANGER
+ : base() {
Contract.Requires(cce.NonNullElements(newBlockSeqGlobal));
Contract.Requires(cce.NonNullDictionaryAndValues(scc) && Contract.ForAll(scc.Values, v => cce.NonNullElements(v)));
Contract.Requires(0 <= unrollMaxDepth);
this.newBlockSeqGlobal = newBlockSeqGlobal;
this.c = unrollMaxDepth;
this.containingSCC = scc;
- //:base();
this.head = this;
if (unrollMaxDepth != 0) {
next = new LoopUnroll(unrollMaxDepth - 1, soundLoopUnrolling, scc, newBlockSeqGlobal, this);
diff --git a/Source/Core/OOLongUtil.cs b/Source/Core/OOLongUtil.cs index 1b3a68ad..474cb800 100644 --- a/Source/Core/OOLongUtil.cs +++ b/Source/Core/OOLongUtil.cs @@ -152,10 +152,9 @@ namespace Boogie.Util { public IfdefReader([Captured] TextReader reader, [Captured] List<string/*!*/>/*!*/ defines)
- : base(reader) {//BASEMOVEA
+ : base(reader) {
Contract.Requires(reader != null);
Contract.Requires(cce.NonNullElements(defines));
- //:base(reader);
this.defines = defines;
}
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 0a10b0a1..aaa6d0d3 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -117,9 +117,9 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation) private class BvBounds : Expr {
public BigNum Lower;
public BigNum Upper;
- public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper) :base(tok){//BASEMOVE
+ public BvBounds(IToken/*!*/ tok, BigNum lower, BigNum upper)
+ : base(tok) {
Contract.Requires(tok != null);
- //:base(tok);
this.Lower = lower;
this.Upper = upper;
}
diff --git a/Source/Core/PureCollections.cs b/Source/Core/PureCollections.cs index a77f59a1..15a6c629 100644 --- a/Source/Core/PureCollections.cs +++ b/Source/Core/PureCollections.cs @@ -247,11 +247,10 @@ namespace PureCollections { [NotDelayed]
public Map(params Pair[] ps)
- : base() {//BASEMOVE DANGER
+ : base() {
Contract.Requires(ps != null);
elems = new Object[ps.Length * 2];
vals = new Object[ps.Length * 2];
- //base();
card = 0;
for (int i = 0; i < ps.Length; i++)
Insert(cce.NonNull(ps[i]).First, cce.NonNull(ps[i]).Second);
@@ -548,9 +547,8 @@ namespace PureCollections { elems = ds;
}
public Sequence(Sequence seq)
- : base(seq) {//BASEMOVEA
+ : base(seq) {
Contract.Requires(seq != null);
- //base(seq);
}
public Sequence(Capacity c) {
elems = new object[c.capacity];
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index 128df8c5..5711e33e 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -133,8 +133,7 @@ namespace Microsoft.Boogie { public class ResolutionContext : CheckingContext {
public ResolutionContext(IErrorSink errorSink)
- : base(errorSink) {//BASEMOVEA
- //:base(errorSink);
+ : base(errorSink) {
}
// ------------------------------ Boogie 2 Types -------------------------
@@ -558,8 +557,7 @@ namespace Microsoft.Boogie { public IdentifierExprSeq Frame; // used in checking the assignment targets of implementation bodies
public TypecheckingContext(IErrorSink errorSink)
- : base(errorSink) {//BASEMOVEA
- //:base(errorSink);
+ : base(errorSink) {
}
public bool InFrame(Variable v) {
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index 9a7fec0c..2aaae096 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -165,47 +165,43 @@ namespace Microsoft.Boogie { }
}
- public TokenTextWriter(string filename) :base(){//BASEMOVE DANGER
+ public TokenTextWriter(string filename)
+ : base() {
Contract.Requires(filename != null);
this.filename = filename;
this.writer = new StreamWriter(filename);
- //base();
}
public TokenTextWriter(string filename, bool setTokens)
- : base() {//BASEMOVE DANGER
+ : base() {
Contract.Requires(filename != null);
this.filename = filename;
this.writer = new StreamWriter(filename);
this.setTokens = setTokens;
- //base();
}
public TokenTextWriter(string filename, TextWriter writer, bool setTokens)
- : base() {//BASEMOVE DANGER
+ : base() {
Contract.Requires(writer != null);
Contract.Requires(filename != null);
this.filename = filename;
this.writer = writer;
this.setTokens = setTokens;
- //base();
}
public TokenTextWriter(string filename, TextWriter writer)
- : base() {//BASEMOVE DANGER
+ : base() {
Contract.Requires(writer != null);
Contract.Requires(filename != null);
this.filename = filename;
this.writer = writer;
- //base();
}
public TokenTextWriter(TextWriter writer)
- : base() {//BASEMOVE DANGER
+ : base() {
Contract.Requires(writer != null);
this.filename = "<no file>";
this.writer = writer;
- //base();
}
public void Write(string text) {
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs index 1e82224c..32336aac 100644 --- a/Source/Core/VCExp.cs +++ b/Source/Core/VCExp.cs @@ -16,9 +16,8 @@ namespace Microsoft.Boogie { public class ProverOptions {
public class OptionException : Exception {
public OptionException(string msg)
- : base(msg) {//BASEMOVEA
+ : base(msg) {
Contract.Requires(msg != null);
- //:base(msg);
}
}
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 947a5882..10c15b40 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -1118,7 +1118,7 @@ namespace Microsoft.Boogie.GraphUtil { [NotDelayed]
public StronglyConnectedComponents(System.Collections.IEnumerable/*<Node!>*/ graph, Adjacency<Node> preds, Adjacency<Node> succs)
: base()
- {//BASEMOVE DANGER
+ {
Contract.Requires(succs != null);
Contract.Requires(preds != null);
Contract.Requires(graph != null);
@@ -1133,7 +1133,6 @@ namespace Microsoft.Boogie.GraphUtil { this.graph = dict;
this.preds = preds;
this.succs = succs;
- //:base();
}
[Pure]
diff --git a/Source/ParserHelper/ParserHelper.cs b/Source/ParserHelper/ParserHelper.cs index a24343c9..111b836b 100644 --- a/Source/ParserHelper/ParserHelper.cs +++ b/Source/ParserHelper/ParserHelper.cs @@ -53,11 +53,10 @@ namespace Microsoft.Boogie { this._val = "anything so that it is nonnull";
}
public Token(int linenum, int colnum)
- : base() {//BASEMOVE DANGER
+ : base() {
this._line = linenum;
this._col = colnum;
this._val = "anything so that it is nonnull";
- //:base();
}
public int kind {
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index fcfd0041..82bdebbe 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -1202,7 +1202,6 @@ namespace Microsoft.Boogie.VCExprAST { : base(op) {
Contract.Requires(op != null);
Contract.Requires(cce.NonNullElements(arguments));
- //this(op, arguments, EMPTY_TYPE_LIST);
this.Arguments = arguments;
this.TypeArgumentsAttr = EMPTY_TYPE_LIST;
this.ExprType = op.InferType(arguments, TypeArgumentsAttr);
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index ec5fab25..fe4b4b99 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -182,8 +182,6 @@ namespace Microsoft.Boogie { this.thmProver = prover;
this.gen = prover.VCExprGen;
-
- // base();
}
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index eb1ce4e1..d82310ee 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -30,7 +30,6 @@ namespace VC { Contract.Requires(ctxt != null);
this.Label2absy = label2absy;
this.Ctxt = ctxt;
- // base();
}
public VCContext(Hashtable/*<int, Absy!>*/ label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr)
|