You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
feat: continue statements. Like Dafny's break statements, these come in two forms: one that uses a label to name the continue target and one that specifies the continue target by nesting level. See section 19.2 of the Reference Manual. (feat: continue statements #1839)
feat: The keyword syntax for functions will change in Dafny version 4. The new command-line option /functionSyntax (see /help) allows early adoption of the new syntax. (Function keywords refresh #1832)
feat: Attribute {:print} declares that a method may have print effects. Print effects are enforced only with /trackPrintEffects:1.
fix: The error "assertion violation" is replaced by the better wording "assertion might not hold". This indicates better that the verifier is unable to prove the assertion. (fix: assertion may not hold #1862)
This discussion was created from the release Dafny 3.5.0.
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
-
continue
statements. Like Dafny'sbreak
statements, these come in two forms: one that uses a label to name the continue target and one that specifies the continue target by nesting level. See section 19.2 of the Reference Manual. (feat: continue statements #1839)/functionSyntax
(see/help
) allows early adoption of the new syntax. (Function keywords refresh #1832){:print}
declares that a method may have print effects. Print effects are enforced only with/trackPrintEffects:1
./proverOpt:BATCH_MODE=true
). Inherited from Boogie 2.13 (Refactor solver process handling to allow non-interactive mode boogie-org/boogie#512)./verificationLogger
and/vcsCores
to be usable together. Inherited from Boogie 2.13 (Support XML generation with /vcsCores boogie-org/boogie#515).RevealableTypeDeclHelper
#1858, IncorrectprogramId
passed to Boogie causes memory leak in LSP server #1863)This discussion was created from the release Dafny 3.5.0.
Beta Was this translation helpful? Give feedback.
All reactions