Skip to content

Cleanup of SMT2 solver test execution and CMake support [blocks: #4063] #4121

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 4 commits into from
Feb 14, 2019
Merged

Cleanup of SMT2 solver test execution and CMake support [blocks: #4063] #4121

merged 4 commits into from
Feb 14, 2019

Conversation

tautschnig
Copy link
Collaborator

I'd suggest reviewing commit-by-commit.

  • 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.

@tautschnig tautschnig force-pushed the smt-solver-cmake-tests branch from 5291dcd to b68b68b Compare February 7, 2019 16:54
@tautschnig tautschnig changed the title Cleanup of SMT2 solver test execution and CMake support Cleanup of SMT2 solver test execution and CMake support [blocks: #4121] Feb 7, 2019
@tautschnig tautschnig changed the title Cleanup of SMT2 solver test execution and CMake support [blocks: #4121] Cleanup of SMT2 solver test execution and CMake support [blocks: #4063] Feb 7, 2019
@tautschnig tautschnig force-pushed the smt-solver-cmake-tests branch from b68b68b to 9632c6b Compare February 7, 2019 17:58
allredj
allredj reviewed Feb 7, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a 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: b68b68b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100124409
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.

allredj
allredj reviewed Feb 7, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a 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: 9632c6b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100143902

romainbrenguier
romainbrenguier reviewed Feb 8, 2019
View reviewed changes
regression/cbmc/Makefile
@@ -4,7 +4,7 @@ test:
@../test.pl -p -c "../../../src/cbmc/cbmc --validate-goto-model" -X smt-backend

test-cprover-smt2:
@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The commits are in the wrong order, this should go after the broken-smt-backend tag is introduced

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that's just GitHub displaying them in the wrong order, but let me make this unambiguous by moving this particular change into the same commit that introduces the tag.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can update the commit date to make github display them in the right order git rebase "$(git merge-base HEAD origin/develop)" --ignore-date -x 'git commit --amend -C HEAD --date="$(date -R)" && sleep 1.05' -i

regression/cbmc/Anonymous_Struct3/test.desc
@@ -1,4 +1,4 @@
CORE
CORE broken-smt-backend
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

typo in commit message? "easier to repeated build" -> "easier to repeatedly build"?
"regression test" -> "regression tests"?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks a lot!

regression/cbmc/CMakeLists.txt
@@ -8,3 +8,15 @@ add_test_pl_profile(
"-C;-X;thorough-paths;-X;smt-backend;-s;paths-lifo"
"CORE"
)

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

typo in commit message: "partity"

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, fixed!

@tautschnig
Add a broken-smt-backend tag to regression tests and use it
4fc2f58 
This will enable dropping the script that deletes directories, and thus makes it
easier to do repeated build&test runs.
@tautschnig
Remove delete-failing-SMT-solver tests script
3b2500b 
With the new tag introduced in the preceding commit this is no longer needed.
This actually simplifies our CI scripts.
@tautschnig
Enable SMT2 solver tests on Windows
7f9e8d3 
There is no reason the solver shouldn't be tested on Windows.
@tautschnig
Run SMT solver tests in CMake/CTest builds
3fc215c 
This will help us get towards feature parity between Makefile and CMake-based
set-ups.
@tautschnig tautschnig force-pushed the smt-solver-cmake-tests branch from 9632c6b to 3fc215c Compare February 8, 2019 12:53
romainbrenguier
romainbrenguier approved these changes Feb 8, 2019
View reviewed changes
Copy link
Contributor

@romainbrenguier romainbrenguier left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should wait for CI but it's a good thing to do

allredj
allredj reviewed Feb 8, 2019
View reviewed changes
Copy link
Contributor

@allredj allredj left a 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: 3fc215c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/100235492

@tautschnig tautschnig mentioned this pull request Feb 13, 2019
Closed
@tautschnig tautschnig merged commit f4ed82a into diffblue:develop Feb 14, 2019
@tautschnig tautschnig deleted the smt-solver-cmake-tests branch February 14, 2019 07:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj left review comments

@smowton smowton smowton approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@romainbrenguier romainbrenguier romainbrenguier approved these changes

@chrisr-diffblue chrisr-diffblue Awaiting requested review from chrisr-diffblue

@forejtv forejtv Awaiting requested review from forejtv

@kroening kroening Awaiting requested review from kroening kroening is a code owner

@thk123 thk123 Awaiting requested review from thk123

Assignees

@tautschnig tautschnig

Labels
blocker Build Tests
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
7 participants
@tautschnig @smowton @peterschrammel @romainbrenguier @allredj @kroening @chrisr-diffblue