Dafny 4.6.0

[robin-aws]

New features

• Add a check to dafny run that notifies the user when a value that was parsed as a user program argument, and which occurs before a -- token, starts with --, since this indicates they probably mistyped a Dafny option name. (dafny run file.dfy --include file.cs does not raise errors #5097)

• Add an option --progress that can be used to track the progress of verification. (Add incremental verification progress reporting in a Dafny-centric way #5150)

• Add the attribute {:isolate_assertions}, which does the same as {:vcs_split_on_every_assert}. Deprecated {:vcs_split_on_every_assert} (Isolate assertions attribute #5247)

Bug fixes

• (soundness issue) Twostate predicate now check if their not new arguments are allocated in the previous heap (Allocation soundness issue #4844)

• Add uniform checking of type characteristics in refinement modules (fix: Add uniform checking of type characteristics in refinement modules #5146)

• Fixed links associated with the standard libraries. (Standard Library documentation is broken #5176)

• fix: Disable the "erase datatype wrappers" optimization if the datatype implements any traits.
  feat: Allow the "erase datatype wrappers" optimization if the only fields in the datatype are ghost fields.
  (fix: Optimize datatype wrappers only in the absence of trait parents #5234)

• Fix the default string value emitted for JavaScript (fix: Generate proper default string value for JavaScript #5239)

---

This discussion was created from the release Dafny 4.6.0.