From 87f0eee292ba37053aabb71cc32cbccee622bb92 Mon Sep 17 00:00:00 2001 From: davidcok Date: Thu, 14 Jul 2022 08:11:36 -0400 Subject: [PATCH 1/5] Edit per comment from Remy --- docs/DafnyRef/Introduction.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/DafnyRef/Introduction.md b/docs/DafnyRef/Introduction.md index 823f29ad02f..4ec609364cd 100644 --- a/docs/DafnyRef/Introduction.md +++ b/docs/DafnyRef/Introduction.md @@ -29,8 +29,8 @@ changing the program’s type declarations, specifications, and statements. and `dafny` to refer to the software tool that verifies and compiles programs in the Dafny language.) -The easiest way to try out `dafny` is to [download](https://github.com/dafny-lang/dafny/releases) it -to run it on your machine as you follow along with the [Dafny tutorial](../OnlineTutorial/guide). +The easiest way to try out the Dafny language is to [download the supporting tools and documentation](https://github.com/dafny-lang/dafny/releases) and +run `dafny` on your machine as you follow along with the [Dafny tutorial](../OnlineTutorial/guide). The `dafny` tool can be run from the command line (on Linux, MacOS, Windows or other platforms) or from an IDE such as emacs or an editor such as VSCode, which can provide syntax highlighting without the built-in verification. From a119ed34f9a48ca4658a1a572cb8a664ce789a89 Mon Sep 17 00:00:00 2001 From: davidcok Date: Sun, 18 Sep 2022 21:49:24 -0400 Subject: [PATCH 2/5] Updates to RM for Issue #2425 --- docs/DafnyRef/Refinement.md | 4 +++ docs/DafnyRef/Statements.md | 59 +++++++++++-------------------------- 2 files changed, 21 insertions(+), 42 deletions(-) diff --git a/docs/DafnyRef/Refinement.md b/docs/DafnyRef/Refinement.md index 011ed712144..c6b487ab4b4 100644 --- a/docs/DafnyRef/Refinement.md +++ b/docs/DafnyRef/Refinement.md @@ -304,3 +304,7 @@ TODO TODO +## 22.11. Statements + +The refinment syntax (`...`) in statements is deprecated. + diff --git a/docs/DafnyRef/Statements.md b/docs/DafnyRef/Statements.md index 479a964322c..5273594893a 100644 --- a/docs/DafnyRef/Statements.md +++ b/docs/DafnyRef/Statements.md @@ -5,13 +5,13 @@ NonLabeledStmt = ( AssertStmt | AssumeStmt | BlockStmt | BreakStmt | CalcStmt | ExpectStmt | ForallStmt | IfStmt | MatchStmt | ModifyStmt - | PrintStmt | ReturnStmt | RevealStmt | SkeletonStmt + | PrintStmt | ReturnStmt | RevealStmt | UpdateStmt | UpdateFailureStmt | VarDeclStatement | WhileStmt | ForLoopStmt | YieldStmt ) ```` Many of Dafny's statements are similar to those in traditional @@ -880,7 +880,6 @@ IfStmt = "if" | ( BindingGuard(allowLambda: true) | Guard - | ellipsis ) BlockStmt [ "else" ( IfStmt | BlockStmt ) ] ) @@ -941,7 +940,7 @@ to the right of `=>` for that guard are executed. The statement requires at least one of the guards to evaluate to `true` (that is, `if-case` statements must be exhaustive: the guards must cover all cases). -TODO: Describe the ... refinement +The form that used `...` (a refinement feature) as the guard is deprecated. ## 20.12. While Statement {#sec-while-statement} ````grammar @@ -949,10 +948,9 @@ WhileStmt = "while" ( LoopSpec AlternativeBlock(allowBindingGuards: false) - | ( Guard | ellipsis ) + | Guard LoopSpec ( BlockStmt - | ellipsis | /* go body-less */ ) ) @@ -987,14 +985,12 @@ iteration of the loop. If false then terminate the loop. Keep the following commented out until we decide a better place to put it. -* An ellipsis (`...`), which makes the while statement a _skeleton_ -`while` statement. TODO: What does that mean? - The _body_ of the loop is usually a block statement, but it can also -be a _skeleton_, denoted by ellipsis, or missing altogether. +be missing altogether. TODO: Wouldn't a missing body cause problems? Isn't it clearer to have a block statement with no statements inside? --> +The form that used `...` (a refinement feature) as the guard is deprecated. The second form uses the `AlternativeBlock`. It is similar to the `do ... od` construct used in the book "A Discipline of Programming" by @@ -1016,8 +1012,6 @@ are executed and the while statement is repeated. If none of the guards evaluates to true, then the loop execution is terminated. -TODO: Describe ... refinement - ## 20.13. For Loops {#sec-for-loops} ````grammar ForLoopStmt = @@ -1514,13 +1508,11 @@ infinite. AssertStmt = "assert" { Attribute } - ( [ LabelName ":" ] - Expression(allowLemma: false, allowLambda: true) - ( ";" - | "by" BlockStmt - ) - | ellipsis - ";" + [ LabelName ":" ] + Expression(allowLemma: false, allowLambda: true) + ( ";" + | "by" BlockStmt + ) ```` `Assert` statements are used to express logical proposition that are @@ -1535,7 +1527,7 @@ much as lemmas might be used in mathematical proofs. `Assert` statements are ignored by the compiler. -Using `...` as the argument of the statement is part of module refinement, as described in [Section 22](#sec-module-refinement). +Using `...` as the argument of the statement is deprecated. In the `by` form of the `assert` statement, there is an additional block of statements that provide the Dafny verifier with additional proof steps. Those statements are often a sequence of [lemmas](#sec-lemmas), [`calc`](#sec-calc-statement) statements, [`reveal`](#sec-reveal-statements) statements or other `assert` statements, @@ -1555,7 +1547,6 @@ AssumeStmt = "assume" { Attribute } ( Expression(allowLemma: false, allowLambda: true) - | ellipsis ) ";" ```` @@ -1574,7 +1565,7 @@ An `assume` statement cannot be compiled. In fact, the compiler will complain if it finds an `assume` anywhere where it has not been replaced through a refinement step. -Using `...` as the argument of the statement is part of module refinement, as described in [Section 22](#sec-module-refinement). +Using `...` as the argument of the statement is deprecated. ## 20.18. Expect Statement {#sec-expect-statement} @@ -1583,7 +1574,6 @@ ExpectStmt = "expect" { Attribute } ( Expression(allowLemma: false, allowLambda: true) - | ellipsis ) [ "," Expression(allowLemma: false, allowLambda: true) ] ";" @@ -1685,13 +1675,7 @@ then the verifier will interpret the `expect` like an `assume`, in which case the `assert` will be proved trivially and potential unsoundness will be hidden. -Using `...` as the argument of the `expect` statement is part of module refinement, as described in [Section 22](#sec-module-refinement). - - +Using `...` as the argument of the statement is deprecated. ## 20.19. Print Statement {#sec-print-statement} ````grammar @@ -1950,10 +1934,8 @@ co-predicates and co-lemmas. See [datatypes](#sec-co-inductive-datatypes). ModifyStmt = "modify" { Attribute } - ( FrameExpression(allowLemma: false, allowLambda: true) - { "," FrameExpression(allowLemma: false, allowLambda: true) } - | ellipsis - ) + FrameExpression(allowLemma: false, allowLambda: true) + { "," FrameExpression(allowLemma: false, allowLambda: true) } ( BlockStmt | ";" ) @@ -2049,7 +2031,7 @@ Finally, the fourth example shows that the restrictions imposed by the modify statement do not apply to local variables, only those that are heap-based. -Using `...` as the argument of the statement is part of module refinement, as described in [Section 22](#sec-module-refinement). +Using `...` as the argument of the statement is deprecated. ## 20.23. Calc Statement {#sec-calc-statement} ````grammar @@ -2177,10 +2159,3 @@ step. As shown in the example, comments can also be used to aid the human reader in cases where Dafny can prove the step automatically. -## 20.24. Skeleton Statement {#sec-skeleton-statement} -````grammar -SkeletonStmt = - ellipsis - ";" -```` -TODO: Move to discussion of refinement? From 19a5162ab0d11f02355b4b44a9d82c6b4f1bf1e4 Mon Sep 17 00:00:00 2001 From: davidcok Date: Sun, 18 Sep 2022 21:50:11 -0400 Subject: [PATCH 3/5] Deprecating statement refinement per #2425 --- Makefile | 1 + Source/DafnyCore/Dafny.atg | 32 ++++++--- Test/allocated1/dafny0/Refinement.dfy.expect | 16 +++++ Test/allocated1/dafny0/Simple.dfy.expect | 2 + Test/allocated1/dafny0/Skeletons.dfy.expect | 7 ++ .../dafny0/Superposition.dfy.expect | 1 + Test/allocated1/dafny0/Termination.dfy.expect | 1 + .../dafny1/SchorrWaite-stages.dfy.expect | 21 ++++++ Test/dafny0/DividedConstructors.dfy.expect | 1 + Test/dafny0/Include.dfy.expect | 1 + Test/dafny0/ParallelResolveErrors.dfy.expect | 11 ++++ Test/dafny0/PrettyPrinting.dfy.expect | 2 + Test/dafny0/Refinement.dfy.expect | 16 +++++ .../RefinementModificationChecking.dfy.expect | 1 + Test/dafny0/Simple.dfy.expect | 2 + Test/dafny0/Skeletons.dfy.expect | 7 ++ Test/dafny0/Superposition.dfy.expect | 1 + Test/dafny0/Termination.dfy.expect | 1 + Test/dafny1/SchorrWaite-stages.dfy.expect | 21 ++++++ Test/dafny1/SchorrWaite.dfy.expect | 21 ++++++ Test/dafny2/MonotonicHeapstate.dfy.expect | 5 ++ Test/dafny2/StoreAndRetrieve.dfy.expect | 25 +++++++ Test/dafny3/CachedContainer.dfy.expect | 65 +++++++++++++++++++ Test/dafny4/ClassRefinement.dfy.expect | 25 +++++++ 24 files changed, 278 insertions(+), 8 deletions(-) diff --git a/Makefile b/Makefile index 2ca3ea3a132..f7ceca6d51d 100644 --- 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 index f45c7adc00f..9700390667e 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -2769,7 +2769,9 @@ SkeletonStmt = (. 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"); + .) . /*------------------------------------------------------------------------*/ @@ -3080,7 +3082,9 @@ IfStmt ( IF(IsBindingGuard()) BindingGuard (. isBindingGuard = true; .) | Guard - | ellipsis (. guardEllipsis = t; .) + | ellipsis (. guardEllipsis = t; + errors.Deprecated(t, "the ... refinement feature in statements is deprecated"); + .) ) BlockStmt (. endTok = thn.EndTok; .) [ "else" @@ -3177,13 +3181,17 @@ WhileStmt (. stmt = new AlternativeLoopStmt(x, endTok, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), alternatives, usesOptionalBraces, attrs); .) | ( 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 ( 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 (. 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 */ ) (. @@ -3424,7 +3432,9 @@ AssertStmt BlockStmt | ";" ) - | ellipsis (. dotdotdot = t; .) + | ellipsis (. dotdotdot = t; + errors.Deprecated(t, "the ... refinement feature in statements is deprecated"); + .) ";" ) (. if (dotdotdot != null) { @@ -3444,7 +3454,9 @@ ExpectStmt "expect" (. x = t; .) { Attribute } ( Expression - | ellipsis (. dotdotdot = t; .) + | ellipsis (. dotdotdot = t; + errors.Deprecated(t, "the ... refinement feature in statements is deprecated"); + .) ) [ "," Expression ] ";" @@ -3465,7 +3477,9 @@ AssumeStmt "assume" (. x = t; .) { Attribute } ( Expression - | ellipsis (. dotdotdot = t; .) + | ellipsis (. dotdotdot = t; + errors.Deprecated(t, "the ... refinement feature in statements is deprecated"); + .) ) ";" (. if (dotdotdot != null) { @@ -3559,7 +3573,9 @@ ModifyStmt ( FrameExpression (. mod.Add(fe); .) { "," FrameExpression (. mod.Add(fe); .) } - | ellipsis (. ellipsisToken = t; .) + | ellipsis (. ellipsisToken = t; + errors.Deprecated(t, "the ... refinement feature in statements is deprecated"); + .) ) ( BlockStmt | SYNC ";" (. endTok = t; .) diff --git a/Test/allocated1/dafny0/Refinement.dfy.expect b/Test/allocated1/dafny0/Refinement.dfy.expect index da8dcda50bc..cf608fa5b67 100644 --- 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 index a37b202e128..596321780f0 100644 --- 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 index 782b0bce284..5f99dc2f397 100644 --- 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 index b7192d30e07..92a80d2806f 100644 --- 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 index 891ed8f90f3..5b0731df039 100644 --- 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 index 851aaf58286..160e780feb5 100644 --- 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 index c38b1f1648b..f7412d8d0a1 100644 --- 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 index 60c77b95189..bdf2bd5392c 100644 --- 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 index b1bbffa044e..22012d5633e 100644 --- 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 index bd35f682b50..3064b92bad2 100644 --- 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 index da8dcda50bc..cf608fa5b67 100644 --- 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 index d2457fbcb04..776540f85fb 100644 --- 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 index 1e90daa15d3..3cebbe1974f 100644 --- 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 { diff --git a/Test/dafny0/Skeletons.dfy.expect b/Test/dafny0/Skeletons.dfy.expect index 782b0bce284..5f99dc2f397 100644 --- 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 index b7192d30e07..92a80d2806f 100644 --- 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 index 63ba4e88c4b..0d90cbb8556 100644 --- 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 index 851aaf58286..4ea2437c20d 100644 --- 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/dafny1/SchorrWaite.dfy.expect b/Test/dafny1/SchorrWaite.dfy.expect index 1981561ca00..98396855cd6 100644 --- a/Test/dafny1/SchorrWaite.dfy.expect +++ b/Test/dafny1/SchorrWaite.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 10 verified, 0 errors diff --git a/Test/dafny2/MonotonicHeapstate.dfy.expect b/Test/dafny2/MonotonicHeapstate.dfy.expect index 25822a5c6cc..f015f6885ea 100644 --- 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 diff --git a/Test/dafny2/StoreAndRetrieve.dfy.expect b/Test/dafny2/StoreAndRetrieve.dfy.expect index 8f23b14d4b7..1033db08d45 100644 --- a/Test/dafny2/StoreAndRetrieve.dfy.expect +++ b/Test/dafny2/StoreAndRetrieve.dfy.expect @@ -1,14 +1,39 @@ +StoreAndRetrieve.dfy(65,13): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(70,9): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(71,13): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(86,9): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(97,9): Warning: the ... refinement feature in statements is deprecated Dafny program verifier finished with 23 verified, 0 errors +StoreAndRetrieve.dfy(65,13): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(70,9): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(71,13): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(86,9): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(97,9): Warning: the ... refinement feature in statements is deprecated Dafny program verifier did not attempt verification 20.3 +StoreAndRetrieve.dfy(65,13): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(70,9): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(71,13): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(86,9): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(97,9): Warning: the ... refinement feature in statements is deprecated Dafny program verifier did not attempt verification 20.3 +StoreAndRetrieve.dfy(65,13): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(70,9): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(71,13): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(86,9): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(97,9): Warning: the ... refinement feature in statements is deprecated Dafny program verifier did not attempt verification 20.3 +StoreAndRetrieve.dfy(65,13): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(70,9): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(71,13): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(86,9): Warning: the ... refinement feature in statements is deprecated +StoreAndRetrieve.dfy(97,9): Warning: the ... refinement feature in statements is deprecated Dafny program verifier did not attempt verification 20.3 diff --git a/Test/dafny3/CachedContainer.dfy.expect b/Test/dafny3/CachedContainer.dfy.expect index 6e82de46859..ace008ac315 100644 --- a/Test/dafny3/CachedContainer.dfy.expect +++ b/Test/dafny3/CachedContainer.dfy.expect @@ -1,14 +1,79 @@ +CachedContainer.dfy(117,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(124,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(127,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(134,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(137,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(158,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(159,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(167,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(168,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(171,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(172,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(183,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(184,13): Warning: the ... refinement feature in statements is deprecated Dafny program verifier finished with 34 verified, 0 errors +CachedContainer.dfy(117,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(124,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(127,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(134,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(137,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(158,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(159,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(167,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(168,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(171,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(172,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(183,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(184,13): Warning: the ... refinement feature in statements is deprecated Dafny program verifier did not attempt verification false true false true +CachedContainer.dfy(117,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(124,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(127,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(134,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(137,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(158,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(159,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(167,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(168,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(171,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(172,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(183,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(184,13): Warning: the ... refinement feature in statements is deprecated Dafny program verifier did not attempt verification false true false true +CachedContainer.dfy(117,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(124,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(127,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(134,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(137,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(158,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(159,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(167,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(168,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(171,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(172,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(183,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(184,13): Warning: the ... refinement feature in statements is deprecated Dafny program verifier did not attempt verification false true false true +CachedContainer.dfy(117,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(124,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(127,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(134,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(137,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(158,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(159,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(167,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(168,13): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(171,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(172,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(183,9): Warning: the ... refinement feature in statements is deprecated +CachedContainer.dfy(184,13): Warning: the ... refinement feature in statements is deprecated Dafny program verifier did not attempt verification false true false true diff --git a/Test/dafny4/ClassRefinement.dfy.expect b/Test/dafny4/ClassRefinement.dfy.expect index d698ab0e8aa..bedccba95f0 100644 --- a/Test/dafny4/ClassRefinement.dfy.expect +++ b/Test/dafny4/ClassRefinement.dfy.expect @@ -1,14 +1,39 @@ +ClassRefinement.dfy(73,9): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(74,13): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(79,9): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(80,13): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(83,13): Warning: the ... refinement feature in statements is deprecated Dafny program verifier finished with 11 verified, 0 errors +ClassRefinement.dfy(73,9): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(74,13): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(79,9): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(80,13): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(83,13): Warning: the ... refinement feature in statements is deprecated Dafny program verifier did not attempt verification 2 1 +ClassRefinement.dfy(73,9): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(74,13): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(79,9): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(80,13): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(83,13): Warning: the ... refinement feature in statements is deprecated Dafny program verifier did not attempt verification 2 1 +ClassRefinement.dfy(73,9): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(74,13): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(79,9): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(80,13): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(83,13): Warning: the ... refinement feature in statements is deprecated Dafny program verifier did not attempt verification 2 1 +ClassRefinement.dfy(73,9): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(74,13): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(79,9): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(80,13): Warning: the ... refinement feature in statements is deprecated +ClassRefinement.dfy(83,13): Warning: the ... refinement feature in statements is deprecated Dafny program verifier did not attempt verification 2 1 From 59822ad60fd49097a424eac483c89853870270c5 Mon Sep 17 00:00:00 2001 From: davidcok Date: Sun, 18 Sep 2022 22:28:27 -0400 Subject: [PATCH 4/5] Fixing a test --- Test/dafny1/SchorrWaite.dfy.expect | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/Test/dafny1/SchorrWaite.dfy.expect b/Test/dafny1/SchorrWaite.dfy.expect index 98396855cd6..1981561ca00 100644 --- a/Test/dafny1/SchorrWaite.dfy.expect +++ b/Test/dafny1/SchorrWaite.dfy.expect @@ -1,23 +1,2 @@ -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 10 verified, 0 errors From 47815c1a3e7c0a66140d3b7960aac120b007abe8 Mon Sep 17 00:00:00 2001 From: davidcok Date: Wed, 21 Sep 2022 09:11:09 -0400 Subject: [PATCH 5/5] Checking included files --- docs/_includes/custom-head.html | 2 ++ docs/_includes/footer.html | 1 + docs/_includes/head.html | 1 + docs/_includes/header.html | 1 + docs/_layouts/default.html | 1 + 5 files changed, 6 insertions(+) diff --git a/docs/_includes/custom-head.html b/docs/_includes/custom-head.html index 8559a67ffad..d5113b87220 100644 --- a/docs/_includes/custom-head.html +++ b/docs/_includes/custom-head.html @@ -4,3 +4,5 @@ 1. Head over to https://realfavicongenerator.net/ to add your own favicons. 2. Customize default _includes/custom-head.html in your source directory and insert the given code snippet. {% endcomment %} + +CUSTOM diff --git a/docs/_includes/footer.html b/docs/_includes/footer.html index 03e4d2d11d9..a280d5a1fd2 100644 --- a/docs/_includes/footer.html +++ b/docs/_includes/footer.html @@ -1,4 +1,5 @@