diff options
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 17 | ||||
| -rw-r--r-- | Test/tutorial/maximum.dfy.expect | 14 | ||||
| -rw-r--r-- | Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy (renamed from Test/wishlist/useless-casts-in-decreases-clauses.dfy) | 0 | ||||
| -rw-r--r-- | Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy.expect | 3 | ||||
| -rw-r--r-- | Test/wishlist/useless-casts-in-decreases-clauses.dfy.expect | 3 |
5 files changed, 23 insertions, 14 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 35c6cec4..c4ea0a5a 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -5182,6 +5182,7 @@ namespace Microsoft.Dafny { return s;
}
+
/// <summary>
/// Create a resolved expression of the form "CVT(e0) - CVT(e1)", where "CVT" is either "int" (if
/// e0.Type is an integer-based numeric type) or "real" (if e0.Type is a real-based numeric type).
@@ -5195,13 +5196,21 @@ namespace Microsoft.Dafny { Contract.Ensures(Contract.Result<Expression>() != null);
Type toType = e0.Type.IsNumericBased(Type.NumericPersuation.Int) ? (Type)Type.Int : Type.Real;
- e0 = new ConversionExpr(e0.tok, e0, toType);
- e0.Type = toType;
- e1 = new ConversionExpr(e1.tok, e1, toType);
- e1.Type = toType;
+ e0 = CastIfNeeded(e0, toType);
+ e1 = CastIfNeeded(e1, toType);
return CreateSubtract(e0, e1);
}
+ private static Expression CastIfNeeded(Expression expr, Type toType) {
+ if (!expr.Type.Equals(toType)) {
+ var cast = new ConversionExpr(expr.tok, expr, toType);
+ cast.Type = toType;
+ return cast;
+ } else {
+ return expr;
+ }
+ }
+
/// <summary>
/// Create a resolved expression of the form "e0 - e1"
/// </summary>
diff --git a/Test/tutorial/maximum.dfy.expect b/Test/tutorial/maximum.dfy.expect index 70768304..16a67088 100644 --- a/Test/tutorial/maximum.dfy.expect +++ b/Test/tutorial/maximum.dfy.expect @@ -1,7 +1,7 @@ -maximum.dfy(11,10): Info: Selected triggers: {values[i]} -maximum.dfy(18,14): Info: Selected triggers: {values[j]} -maximum.dfy(28,27): Info: Selected triggers: {values[i]} -maximum.dfy(29,27): Info: Selected triggers: {values[i]} -maximum.dfy(15,2): Info: decreases int(|values|) - int(idx) - -Dafny program verifier finished with 4 verified, 0 errors +maximum.dfy(11,10): Info: Selected triggers: {values[i]}
+maximum.dfy(18,14): Info: Selected triggers: {values[j]}
+maximum.dfy(28,27): Info: Selected triggers: {values[i]}
+maximum.dfy(29,27): Info: Selected triggers: {values[i]}
+maximum.dfy(15,2): Info: decreases |values| - idx
+
+Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/wishlist/useless-casts-in-decreases-clauses.dfy b/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy index 9b002d47..9b002d47 100644 --- a/Test/wishlist/useless-casts-in-decreases-clauses.dfy +++ b/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy diff --git a/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy.expect b/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy.expect new file mode 100644 index 00000000..36d7e6b8 --- /dev/null +++ b/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy.expect @@ -0,0 +1,3 @@ +useless-casts-in-decreases-clauses.dfy(6,2): Info: decreases pos - 0
+
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/wishlist/useless-casts-in-decreases-clauses.dfy.expect b/Test/wishlist/useless-casts-in-decreases-clauses.dfy.expect deleted file mode 100644 index e37b8b9b..00000000 --- a/Test/wishlist/useless-casts-in-decreases-clauses.dfy.expect +++ /dev/null @@ -1,3 +0,0 @@ -useless-casts-in-decreases-clauses.dfy(6,2): Info: decreases int(pos) - int(0)
-
-Dafny program verifier finished with 2 verified, 0 errors
|