-
Notifications
You must be signed in to change notification settings - Fork 274
move string solver into separate directory #3753
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
kroening
commented
Jan 10, 2019
- Each commit message has a non-empty body, explaining why the change was made.
- n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
93971d3
to
2d77eda
Compare
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.
This seems to be missing a git add
, the files have just been removed, not re-added. And likely it will need a clang-format
with results to go in a separate commit to make CI happy.
84ae0f8
to
69f67d4
Compare
0364fae
to
628181c
Compare
263b436
to
edada49
Compare
edada49
to
46e2151
Compare
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.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 46e2151).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97658054
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
46e2151
to
3762599
Compare
Rebased and updated the test-gen pointer bump. Once both pass CI, I'll merge this. |
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.
✔️
Passed Diffblue compatibility checks (cbmc commit: 3762599).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98022743
The refinement solver a part of the string solver, but can live on its own, and thus, shouldn't use its exception class.
The string solver is now large enough to justify a separate directory.
3762599
to
93a0994
Compare
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.
✔️
Passed Diffblue compatibility checks (cbmc commit: 93a0994).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98064757