Skip to content

Replace Object.getClass preprocessing by a CProver.classIdentifier method #4513

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 3 commits into from
Apr 11, 2019
Merged

Replace Object.getClass preprocessing by a CProver.classIdentifier method #4513

merged 3 commits into from
Apr 11, 2019

Conversation

romainbrenguier
Copy link
Contributor

This simplifies the preprocessing and leave it to the model to handle
the complexity, which is less error-prone.

  • Each commit message has a non-empty body, explaining why the change was made.
  • [na] 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).
  • [na] My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • [na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@romainbrenguier
Copy link
Contributor Author

There is a test for getClass in jbmc/regression/jbmc-strings/ClassName but I will add others for the new CProver.classIdentifier.

@romainbrenguier romainbrenguier force-pushed the bugfix/get-class branch 2 times, most recently from 3ef4482 to d4079e6 Compare April 11, 2019 08:48
@romainbrenguier
Copy link
Contributor Author

There is a test for getClass in jbmc/regression/jbmc-strings/ClassName but I will add others for the new CProver.classIdentifier.

Test added

allredj
allredj reviewed Apr 11, 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: d4079e6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107932717

allredj
allredj approved these changes Apr 11, 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.

Looks good!

@allredj
Copy link
Contributor

allredj commented Apr 11, 2019

java-models-library PR needs to be merged first, then the pointer updated, then this can go in.

@romainbrenguier
Update for diffblue/java-models-library#21 (getClass)
e440311 
Update the models for a version of getClass which uses
CProver.classIdentifier.
This is necessary for getting rid of the preprocessing of getClass which
is error-prone.
diffblue/java-models-library#21
@romainbrenguier
Replace getClass preprocess by CProver.classIdentifier
984bf19 
This simplifies the preprocessing and leave it to the model to handle
the complexity, which is less error-prone (writing safe java program is
easier than write c++ that generates safe goto-program).
@romainbrenguier
Add test for CProver.classIdentifier
d841712 
This tests that the new builtin cprover function is working.
@romainbrenguier
Copy link
Contributor Author

java-models-library update now pointing to master

allredj
allredj reviewed Apr 11, 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: d841712).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107948360

@romainbrenguier romainbrenguier merged commit 0f68971 into diffblue:develop Apr 11, 2019
@romainbrenguier romainbrenguier deleted the bugfix/get-class branch April 11, 2019 12:34
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@allredj allredj allredj approved these changes

@smowton smowton smowton 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

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

@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

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

@thk123 thk123 Awaiting requested review from thk123

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@romainbrenguier @allredj @smowton