Allocate nondet char array #3259
Conversation
romainbrenguier
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli,
smowton and
thk123
as code owners
|
Tests will be added here: https://github.com/diffblue/test-gen/pull/2441 |
|
A unit test needs to be updated |
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 05cddb1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90242967
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
| { | ||
| side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location()); | ||
| alloc.copy_to_operands(size); | ||
| alloc.copy_to_operands(false_exprt()); |
There was a problem hiding this comment.
Use add_to_operands (allows move)
tautschnig
assigned romainbrenguier and unassigned smowton, NathanJPhillips and peterschrammel
make_nondet_infonite_char_array was not allocating the array as a dynamic object. This means if this code was added in a function called several time then the array would get overwritten each time. This problem was not visible by the string refinement as it associates a independent array to each string and does not care about memory allocation, but can be a problem for the interpreter.
The string creation in java_object_factory was allocating a char array, which is already done in make_nondet_char_array. We remove the duplicate allocation and simplify make_nondet_infinite_char_array by using make_allocate_code which was used in the java_object_factory version.
romainbrenguier
force-pushed
the
bugfix/allocate-nondet-char-array
branch
from
05cddb1 to
130c190
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 130c190).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90382716
make_nondet_infonite_char_arraywas not allocating the array as adynamic object. This means if this code was added in a function called
several times then the array would get overwritten each time.
This problem was not visible by the string refinement as it associates a
independent array to each string and does not care about memory
allocation, but can be a problem for the interpreter.