Cover failed assertions #5636
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -76,13 +76,15 @@ by other mechanism may categorise their properties differently. | |
|
|
||
| ### Coverage mode | ||
|
|
||
| There is one further BMC mode that differs more fundamentally: when `--cover` | ||
| is passed, assertions in the program text are converted into assumptions (these | ||
| must hold for control flow to proceed past them, but are not goals for the | ||
| equation solver; In cases where this behaviour is undesirable you can pass the | ||
| `--cover-failed-assertions` which makes coverage checking continue even for | ||
|
There was a problem hiding this comment. BTW shouldn’t this file be under There was a problem hiding this comment. The READMEs which are in each module are pulled into here: http://cprover.diffblue.com/folder-walkthrough.html (click on |
||
| paths where assertions fail), while new `assert(false)` statements are added | ||
| throughout the source program representing coverage goals. The equation solving | ||
| process then proceeds the same as in all-properties mode. Coverage solving is | ||
| implemented by `bmc_covert`, but is structurally practically identical to | ||
| `bmc_all_propertiest`-- only the reporting differs (goals are called "covered" | ||
| rather than "failed"). | ||
|
|
||
|
|
||
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't want to open a massive can of worms here but ... why is this the default? Is this actually useful? Given that there are options for
--no-assertions,--no-assumptionsand--assert-to-assume(whether they work or even do anything at all ... is an open question) could we make the transformation of assertions and assumptions orthogonal to--cover. It feels like this should be possible and even desirable...There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@martin-cs I think this is the default because whoever wrote this had the expectation that programs should stop at failed assertions. I suppose we could change it, but I’m always a bit wary about changing defaults.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@martin-cs FWIW because cover treats each failed goal as something relating to coverage right now we have to do something with asserts. That said, I think the alternative (just making cover cleverer about how it counts coverage) would be more desirable.
I'd consider that as something we can take a look at in terms of future work though.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, if you are doing a naive count then, I see the need to do something with pre-existing assertions or otherwise true assertions (generally a good thing) will count against your coverage. Smarter counting would certainly be one way to address this.
It feels to me that making the "doing something about asserts" independent might be a desirable option as well. I can see use-cases for converting to SKIP, to ASSUME and leaving as they are.
Then again, I am not a user of this code at the moment and do not have time to work on it so my views maybe not so important.