Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Isolate assertions attribute #5247

Merged
merged 10 commits into from
Mar 27, 2024
Merged

Isolate assertions attribute #5247

Changes from 1 commit
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
95c3d05
Isolate assertions attribute
keyboardDrummer Mar 25, 2024
c961aae
Update documentation and dfy files so they use the new attribute
keyboardDrummer Mar 25, 2024
12c60e2
Add release note
keyboardDrummer Mar 25, 2024
d2ee83b
Update doo files
keyboardDrummer Mar 25, 2024
0b13722
Ran format on stdlib
keyboardDrummer Mar 26, 2024
6cc9591
Update docs/dev/news/5247.feat
keyboardDrummer Mar 27, 2024
b11e20d
Update docs/DafnyRef/Attributes.md
keyboardDrummer Mar 27, 2024
41e12f0
Update doo files
keyboardDrummer Mar 27, 2024
d6c61a7
Merge branch 'isolateAssertionsAttribute' of github.com:keyboardDrumm…
keyboardDrummer Mar 27, 2024
735ca52
Merge branch 'master' into isolateAssertionsAttribute
keyboardDrummer Mar 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Update docs/DafnyRef/Attributes.md 
Co-authored-by: Mikaël Mayer <[email protected]>
  • Loading branch information
@keyboardDrummer @MikaelMayer
keyboardDrummer and MikaelMayer committed Mar 27, 2024
commit b11e20d9e0e069863dc96c3d328c84124aef8fe2
2 changes: 1 addition & 1 deletion docs/DafnyRef/Attributes.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -630,7 +630,7 @@ Defaults to 1.
If [`{:isolate_assertions}`](#sec-isolate_assertions) is set, then this parameter is useless.

### 11.2.25. `{:isolate_assertions}` {#sec-isolate_assertions}
Per-method version of the command-line option `/vcsSplitOnEveryAssert`.
Per-method version of the command-line option<span id="sec-vcs_split_on_every_assert"></span> `/vcsSplitOnEveryAssert`

In the first and only verification round, this option will split the original [assertion batch](#sec-assertion-batches)
into one assertion batch per assertion.
Expand Down
Loading