diff options
Diffstat (limited to 'Source/AbsInt')
-rw-r--r-- | Source/AbsInt/IntervalDomain.cs | 8 | ||||
-rw-r--r-- | Source/AbsInt/Traverse.cs | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index c024a62a..0e095c44 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -658,7 +658,7 @@ namespace Microsoft.Boogie.AbstractInterpretation public override Expr VisitNAryExpr(NAryExpr node) {
if (node.Fun is UnaryOperator) {
var op = (UnaryOperator)node.Fun;
- Contract.Assert(node.Args.Length == 1);
+ Contract.Assert(node.Args.Count == 1);
if (op.Op == UnaryOperator.Opcode.Neg) {
BigInteger? lo, hi;
VisitExpr(node.Args[0]);
@@ -681,7 +681,7 @@ namespace Microsoft.Boogie.AbstractInterpretation }
} else if (node.Fun is BinaryOperator) {
var op = (BinaryOperator)node.Fun;
- Contract.Assert(node.Args.Length == 2);
+ Contract.Assert(node.Args.Count == 2);
BigInteger? lo0, hi0, lo1, hi1;
VisitExpr(node.Args[0]);
lo0 = Lo; hi0 = Hi;
@@ -837,7 +837,7 @@ namespace Microsoft.Boogie.AbstractInterpretation }
} else if (node.Fun is IfThenElse) {
var op = (IfThenElse)node.Fun;
- Contract.Assert(node.Args.Length == 3);
+ Contract.Assert(node.Args.Count == 3);
BigInteger? guardLo, guardHi, lo0, hi0, lo1, hi1;
VisitExpr(node.Args[0]);
guardLo = Lo; guardHi = Hi;
@@ -1037,7 +1037,7 @@ namespace Microsoft.Boogie.AbstractInterpretation public override Expr VisitNAryExpr(NAryExpr node) {
if (node.Fun is BinaryOperator) {
var op = (BinaryOperator)node.Fun;
- Contract.Assert(node.Args.Length == 2);
+ Contract.Assert(node.Args.Count == 2);
var arg0 = node.Args[0];
var arg1 = node.Args[1];
BigInteger? k;
diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs index a1e88656..633ad86e 100644 --- a/Source/AbsInt/Traverse.cs +++ b/Source/AbsInt/Traverse.cs @@ -88,7 +88,7 @@ namespace Microsoft.Boogie { //PM: The folowing assumption is needed because we cannot prove that a simple field update
//PM: leaves the value of a property unchanged.
- Contract.Assume(g.labelNames == null || g.labelNames.Length == g.labelTargets.Length);
+ Contract.Assume(g.labelNames == null || g.labelNames.Count == g.labelTargets.Count);
cce.EndExpose();
} else {
Contract.Assert(b.TransferCmd == null || b.TransferCmd is ReturnCmd); // It must be a returnCmd;
|