From 5623306213e01e8d667a7893cb0c3275ecfbf065 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 22 Aug 2015 13:44:42 -0700 Subject: Add a 'tutorial' folder to the distribution, with an initial example. It would be nice to gather neat Dafny examples there; each new feature could have its own small file that demoes it, and we could also have examples that showcase stuff that we think is impressive. I'm adding this as a test folder, because it's important to check that these cool examples don't break, but the focus probably shouldn't be on exhaustively testing the features being demoed. --- Test/tutorial/maximum.dfy.expect | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 Test/tutorial/maximum.dfy.expect (limited to 'Test/tutorial/maximum.dfy.expect') diff --git a/Test/tutorial/maximum.dfy.expect b/Test/tutorial/maximum.dfy.expect new file mode 100644 index 00000000..70768304 --- /dev/null +++ b/Test/tutorial/maximum.dfy.expect @@ -0,0 +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 -- cgit v1.2.3 From 2142e51d713394d384b0f33c1189f633dcbe301a Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 22 Aug 2015 20:15:34 -0700 Subject: Grant "wishlist/useless-casts-in-decreases-clauses.dfy" --- Source/Dafny/DafnyAst.cs | 17 +++++++++++++---- Test/tutorial/maximum.dfy.expect | 14 +++++++------- .../granted/useless-casts-in-decreases-clauses.dfy | 9 +++++++++ .../useless-casts-in-decreases-clauses.dfy.expect | 3 +++ Test/wishlist/useless-casts-in-decreases-clauses.dfy | 9 --------- .../useless-casts-in-decreases-clauses.dfy.expect | 3 --- 6 files changed, 32 insertions(+), 23 deletions(-) create mode 100644 Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy create mode 100644 Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy.expect delete mode 100644 Test/wishlist/useless-casts-in-decreases-clauses.dfy delete mode 100644 Test/wishlist/useless-casts-in-decreases-clauses.dfy.expect (limited to 'Test/tutorial/maximum.dfy.expect') 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; } + /// /// 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() != 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; + } + } + /// /// Create a resolved expression of the form "e0 - e1" /// 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/granted/useless-casts-in-decreases-clauses.dfy b/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy new file mode 100644 index 00000000..9b002d47 --- /dev/null +++ b/Test/wishlist/granted/useless-casts-in-decreases-clauses.dfy @@ -0,0 +1,9 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method M() { + var pos := 10; + while (pos > 0) { // This shouldn't print int(pos) - int(0); pos - 0 would be better + pos := pos - 1; + } +} 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 b/Test/wishlist/useless-casts-in-decreases-clauses.dfy deleted file mode 100644 index 9b002d47..00000000 --- a/Test/wishlist/useless-casts-in-decreases-clauses.dfy +++ /dev/null @@ -1,9 +0,0 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /printTooltips "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -method M() { - var pos := 10; - while (pos > 0) { // This shouldn't print int(pos) - int(0); pos - 0 would be better - pos := pos - 1; - } -} 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 -- cgit v1.2.3