Skip to content

Make EXIT and SIGNAL patterns a requirement in test specifications #3618

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 2 commits into from
Feb 21, 2019
Merged

Make EXIT and SIGNAL patterns a requirement in test specifications #3618

merged 2 commits into from
Feb 21, 2019

Conversation

tautschnig
Copy link
Collaborator

This will make sure regression tests do not spuriously pass despite, e.g.,
failing an invariant.

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

allredj
allredj reviewed Dec 21, 2018
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: be59b3d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95529385

@tautschnig tautschnig force-pushed the exit-signal-mandatory branch from be59b3d to d8db26b Compare December 21, 2018 14:21
allredj
allredj reviewed Dec 21, 2018
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: d8db26b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95540565

@tautschnig
Copy link
Collaborator Author

@allredj @thk123 Heads-up: this might break TG tests, if those are also using test.pl. Please do a run and implement fixes similar to those in the first commit of this PR.

@tautschnig tautschnig force-pushed the exit-signal-mandatory branch from d8db26b to d6213f7 Compare January 3, 2019 12:19
@allredj
Copy link
Contributor

allredj commented Jan 3, 2019

Will process this one shortly. Please don't merge in the mean time.

allredj
allredj reviewed Jan 3, 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: d6213f7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96188312

@tautschnig tautschnig force-pushed the exit-signal-mandatory branch from d6213f7 to 874732e Compare January 4, 2019 15:18
allredj
allredj reviewed Jan 4, 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: 874732e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96323714

@tautschnig tautschnig force-pushed the exit-signal-mandatory branch from 874732e to 0ed760b Compare January 9, 2019 12:37
allredj
allredj reviewed Jan 9, 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: 0ed760b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96757780
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 force-pushed the exit-signal-mandatory branch 3 times, most recently from af1f5f0 to 19aaa26 Compare January 27, 2019 10:41
allredj
allredj reviewed Jan 27, 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: 19aaa26).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/98731462

@tautschnig tautschnig force-pushed the exit-signal-mandatory branch 3 times, most recently from cdf1659 to 94a3b75 Compare February 1, 2019 17:51
allredj
allredj reviewed Feb 1, 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: cdf1659).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99466991
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 3, 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: 94a3b75).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99537046

@tautschnig tautschnig force-pushed the exit-signal-mandatory branch from 94a3b75 to 1178a56 Compare February 5, 2019 11:39
allredj
allredj reviewed Feb 5, 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: 1178a56).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99774610

@romainbrenguier
Copy link
Contributor

This breaks our tests. Not that there is something wrong with the changes but rather that we use the perl script in a wrong way. @thk123 can we come up with a plan for that?

@tautschnig
Copy link
Collaborator Author

@romainbrenguier Is it more than just making the changes that I've had to make in this repo as documented in the first commit?

@tautschnig tautschnig assigned romainbrenguier and unassigned allredj Feb 6, 2019
@romainbrenguier
Copy link
Contributor

@romainbrenguier Is it more than just making the changes that I've had to make in this repo as documented in the first commit?

The error looks very different, so it seems a bit more complicated than that.

@tautschnig tautschnig force-pushed the exit-signal-mandatory branch 2 times, most recently from 4100fd4 to f721a3e Compare February 17, 2019 08:43
allredj
allredj reviewed Feb 17, 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: f721a3e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/101217387

@tautschnig tautschnig mentioned this pull request Feb 19, 2019
Closed
2 tasks
@tautschnig tautschnig added dependent - do not merge Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers and removed do not merge labels Feb 21, 2019
@tautschnig tautschnig force-pushed the exit-signal-mandatory branch from f721a3e to c0b12a8 Compare February 21, 2019 13:52
@tautschnig tautschnig removed Needs TG approval 🦉 Only merge with explicit approval from test-gen maintainers dependent - do not merge labels Feb 21, 2019
@tautschnig
Copy link
Collaborator Author

The EXIT and SIGNAL patterns are now only required if -e is specified, thus TG is free to omit them. Will merge as soon as CI passes.

@tautschnig
Add missing EXIT or SIGNAL specifications
8e013bc 
We should always check for these to avoid spuriously passing tests.
@tautschnig
test.pl: check for EXIT and SIGNAL patterns if -e is set
bb79432 
Using EXIT and SIGNAL patterns avoids spurious test successes despite, e.g.,
failing an invariant.
@tautschnig tautschnig force-pushed the exit-signal-mandatory branch from c0b12a8 to bb79432 Compare February 21, 2019 15:05
@tautschnig tautschnig merged commit e3ed7a5 into diffblue:develop Feb 21, 2019
@tautschnig tautschnig deleted the exit-signal-mandatory branch February 21, 2019 16:57
@tautschnig tautschnig restored the exit-signal-mandatory branch December 27, 2020 06:28
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

@kroening kroening kroening approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

Assignees

@tautschnig tautschnig

Labels
Tests
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@tautschnig @allredj @romainbrenguier @kroening @peterschrammel @thk123