fix exprt::opX accesses in java_bytecode #5018
Merged
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
kroening
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli,
smowton and
thk123
as code owners
NathanJPhillips
approved these changes
Aug 14, 2019
smowton
reviewed
Aug 14, 2019
| @@ -916,8 +916,9 @@ void add_java_array_types(symbol_tablet &symbol_table) | |||
|
|
|||
| side_effect_exprt inc(ID_assign, typet(), location); | |||
| inc.operands().resize(2); | |||
| inc.op0()=index_symexpr; | |||
| inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type())); | |||
| to_binary_expr(inc).op0() = index_symexpr; | |||
There was a problem hiding this comment.
Let's introduce side_effect_expr_assignt instead?
| @@ -494,20 +493,23 @@ optionalt<codet> java_bytecode_instrumentt::instrument_expr(const exprt &expr) | |||
| { | |||
| // this corresponds to a throw and so we check that | |||
| // we don't throw null | |||
| result.add(check_null_dereference(expr.op0(), expr.source_location())); | |||
| result.add(check_null_dereference( | |||
| to_unary_expr(expr).op(), expr.source_location())); | |||
There was a problem hiding this comment.
We have side_effect_expr_throwt
There was a problem hiding this comment.
yes, but that doesn't have operands -- will make that a separate PR.
| } | ||
| else if(statement==ID_java_new_array) | ||
| { | ||
| // this corresponds to new array so we check that | ||
| // length is >=0 | ||
| result.add(check_array_length(expr.op0(), expr.source_location())); | ||
| result.add(check_array_length( | ||
| to_multi_ary_expr(expr).op0(), expr.source_location())); |
There was a problem hiding this comment.
Add a container for java_new_array?
allredj
reviewed
Aug 14, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: d85e24f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/123241525
This improves type safety.
kroening
force-pushed
the
java_bytecode-opX
branch
from
d85e24f to
185a3c3
Compare
allredj
reviewed
Aug 15, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 185a3c3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/123355159
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.
This improves type safety.