Skip to content

Conversation

@kroening
Copy link
Collaborator

@kroening kroening commented Nov 3, 2018

  • 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.
  • 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.
  • White-space or formatting changes outside the feature-related changed lines are in commits of their own.

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: f73969c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90165384
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.

Copy link
Collaborator

@tautschnig tautschnig left a comment

Choose a reason for hiding this comment

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

Do the SMT-solver backed tests exercise this bit of code? If so, could an explicit test be added?

@tautschnig tautschnig assigned kroening and unassigned tautschnig Nov 4, 2018
@kroening
Copy link
Collaborator Author

kroening commented Nov 5, 2018

We can add a test either if
a) we activate the SMT-backend tests and have a solver that supports unbounded integers; or
b) we add (at least basic) support for unbounded integers to the internal solver.

@tautschnig
Copy link
Collaborator

We already have regression/cbmc/integer-assignments1, maybe that should include some patterns to inspect the trace output?

@kroening
Copy link
Collaborator Author

kroening commented Nov 5, 2018

Indeed, done

^EXIT=10$
^SIGNAL=0$
^ b=100
^ b=100 (0b1100100)$
Copy link
Collaborator

Choose a reason for hiding this comment

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

The parentheses will need escaping. (CI currently passes as we don't have SMT in there yet.)

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

done

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: a4462eb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90246246
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.

@tautschnig tautschnig merged commit 11a98d8 into develop Nov 5, 2018
@tautschnig tautschnig deleted the smt2-integer branch November 5, 2018 13:09
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: 4e87b90).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90264632

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants