Adjustments to validator #7
Open
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
4 tasks
hannes-steffenhagen-diffblue
force-pushed
the
ci/xsd-validation
branch
2 times, most recently
from
5f02606 to
18ca4aa
Compare
…the developer manual
hannes-steffenhagen-diffblue
force-pushed
the
ci/xsd-validation
branch
from
18ca4aa to
ffd35ff
Compare
The incremental status should report failure from the first unwinding for which one property is falsified.
It is not possible to conclude successful verification before the unwinding has finished, so this prints inconclusive until the analysis is complete. However, if one property has been falsified, then even though the analysis can continue to check other properties, the verification will certainly fail.
We want to print the status after we've done any solving for that unwind, but before we've done an extra step of symexing. We should not print in the event the full equation has been generated, as then we have a full solution so ins't incremental. Ditto we don't need to print the status if we've found a failure, as this function will be called again to do the next symex invocation if there are further propreties to check
We now print after all solving, and the last thing before the next increment, therefore the printing checks are easier to check immediately precedes the next unwinding, rather than checking appears after the increment we are talking about.
In this case, the status is inconclusive until completion, at which point success will be reported by CBMC overall.
hannes-steffenhagen-diffblue
force-pushed
the
ci/xsd-validation
branch
from
ffd35ff to
cd578d9
Compare
…-manual Fix dead links in cbmc user manual
…emental-solving Incremental solving producing cprover status as it goes
Add documentation for memory primitives
…/xsd-validation Add validation tests for trace XSD
thk123
force-pushed
the
adjustments-to-validator
branch
from
774cd38 to
5b3640a
Compare
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.
Addressing review comments.
I expect this to fail - CIs without dependencies now need to explicitly not run this test suite
@hannes-steffenhagen-diffblue If this passes, feel free to incorporate into your PR, squashing as you see fit.