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
As discussed as a team, the following should report only 3 errors instead of 6:
method {:only} TestReported() {
assertfalse; // An error here
}
methodTestNotReported() {
assertfalse; // No error here
}
classA {
method {:only} TestReported() {
assertfalse; // An error here
}
methodTestNotReported() {
assertfalse; // No error here
}
}
module B {
method {:only} TestReported() {
assertfalse; // An error here
}
methodTestNotReported() {
assertfalse; // No error here
}
}
That feature will make the use of {:only} on part with selective verification where users can verify only one method at a time, except that it would work for any IDE and also on the command line, without having to specify a specific attribute.
The text was updated successfully, but these errors were encountered:
This PR implements a feature that fixes#4074
I added the corresponding tests, auditor entries and documentations with
appropriate links.
<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
---------
Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
As discussed as a team, the following should report only 3 errors instead of 6:
That feature will make the use of
{:only}
on part with selective verification where users can verify only one method at a time, except that it would work for any IDE and also on the command line, without having to specify a specific attribute.The text was updated successfully, but these errors were encountered: