Skip to content

[TG-6381] Set opaque fields as final #4439

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
Apr 3, 2019
Merged

[TG-6381] Set opaque fields as final #4439

merged 2 commits into from
Apr 3, 2019

Conversation

majakusber
Copy link

@majakusber majakusber commented Mar 26, 2019 •
edited
Loading

Previously, we implicitly assumed that stub/opaque fields are not final and thus they can be assigned directly which causes problems if the field is actually final. Since we don;t know any better, we must assume all opaque fields are final.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • 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).
  • 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.

@majakusber majakusber self-assigned this Mar 26, 2019
@majakusber majakusber requested a review from allredj March 26, 2019 17:29
thk123
thk123 approved these changes Mar 26, 2019
View reviewed changes
jbmc/unit/java_bytecode/java_bytecode_language/language.cpp
{
const symbolt &opaque_field_symbol =
symbol_table.lookup_ref(opaque_class_prefix + ".field1");
REQUIRE(opaque_field_symbol.type.get_bool(ID_C_constant));
Copy link
Contributor

Choose a reason for hiding this comment

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

⛏️ @thomasspriggs was going to look at a nice way of accessing properties of static fields (since them being comments on the type is a bit unstable) perhaps in a follow up PR you can do whatever he ends up doing.

Copy link
Author

Choose a reason for hiding this comment

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

Good point, Tom passed me his PRs so I will follow up on that.

smowton
smowton approved these changes Mar 27, 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.

OK considering we don't use stub-side-effects widely, will limit the solution space when we do though.

@majakusber majakusber force-pushed the opaque-fields-final branch 4 times, most recently from 3a5a22b to b4b9f24 Compare April 2, 2019 14:06
allredj
allredj reviewed Apr 2, 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: b4b9f24).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106750508

@majakusber
Copy link
Author

I added the Do not merge label because I'm still working on the test-gen bump (needs to adjust tests) https://github.com/diffblue/test-gen/pull/3240

svorenova added 2 commits April 2, 2019 16:56
Set opaque fields as final
17a03a3 
Both static and non-static opaque (stub) fields should be considered
final to avoid assuming they can be overridden
Add unit tests to check opaque fields are final
1c4444a
@majakusber majakusber force-pushed the opaque-fields-final branch from b4b9f24 to 1c4444a Compare April 2, 2019 15:56
allredj
allredj reviewed Apr 2, 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: 1c4444a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/106770545

@majakusber
Copy link
Author

Test-gen bump passed CI, merging.

@majakusber majakusber merged commit d9694d5 into diffblue:develop Apr 3, 2019
@majakusber majakusber deleted the opaque-fields-final branch April 3, 2019 09:11
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

@thk123 thk123 thk123 approved these changes

@cesaro cesaro Awaiting requested review from cesaro

@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

Assignees

@majakusber majakusber

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@majakusber @smowton @thk123 @allredj