Constant propagation of CProverString.setLength() and CProverString.setCharAt() #5134
Conversation
danpoe
requested review from
cesaro,
cristina-david,
kroening,
peterschrammel,
pkesseli,
romainbrenguier,
smowton,
tautschnig and
thk123
as code owners
|
|
||
| public class Test | ||
| { | ||
| public void testSuccess1() |
There was a problem hiding this comment.
No negative tests? Setting out of range for example?
There was a problem hiding this comment.
I've not included test cases for the error cases here as those will be handled by the models in the future. I'll add tests for those cases once we have models that use the CProverString primitives.
There was a problem hiding this comment.
Sure but we should check that they aren't accidentally const propagated?
There was a problem hiding this comment.
Fair enough, added more tests.
| public void testSuccess1() | ||
| { | ||
| StringBuffer sb = new StringBuffer("abc"); | ||
| CProverString.setLength(sb, 0); |
There was a problem hiding this comment.
Test setting to same length (i.e. 3 in this case)
|
|
||
| public void testSuccess3() | ||
| { | ||
| StringBuffer sb = new StringBuffer("abc"); |
There was a problem hiding this comment.
Test extension by more than one char
danpoe
force-pushed
the
feature/constant-propagation-of-string-operations
branch
3 times, most recently
from
ac6103a to
a966852
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: a966852).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/129478144
danpoe
force-pushed
the
feature/constant-propagation-of-string-operations
branch
from
a966852 to
2c6c2a9
Compare
Only minimal tests are added at this point. The error conditions (like index out of bounds) will be handled by the models. Once we have models that use CProverString.setLength(), more comprehensive tests will be added.
Only minimal tests are added at this point. The error conditions (like index out of bounds) will be handled by the models. Once we have models that use CProverString.setCharAt(), more comprehensive tests will be added.
danpoe
force-pushed
the
feature/constant-propagation-of-string-operations
branch
from
2c6c2a9 to
4bb03aa
Compare
Uh oh!
There was an error while loading. Please reload this page.