Remove two unnecessary fields from the Java object factory #4432
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
antlechner
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli,
smowton and
thk123
as code owners
owen-mc-diffblue
approved these changes
Mar 26, 2019
antlechner
force-pushed
the
antonia/object-factory-location
branch
from
3c49d89 to
8761c52
Compare
|
This failed CI because of a typo, which I fixed so it should pass now. |
allredj
reviewed
Mar 26, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 8761c52).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105827742
An instance of java_object_factoryt is only constructed in two places in the code. Both times, gen_nondet_init is immediately called on it with the same source location that was also passed to the constructor. Storing the same value both in a field and in function parameters is unnecessary, so the field is removed in this commit.
ns was supposed to always contain a pointer to symbol_table. This kind of class invariant is unnecessary. It is better to just work with the symbol table if possible, and construct a namespacet from it whenever we need it. This way the namespacet can always be declared const and we can easily see which functions make use of it.
antlechner
force-pushed
the
antonia/object-factory-location
branch
from
8761c52 to
dea4be5
Compare
allredj
reviewed
Mar 26, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: dea4be5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/105851506
peterschrammel
approved these changes
Mar 26, 2019
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No functional change.
The first commit is a follow-up PR to #4416, where it was requested in reviews. The second commit seemed related enough to include it in the same PR.