diff options
author | 2010-08-27 21:15:08 +0000 | |
---|---|---|
committer | 2010-08-27 21:15:08 +0000 | |
commit | c333ecd2f30badea143e79f5f944a8c63398b959 (patch) | |
tree | 28b04dc9f46d6fa90b4fdf38ffb24898bdc139b0 /Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs | |
parent | dce6bf46952b5dd470ae841cae03706dbc30bc3b (diff) |
Boogie: Removed some errors with code contracts (commenting out doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
Diffstat (limited to 'Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs')
-rw-r--r-- | Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs | 72 |
1 files changed, 36 insertions, 36 deletions
diff --git a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs index 60aceb7f..44abfed6 100644 --- a/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs +++ b/Source/AIFramework/Polyhedra/PolyhedraAbstraction.cs @@ -48,7 +48,7 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override void Dump(string/*!*/ msg) {
- Contract.Requires(msg != null);
+ //Contract.Requires(msg != null);
System.Console.WriteLine("PolyhedraLatticeElement.Dump({0}):", msg);
lcs.Dump();
}
@@ -107,13 +107,13 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override bool IsBottom(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
PolyhedraLatticeElement e = (PolyhedraLatticeElement)element;
return e.lcs.IsBottom();
}
public override bool IsTop(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
PolyhedraLatticeElement e = (PolyhedraLatticeElement)element;
return e.lcs.IsTop();
}
@@ -126,8 +126,8 @@ namespace Microsoft.AbstractInterpretationFramework { /// <returns></returns>
protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
{
- Contract.Requires(first != null);
- Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ //Contract.Requires(second != null);
PolyhedraLatticeElement a = (PolyhedraLatticeElement)first;
PolyhedraLatticeElement b = (PolyhedraLatticeElement)second;
return b.lcs.IsSubset(a.lcs);
@@ -135,13 +135,13 @@ namespace Microsoft.AbstractInterpretationFramework { public override string/*!*/ ToString(Element/*!*/ e) {
- Contract.Requires(e != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<string>() != null);
return ((PolyhedraLatticeElement)e).lcs.ToString();
}
public override IExpr/*!*/ ToPredicate(Element/*!*/ element) {
- Contract.Requires(element != null);
+ //Contract.Requires(element != null);
Contract.Ensures(Contract.Result<IExpr>() != null);
PolyhedraLatticeElement e = (PolyhedraLatticeElement)element;
return e.lcs.ConvertToExpression(factory);
@@ -150,8 +150,8 @@ namespace Microsoft.AbstractInterpretationFramework { public override Lattice.Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
- Contract.Requires(second != null);
- Contract.Requires(first != null);
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
Contract.Ensures(Contract.Result<Lattice.Element>() != null);
log.DbgMsg("Joining ...");
log.DbgMsgIndent();
@@ -165,8 +165,8 @@ namespace Microsoft.AbstractInterpretationFramework { public override Lattice.Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
- Contract.Requires(second != null);
- Contract.Requires(first != null);
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
Contract.Ensures(Contract.Result<Lattice.Element>() != null);
PolyhedraLatticeElement aa = (PolyhedraLatticeElement)first;
PolyhedraLatticeElement bb = (PolyhedraLatticeElement)second;
@@ -175,8 +175,8 @@ namespace Microsoft.AbstractInterpretationFramework { public override Lattice.Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
- Contract.Requires(second != null);
- Contract.Requires(first != null);
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
Contract.Ensures(Contract.Result<Lattice.Element>() != null);
log.DbgMsg("Widening ...");
log.DbgMsgIndent();
@@ -192,8 +192,8 @@ namespace Microsoft.AbstractInterpretationFramework { public override Element/*!*/ Eliminate(Element/*!*/ e, IVariable/*!*/ variable) {
- Contract.Requires(variable != null);
- Contract.Requires(e != null);
+ //Contract.Requires(variable != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
log.DbgMsg(string.Format("Eliminating {0} ...", variable));
@@ -206,9 +206,9 @@ namespace Microsoft.AbstractInterpretationFramework { public override Element/*!*/ Rename(Element/*!*/ e, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
- Contract.Requires(newName != null);
- Contract.Requires(oldName != null);
- Contract.Requires(e != null);
+ //Contract.Requires(newName != null);
+ //Contract.Requires(oldName != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
log.DbgMsg(string.Format("Renaming {0} to {1} in {2} ...", oldName, newName, this.ToString(e)));
@@ -220,8 +220,8 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
- Contract.Requires(args != null);
- Contract.Requires(f != null);
+ //Contract.Requires(args != null);
+ //Contract.Requires(f != null);
return f is IntSymbol ||
f.Equals(Int.Add) ||
f.Equals(Int.Sub) ||
@@ -237,9 +237,9 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2) {
- Contract.Requires(var2 != null);
- Contract.Requires(var1 != null);
- Contract.Requires(e != null);
+ //Contract.Requires(var2 != null);
+ //Contract.Requires(var1 != null);
+ //Contract.Requires(e != null);
PolyhedraLatticeElement/*!*/ ple = (PolyhedraLatticeElement)cce.NonNull(e);
Contract.Assume(ple.lcs.Constraints != null);
ArrayList /*LinearConstraint!*//*!*/ clist = (ArrayList /*LinearConstraint!*/)cce.NonNull(ple.lcs.Constraints.Clone());
@@ -257,8 +257,8 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred) {
- Contract.Requires(pred != null);
- Contract.Requires(e != null);
+ //Contract.Requires(pred != null);
+ //Contract.Requires(e != null);
PolyhedraLatticeElement/*!*/ ple = (PolyhedraLatticeElement)Constrain(e, pred);
Contract.Assert(ple != null);
if (ple.lcs.IsBottom()) {
@@ -295,7 +295,7 @@ namespace Microsoft.AbstractInterpretationFramework { [Pure]
public object DoVisit(ExprVisitor/*!*/ visitor) {
- Contract.Requires(visitor != null);
+ //Contract.Requires(visitor != null);
return visitor.VisitFunApp(this);
}
@@ -316,7 +316,7 @@ namespace Microsoft.AbstractInterpretationFramework { }
public IFunApp/*!*/ CloneWithArguments(IList/*<IExpr!>*//*!*/ args) {
- Contract.Requires(args != null);
+ //Contract.Requires(args != null);
Contract.Ensures(Contract.Result<IFunApp>() != null);
Contract.Assert(args.Count == 1);
return new PolyhedraLatticeNegation((IExpr/*!*/)cce.NonNull(args[0]));
@@ -324,19 +324,19 @@ namespace Microsoft.AbstractInterpretationFramework { }
public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars) {
- Contract.Requires(prohibitedVars != null);
- Contract.Requires(var != null);
- Contract.Requires(expr != null);
- Contract.Requires(q != null);
- Contract.Requires(e != null);
+ //Contract.Requires(prohibitedVars != null);
+ //Contract.Requires(var != null);
+ //Contract.Requires(expr != null);
+ //Contract.Requires(q != null);
+ //Contract.Requires(e != null);
// BUGBUG: TODO: this method can be implemented in a more precise way
return null;
}
public override Element/*!*/ Constrain(Element/*!*/ e, IExpr/*!*/ expr) {
- Contract.Requires(expr != null);
- Contract.Requires(e != null);
+ //Contract.Requires(expr != null);
+ //Contract.Requires(e != null);
Contract.Ensures(Contract.Result<Element>() != null);
log.DbgMsg(string.Format("Constraining with {0} into {1} ...", expr, this.ToString(e)));
@@ -387,7 +387,7 @@ namespace Microsoft.AbstractInterpretationFramework { class LCBottom : LinearCondition {
public override void AddToConstraintSystem(ArrayList/*!*/ /*LinearConstraint*/ clist) {
- Contract.Requires(clist != null);
+ //Contract.Requires(clist != null);
// make an unsatisfiable constraint
LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ);
lc.rhs = Rational.FromInt(1);
@@ -415,7 +415,7 @@ namespace Microsoft.AbstractInterpretationFramework { this.constraint = constraint;
}
public override void AddToConstraintSystem(ArrayList/*!*/ /*LinearConstraint*/ clist) {
- Contract.Requires(clist != null);
+ //Contract.Requires(clist != null);
if (positive) {
clist.Add(constraint);
} else {
|