SV-COMP 22 fixes #27
Merged
SV-COMP 22 fixes #27
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
viktormalik
approved these changes
Oct 11, 2021
peterschrammel
approved these changes
Oct 11, 2021
Author
|
One more bug uncovered, memcleanup instrumentation was not done, the |
You should probably rename the PR. |
viktormalik
approved these changes
Oct 15, 2021
FrNecas
changed the title
Author
|
One more fix added related to nontermination witnesses. |
This reverts commit 40046b2. A commit achieving the same thing is already present in CBMC causing duplication of the attribute.
If inlining is performed, the function_identifier parameter will always be __CPROVER_start. However, the former function is still stored in the goto instruction and can be sued for the instrumentation Signed-off-by: František Nečas <[email protected]>
This was previously commented out but was dropped in the rebase by accident (the code was moved and merge conflict not correctly resolved). This is necessary for some nontermination witnesses to function correctly. Signed-off-by: František Nečas <[email protected]>
FrNecas
force-pushed
the
frnecas-svcomp-fixes
branch
from
cef5c19 to
36c8f77
Compare
Author
|
Rebased to the current state of target branch. Lets see the results of one more pre-run and we can probably merge this if everything goes well :) |
|
@peterschrammel this should be ready, could you merge it, please? Thanks! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
@peterschrammel this is a fix for SVcomp, the same change that we had in our fork was applied in the develop branch ( see diffblue#5660 ) so it is no longer necessary. Reverting for now, we can drop these commits if we later rebase to a newer version.