Skip to content

remove_returns now preserves signature #4266

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 1 commit into from
Mar 14, 2019
Merged

remove_returns now preserves signature #4266

merged 1 commit into from
Mar 14, 2019

Conversation

kroening
Copy link
Member

This simplifies removal, and removes the need to query the 'original' return
type.

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

@kroening kroening force-pushed the remove-returns-preserve-return-type branch 2 times, most recently from e60c7c8 to 460c788 Compare February 25, 2019 10:16
@kroening kroening marked this pull request as ready for review February 25, 2019 10:40
@tautschnig
Copy link
Collaborator

This is currently hidden by a checker that ignores the return type, for a
wrong reason.

Could you please elaborate? Notably, that test was introduced in #3089 together with changes (only) to remove_returns.

allredj
allredj reviewed Feb 25, 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: 460c788).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102144138
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.

@kroening kroening mentioned this pull request Feb 27, 2019
Merged
6 tasks
sonodtt pushed a commit to sonodtt/cbmc that referenced this pull request Mar 1, 2019
Address review comments - Kroening
971c788 
Removed previously disabled checks:
Not every instruction has a code member - so removed checks that both 
instruction sourcelocation and code sourcelocation are set and identical
Remove also remaining check that every instruction have a non-nil 
sourcelocation as this would have to be optional (if enabled fails 
many regression tests). This also simplifies considerably the overall 
validation pass (removes much passing around of the options structure).

Removes check on function return type - this will be preserved (diffblue#4266)

goto_model::validate now has default parameters.

Minor fixes.
sonodtt pushed a commit to sonodtt/cbmc that referenced this pull request Mar 1, 2019
Address review comments - Kroening
b5b1f64 
Removed previously disabled checks:
Not every instruction has a code member - so removed checks that both 
instruction sourcelocation and code sourcelocation are set and identical
Remove also remaining check that every instruction have a non-nil 
sourcelocation as this would have to be optional (if enabled fails 
many regression tests). This also simplifies considerably the overall 
validation pass (removes much passing around of the options structure).

Removes check on function return type - this will be preserved (diffblue#4266)

goto_model::validate now has default parameters.

Minor fixes.
@kroening kroening force-pushed the remove-returns-preserve-return-type branch from 460c788 to 696b1f4 Compare March 3, 2019 12:13
allredj
allredj reviewed Mar 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.

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 696b1f4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102950599
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

@kroening kroening force-pushed the remove-returns-preserve-return-type branch from 696b1f4 to 1365203 Compare March 5, 2019 16:06
allredj
allredj reviewed Mar 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.

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 1365203).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103247677
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

@kroening kroening force-pushed the remove-returns-preserve-return-type branch from 1365203 to 476b698 Compare March 14, 2019 10:40
remove_returns now preserves signature
aecd491 
This simplifies removal, and removes the need to query the 'original' return
type.
@kroening kroening force-pushed the remove-returns-preserve-return-type branch from 476b698 to aecd491 Compare March 14, 2019 10:59
allredj
allredj reviewed Mar 14, 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: 476b698).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104397771
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

allredj
allredj reviewed Mar 14, 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: aecd491).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/104402256
Status will be re-evaluated on next push.
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 compatibility was already broken by an earlier merge.

smowton
smowton approved these changes Mar 14, 2019
View reviewed changes
Copy link
Contributor

@smowton smowton left a comment

Choose a reason for hiding this comment

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

One suggestion: document in remove_returns.h what the new contract is (leave the signature alone but leave the . return value undefined?)

@kroening
Copy link
Member Author

@smowton I felt that the documentation is reasonably clear -- what do you mean by "leave the . return value undefined"? The #return_value variable is set, which is nicely illustrated towards the end of the comment block.

@smowton
Copy link
Contributor

smowton commented Mar 14, 2019

I mean if the type indicates it returns int, then we have both the "natural" return value and the global. Subsequent passes need to know that return type and return behaviour may no longer coincide, whereas previously the void return type meant a naive pass would also do fine, as the function really was void-typed.

@kroening
Copy link
Member Author

Ah; that may be a matter of viewpoint. My view is that we have two different semantics for goto-programs, one with return instructions, and one without. The "without" semantics is a strict subset of the one "with", which implies that you don't actually need to know which to apply.

@kroening kroening merged commit df04421 into develop Mar 14, 2019
@kroening kroening deleted the remove-returns-preserve-return-type branch March 14, 2019 18:54
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

@tautschnig tautschnig tautschnig approved these changes

@cesaro cesaro Awaiting requested review from cesaro

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

@cristina-david cristina-david Awaiting requested review from cristina-david

@NathanJPhillips NathanJPhillips Awaiting requested review from NathanJPhillips

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

@pkesseli pkesseli Awaiting requested review from pkesseli

@thk123 thk123 Awaiting requested review from thk123

Assignees

@kroening kroening

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@kroening @tautschnig @smowton @allredj