Don't warn on array_of_expr with zero length #1013
Conversation
|
Working with zero-sized arrays seems wrong - would it be possible to get a pointer to a regression test? |
|
https://github.com/diffblue/cbmc/tree/test-gen-support/regression/cbmc-java/NondetArray2 running against current test-gen-support with latest master merged (e.g. here: https://github.com/smowton/cbmc/tree/smowton/merge/master_20170614) Basically |
|
Oh, I was not aware that this was coming from Java. We should certainly have this backed by a regression test to document the context in which this is expected. |
These result from array_set instructions, which when targeting variable-length arrays can end up targeting zero-sized arrays.
This should compile warning-free, since it is legal Java. Previously an array_of expression with nil length yielded a warning, as would a WITH based upon one.
smowton
force-pushed
the
smowton/fix/array_of_zero_length
branch
from
e967fd0 to
677f39d
Compare
|
Added a test and made the checks a little more precise. I considered avoiding calling Also I note that https://github.com/diffblue/cbmc/blob/master/src/solvers/flattening/boolbv_if.cpp#L17 already tolerates a zero-length bitvector, so I think it's probably okay to pass these in other places too. |
| { | ||
| // A zero-length array is acceptable; | ||
| // an element with unknown size is not. | ||
| if(boolbv_width(array_type.subtype())==0) |
There was a problem hiding this comment.
What about arrays of arrays of zero length? Would Java permit that? If so, this check needs to be amended.
There was a problem hiding this comment.
No, at least in Java such a thing would be an array of pointers
|
I'm not sure what's going on here with regard to the build checks... |
|
Re: checks I accidentally pushed to origin/smowton/... instead of smowton/smowton/... and then deleted the branch created in error. I think the /push and /branch ones relate to that and the PR ones are working as intended. |
These result from array_set instructions, which when targeting variable-length arrays can end up targeting zero-sized arrays.
Some regression tests in test-gen-support are currently not looking for
warning: ignoringbecause of this.