Run CBMC regression tests with --paths lifo in CI #3976
Merged
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
chrisr-diffblue,
forejtv,
kroening,
peterschrammel,
smowton and
thk123
as code owners
|
+1 testing more options in CI / regressions A Good Thing. |
tautschnig
added a commit
that referenced
this pull request
Jan 30, 2019
Restore namespace after symbolic execution [blocks: #3976]
tautschnig
added a commit
that referenced
this pull request
Jan 31, 2019
Maintain nondet and dynamic counters across symex instances [blocks: #3976]
tautschnig
changed the title
3 tasks
peterschrammel
force-pushed
the
paths-regression-test
branch
from
c6c187b to
8e72f89
Compare
tautschnig
requested review from
cesaro,
cristina-david,
NathanJPhillips and
pkesseli
as code owners
peterschrammel
added a commit
that referenced
this pull request
Feb 4, 2019
Single-path symex checker [blocks: #3976]
tautschnig
force-pushed
the
paths-regression-test
branch
2 times, most recently
from
c6c187b to
37bec93
Compare
tautschnig
changed the title
tautschnig
force-pushed
the
paths-regression-test
branch
from
37bec93 to
11db7b0
Compare
allredj
reviewed
Feb 5, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 11db7b0).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99712165
allredj
reviewed
Feb 5, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 3310e02).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99716161
We were not regularly exercising this code outside unit tests, leading to regressions on several tests. On my system, running this additional test takes 42 seconds, which is still better than users running into issues. (ctest -V -L CORE -j8 takes an extra 10 seconds.) Fixes: diffblue#3956
On Codebuild we have seen "1.5222e-05s" when running in path-based mode.
tautschnig
force-pushed
the
paths-regression-test
branch
from
3310e02 to
0bda456
Compare
allredj
reviewed
Feb 5, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 0bda456).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99753724
peterschrammel
approved these changes
Feb 5, 2019
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.
We were not regularly exercising this code outside unit tests, leading to
regressions on several tests. On my system, running this additional test takes
42 seconds, which is still better than users running into issues. (ctest -V -L
CORE -j8 takes an extra 10 seconds.)
Fixes: #3956