Add tests for --java-assume-inputs-non-null #4503
Conversation
|
|
||
| public static void stringArrayArg(String[] arg) { | ||
| if (arg == null) { | ||
| assert false; |
There was a problem hiding this comment.
💡 It might make the tests a little easier to comprehend if you only put the assert false in the branches that shouldn't be covered.
Indeed could even be written as non-coverage style:
assert(arg != null)Then you only need to check for verification successful.
There was a problem hiding this comment.
I have a slight preference for the branching solution (using ifs) as I would like to keep both assertions (to be sure that a trace exists at all), and I don't want to make too many assumptions as to whether the assert acts as a guard or not.
allredj
force-pushed
the
tests-assume-inputs-non-null
branch
from
4558508 to
d0f608a
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: d0f608a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107658751
| ^EXIT=10$ | ||
| ^SIGNAL=0$ | ||
| ^VERIFICATION FAILED$ | ||
| [java::My.classArg:(LOther;)V.assertion.1].*SUCCESS |
There was a problem hiding this comment.
[ ] is for character sets
There was a problem hiding this comment.
Crap. Now escaped [ ] ( ).
allredj
force-pushed
the
tests-assume-inputs-non-null
branch
from
d0f608a to
83ec561
Compare
allredj
force-pushed
the
tests-assume-inputs-non-null
branch
from
83ec561 to
5ee583f
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 5ee583f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/107788971
I noticed that
--java-assume-inputs-non-nullwas untested in JBMC. Here are some tests that verify that the option actually does something for Strings, arrays of Strings, and user-defined objects.I also discovered that class fields were not affected by this option (as they are presumably considered to be fields of
this, and the option does not extend to fields of inputs). Whether or not this was intentional, that behaviour is now documented by tests.