dafny-lang · davidcok · Sep 26, 2022 · Jul 14, 2022 · Jul 14, 2022 · Jul 14, 2022
diff --git a/Makefile b/Makefile
@@ -35,6 +35,7 @@ clean:
 	(cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
 	(cd ${DIR} ; dotnet build Source/Dafny.sln -v:q --nologo -target:clean )
 	make -C ${DIR}/Source/DafnyCore -f Makefile clean
+	(cd ${DIR}/Source/Dafny && rm -rf Scanner.cs Parser.cs obj )
 	(cd ${DIR}/Source/DafnyRuntime/DafnyRuntimeJava; ./gradlew clean)
 	make -C ${DIR}/docs/DafnyRef clean
 	(cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)

diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg
@@ -2774,7 +2774,9 @@ SkeletonStmt<out Statement s>
 = (. IToken dotdotdot; .)
   ellipsis                             (. dotdotdot = t; .)
   ";"
-  (. s = new SkeletonStatement(dotdotdot, t); .)
+  (. s = new SkeletonStatement(dotdotdot, t); 
+     errors.Deprecated(t, "the ... refinement feature in statements is deprecated");
+  .)
   .
 
 /*------------------------------------------------------------------------*/
@@ -3085,7 +3087,9 @@ IfStmt<out Statement/*!*/ ifStmt>
     ( IF(IsBindingGuard())
       BindingGuard<out guard, true>      (. isBindingGuard = true; .)
     | Guard<out guard>
-    | ellipsis                           (. guardEllipsis = t; .)
+    | ellipsis                           (. guardEllipsis = t;
+                                            errors.Deprecated(t, "the ... refinement feature in statements is deprecated");
+                                         .)
     )
     BlockStmt<out thn, out bodyStart, out bodyEnd>    (. endTok = thn.EndTok; .)
     [ "else"
@@ -3182,13 +3186,17 @@ WhileStmt<out Statement stmt>
     (. stmt = new AlternativeLoopStmt(x, endTok, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), alternatives, usesOptionalBraces, attrs); .)
   |
     ( Guard<out guard>           (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
-    | ellipsis                   (. guardEllipsis = t; .)
+    | ellipsis                   (. guardEllipsis = t; 
+                                    errors.Deprecated(t, "the ... refinement feature in statements is deprecated");
+                                 .)
     )
     LoopSpec<invariants, decreases, ref mod, ref decAttrs, ref modAttrs>
     ( IF(la.kind == _lbrace)      /* if there's an open brace, claim it as the beginning of the loop body (as opposed to a BlockStmt following the loop) */
       BlockStmt<out body, out bodyStart, out bodyEnd>  (. endTok = body.EndTok; isDirtyLoop = false; .)
     | IF(la.kind == _ellipsis)    /* if there's an ellipsis, claim it as standing for the loop body (as opposed to a "...;" statement following the loop) */
-      ellipsis                   (. bodyEllipsis = t; endTok = t; isDirtyLoop = false; .)
+      ellipsis                   (. bodyEllipsis = t; endTok = t; isDirtyLoop = false;
+                                    errors.Deprecated(t, "the ... refinement feature in statements is deprecated");
+                                  .)
     | /* go body-less */
     )
     (.
@@ -3429,7 +3437,9 @@ AssertStmt<out Statement/*!*/ s, bool inExprContext>
       BlockStmt<out proof, out proofStart, out proofEnd>
     | ";"
     )
-  | ellipsis                                   (. dotdotdot = t; .)
+  | ellipsis                                   (. dotdotdot = t; 
+                                                  errors.Deprecated(t, "the ... refinement feature in statements is deprecated");
+                                                .)
     ";"
   )
   (. if (dotdotdot != null) {
@@ -3449,7 +3459,9 @@ ExpectStmt<out Statement/*!*/ s>
   "expect"                                     (. x = t; .)
   { Attribute<ref attrs> }
   ( Expression<out e, false, true>
-  | ellipsis                                   (. dotdotdot = t; .)
+  | ellipsis                                   (. dotdotdot = t; 
+                                                  errors.Deprecated(t, "the ... refinement feature in statements is deprecated");
+                                                .)
   )
   [ "," Expression<out m, false, true> ]
   ";"
@@ -3470,7 +3482,9 @@ AssumeStmt<out Statement/*!*/ s>
   "assume"                                     (. x = t; .)
   { Attribute<ref attrs> }
   ( Expression<out e, false, true>
-  | ellipsis                                   (. dotdotdot = t; .)
+  | ellipsis                                   (. dotdotdot = t; 
+                                                  errors.Deprecated(t, "the ... refinement feature in statements is deprecated");
+                                                .)
   )
   ";"
   (. if (dotdotdot != null) {
@@ -3564,7 +3578,9 @@ ModifyStmt<out Statement s>
   ( FrameExpression<out fe, false, true>       (. mod.Add(fe); .)
     { "," FrameExpression<out fe, false, true> (. mod.Add(fe); .)
     }
-  | ellipsis                            (. ellipsisToken = t; .)
+  | ellipsis                            (. ellipsisToken = t; 
+                                           errors.Deprecated(t, "the ... refinement feature in statements is deprecated");
+                                         .)
   )
   ( BlockStmt<out body, out bodyStart, out endTok>
   | SYNC ";"         (. endTok = t; .)

diff --git a/Test/allocated1/dafny0/Refinement.dfy.expect b/Test/allocated1/dafny0/Refinement.dfy.expect
@@ -1,3 +1,19 @@
+Refinement.dfy(156,13): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(161,9): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(162,13): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(167,13): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(198,13): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(203,9): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(204,13): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(209,13): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(252,11): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(255,7): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(259,7): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(260,10): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(262,9): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(264,7): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(269,7): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(276,7): Warning: the ... refinement feature in statements is deprecated
 Refinement.dfy(233,4): Warning: note, this loop has no body (loop frame: i)
 Refinement.dfy(15,4): Error: A postcondition might not hold on this return path.
 Refinement.dfy(14,16): Related location: This is the postcondition that might not hold.

diff --git a/Test/allocated1/dafny0/Simple.dfy.expect b/Test/allocated1/dafny0/Simple.dfy.expect
@@ -1,3 +1,5 @@
+Simple.dfy(98,7): Warning: the ... refinement feature in statements is deprecated
+Simple.dfy(101,7): Warning: the ... refinement feature in statements is deprecated
 // Simple.dfy
 
 lemma M(x: int)

diff --git a/Test/allocated1/dafny0/Skeletons.dfy.expect b/Test/allocated1/dafny0/Skeletons.dfy.expect
@@ -1,3 +1,10 @@
+Skeletons.dfy(27,11): Warning: the ... refinement feature in statements is deprecated
+Skeletons.dfy(29,11): Warning: the ... refinement feature in statements is deprecated
+Skeletons.dfy(31,7): Warning: the ... refinement feature in statements is deprecated
+Skeletons.dfy(32,10): Warning: the ... refinement feature in statements is deprecated
+Skeletons.dfy(60,7): Warning: the ... refinement feature in statements is deprecated
+Skeletons.dfy(62,6): Warning: the ... refinement feature in statements is deprecated
+Skeletons.dfy(64,7): Warning: the ... refinement feature in statements is deprecated
 Skeletons.dfy(45,2): Error: A postcondition might not hold on this return path.
 Skeletons.dfy(44,14): Related location: This is the postcondition that might not hold.
 

diff --git a/Test/allocated1/dafny0/Superposition.dfy.expect b/Test/allocated1/dafny0/Superposition.dfy.expect
@@ -1,3 +1,4 @@
+Superposition.dfy(38,9): Warning: the ... refinement feature in statements is deprecated
 
 Verifying M0.C.M (correctness) ...
   [4 proof obligations]  verified

diff --git a/Test/allocated1/dafny0/Termination.dfy.expect b/Test/allocated1/dafny0/Termination.dfy.expect
@@ -1,3 +1,4 @@
+Termination.dfy(450,7): Warning: the ... refinement feature in statements is deprecated
 Termination.dfy[TerminationRefinement1](441,5): Error: decreases clause might not decrease
 Termination.dfy(108,2): Error: cannot prove termination; try supplying a decreases clause for the loop
 Termination.dfy(125,2): Error: decreases expression might not decrease

diff --git a/Test/allocated1/dafny1/SchorrWaite-stages.dfy.expect b/Test/allocated1/dafny1/SchorrWaite-stages.dfy.expect
@@ -1,2 +1,23 @@
+SchorrWaite-stages.dfy(150,7): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(151,10): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(162,9): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(163,16): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(165,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(169,15): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(175,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(176,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(202,7): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(203,10): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(222,9): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(224,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(226,16): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(231,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(237,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(240,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(256,7): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(257,10): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(261,9): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(262,16): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(264,11): Warning: the ... refinement feature in statements is deprecated
 
 Dafny program verifier finished with 7 verified, 0 errors
diff --git a/Test/dafny0/DividedConstructors.dfy.expect b/Test/dafny0/DividedConstructors.dfy.expect
@@ -1,3 +1,4 @@
+DividedConstructors.dfy(62,9): Warning: the ... refinement feature in statements is deprecated
 // DividedConstructors.dfy
 
 

diff --git a/Test/dafny0/Include.dfy.expect b/Test/dafny0/Include.dfy.expect
@@ -1,3 +1,4 @@
+Include.dfy(31,7): Warning: the ... refinement feature in statements is deprecated
 Include.dfy(19,18): Error: A postcondition might not hold on this return path.
 Includee.dfy(17,19): Related location: This is the postcondition that might not hold.
 Includee.dfy[Concrete](22,15): Error: assertion might not hold

diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect
@@ -1,3 +1,14 @@
+ParallelResolveErrors.dfy(247,7): Warning: the ... refinement feature in statements is deprecated
+ParallelResolveErrors.dfy(248,10): Warning: the ... refinement feature in statements is deprecated
+ParallelResolveErrors.dfy(249,13): Warning: the ... refinement feature in statements is deprecated
+ParallelResolveErrors.dfy(256,9): Warning: the ... refinement feature in statements is deprecated
+ParallelResolveErrors.dfy(263,7): Warning: the ... refinement feature in statements is deprecated
+ParallelResolveErrors.dfy(264,10): Warning: the ... refinement feature in statements is deprecated
+ParallelResolveErrors.dfy(272,9): Warning: the ... refinement feature in statements is deprecated
+ParallelResolveErrors.dfy(279,7): Warning: the ... refinement feature in statements is deprecated
+ParallelResolveErrors.dfy(280,10): Warning: the ... refinement feature in statements is deprecated
+ParallelResolveErrors.dfy(281,13): Warning: the ... refinement feature in statements is deprecated
+ParallelResolveErrors.dfy(288,9): Warning: the ... refinement feature in statements is deprecated
 ParallelResolveErrors.dfy(26,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression
 ParallelResolveErrors.dfy(8,6): Error: a forall statement is not allowed to update a variable it doesn't declare
 ParallelResolveErrors.dfy(25,6): Error: a forall statement is not allowed to update a variable it doesn't declare

diff --git a/Test/dafny0/PrettyPrinting.dfy.expect b/Test/dafny0/PrettyPrinting.dfy.expect
@@ -1,3 +1,5 @@
+PrettyPrinting.dfy(18,10): Warning: the ... refinement feature in statements is deprecated
+PrettyPrinting.dfy(20,6): Warning: the ... refinement feature in statements is deprecated
 // PrettyPrinting.dfy
 
 

diff --git a/Test/dafny0/Refinement.dfy.expect b/Test/dafny0/Refinement.dfy.expect
@@ -1,3 +1,19 @@
+Refinement.dfy(156,13): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(161,9): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(162,13): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(167,13): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(198,13): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(203,9): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(204,13): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(209,13): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(252,11): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(255,7): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(259,7): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(260,10): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(262,9): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(264,7): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(269,7): Warning: the ... refinement feature in statements is deprecated
+Refinement.dfy(276,7): Warning: the ... refinement feature in statements is deprecated
 Refinement.dfy(233,4): Warning: note, this loop has no body (loop frame: i)
 Refinement.dfy(15,4): Error: A postcondition might not hold on this return path.
 Refinement.dfy(14,16): Related location: This is the postcondition that might not hold.

diff --git a/Test/dafny0/RefinementModificationChecking.dfy.expect b/Test/dafny0/RefinementModificationChecking.dfy.expect
@@ -1,3 +1,4 @@
+RefinementModificationChecking.dfy(20,9): Warning: the ... refinement feature in statements is deprecated
 RefinementModificationChecking.dfy(22,6): Error: refinement method cannot assign to variable defined in parent module ('t')
 RefinementModificationChecking.dfy(23,6): Error: refinement method cannot assign to variable defined in parent module ('r')
 RefinementModificationChecking.dfy(24,6): Error: refinement method cannot assign to a field defined in parent module ('f')

diff --git a/Test/dafny0/Simple.dfy.expect b/Test/dafny0/Simple.dfy.expect
@@ -1,3 +1,5 @@
+Simple.dfy(98,7): Warning: the ... refinement feature in statements is deprecated
+Simple.dfy(101,7): Warning: the ... refinement feature in statements is deprecated
 // Simple.dfy
 
 class MyClass<T, U> {

diff --git a/Test/dafny0/Skeletons.dfy.expect b/Test/dafny0/Skeletons.dfy.expect
@@ -1,3 +1,10 @@
+Skeletons.dfy(27,11): Warning: the ... refinement feature in statements is deprecated
+Skeletons.dfy(29,11): Warning: the ... refinement feature in statements is deprecated
+Skeletons.dfy(31,7): Warning: the ... refinement feature in statements is deprecated
+Skeletons.dfy(32,10): Warning: the ... refinement feature in statements is deprecated
+Skeletons.dfy(60,7): Warning: the ... refinement feature in statements is deprecated
+Skeletons.dfy(62,6): Warning: the ... refinement feature in statements is deprecated
+Skeletons.dfy(64,7): Warning: the ... refinement feature in statements is deprecated
 Skeletons.dfy(45,2): Error: A postcondition might not hold on this return path.
 Skeletons.dfy(44,14): Related location: This is the postcondition that might not hold.
 

diff --git a/Test/dafny0/Superposition.dfy.expect b/Test/dafny0/Superposition.dfy.expect
@@ -1,3 +1,4 @@
+Superposition.dfy(38,9): Warning: the ... refinement feature in statements is deprecated
 
 Verifying M0.C.M (correctness) ...
   [4 proof obligations]  verified

diff --git a/Test/dafny0/Termination.dfy.expect b/Test/dafny0/Termination.dfy.expect
@@ -1,3 +1,4 @@
+Termination.dfy(450,7): Warning: the ... refinement feature in statements is deprecated
 Termination.dfy[TerminationRefinement1](441,5): Error: decreases clause might not decrease
 Termination.dfy(361,46): Error: decreases clause might not decrease
 Termination.dfy(577,5): Error: cannot find witness that shows type is inhabited; try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type

diff --git a/Test/dafny1/SchorrWaite-stages.dfy.expect b/Test/dafny1/SchorrWaite-stages.dfy.expect
@@ -1,2 +1,23 @@
+SchorrWaite-stages.dfy(149,7): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(150,10): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(161,9): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(162,16): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(164,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(168,15): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(174,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(175,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(201,7): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(202,10): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(221,9): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(223,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(225,16): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(230,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(236,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(239,11): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(255,7): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(256,10): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(260,9): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(261,16): Warning: the ... refinement feature in statements is deprecated
+SchorrWaite-stages.dfy(263,11): Warning: the ... refinement feature in statements is deprecated
 
 Dafny program verifier finished with 7 verified, 0 errors
diff --git a/Test/dafny2/MonotonicHeapstate.dfy.expect b/Test/dafny2/MonotonicHeapstate.dfy.expect
@@ -1,2 +1,7 @@
+MonotonicHeapstate.dfy(92,13): Warning: the ... refinement feature in statements is deprecated
+MonotonicHeapstate.dfy(99,13): Warning: the ... refinement feature in statements is deprecated
+MonotonicHeapstate.dfy(106,13): Warning: the ... refinement feature in statements is deprecated
+MonotonicHeapstate.dfy(146,9): Warning: the ... refinement feature in statements is deprecated
+MonotonicHeapstate.dfy(147,13): Warning: the ... refinement feature in statements is deprecated
 
 Dafny program verifier finished with 24 verified, 0 errors