Unwinding options --unwinding-assertions and --partial-loops do not conflict #6644
Conversation
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
tautschnig
requested review from
chris-ryder,
kroening,
martin-cs,
peterschrammel and
romainbrenguier
as code owners
chris-ryder
approved these changes
Feb 6, 2022
tautschnig
force-pushed
the
feature/partial-loops
branch
from
c2c51d8 to
7cd36a7
Compare
Codecov Report
@@ Coverage Diff @@
## develop #6644 +/- ##
===========================================
+ Coverage 77.04% 77.76% +0.71%
===========================================
Files 1594 1568 -26
Lines 185276 179628 -5648
===========================================
- Hits 142748 139684 -3064
+ Misses 42528 39944 -2584
Continue to review full report at Codecov.
|
doc/cprover-manual/cbmc-unwinding.md
Outdated
| @@ -161,7 +161,9 @@ to the later assertion, use the option | |||
| This option will allow paths that execute loops only partially, enabling | |||
| a counterexample for the assertion above even for small unwinding | |||
| bounds. The disadvantage of using this option is that the resulting path | |||
| may be spurious, that is, it may not exist in the original program. | |||
| may be spurious, that is, it may not exist in the original program. If | |||
| `--unwinding-assertions` is also used and all unwinding assertions pass, | |||
There was a problem hiding this comment.
If
--unwinding-assertionsis also used [together with --partial-loops] and all unwinding assertions pass
I can't quite see the example where this would happen. Does the following statement hold? Whenever a failing assertion becomes reachable due to the use of --partial-loops, there must be a failing unwinding assertion. ❓
There was a problem hiding this comment.
Fair point. I have now reworded the text as follows:
If `--unwinding-assertions` is also used, and the particular counterexample
trace does not include a report of a violated unwinding assertion, then that
counterexample is not impacted by insufficient loop unwinding.
…onflict By default, bounded loop unwinding will yield an assumption to ensure that all counterexamples are genuine. Option --unwinding-assertions requests that an additional assertion be generated, which will furthermore ensure that successful verification does not constitute spurious proof. Option --partial-loops disables generating the unwinding assumption. Therefore, --unwinding-assertions and --partial-loops each control (not) generating one instruction, but there is no overlap in the instructions that they are (not) generating. It is, thus, safe to use these options together.
tautschnig
force-pushed
the
feature/partial-loops
branch
from
7cd36a7 to
836f04b
Compare
peterschrammel
approved these changes
May 10, 2022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
By default, bounded loop unwinding will yield an assumption to ensure
that all counterexamples are genuine.
Option --unwinding-assertions requests that an additional assertion be
generated, which will furthermore ensure that successful verification
does not constitute spurious proof.
Option --partial-loops disables generating the unwinding assumption.
Therefore, --unwinding-assertions and --partial-loops each control (not)
generating one instruction, but there is no overlap in the instructions
that they are (not) generating. It is, thus, safe to use these options
together.