Add regression tests for [TG-8284] #4939
Conversation
yumibagge
force-pushed
the
yb/jbmc-regression-tg-8284
branch
from
ddf0358 to
0557ee5
Compare
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 5ef594d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120229016
Codecov Report
@@ Coverage Diff @@
## develop #4939 +/- ##
========================================
Coverage 69.27% 69.27%
========================================
Files 1307 1307
Lines 108145 108145
========================================
Hits 74918 74918
Misses 33227 33227Continue to review full report at Codecov.
|
yumibagge
force-pushed
the
yb/jbmc-regression-tg-8284
branch
from
5ef594d to
723312f
Compare
| assert s1.indexOf(b) == 1; | ||
| assert s1.indexOf(b, -10) == 1; | ||
| assert s1.indexOf(b, 3) == 4; | ||
| assert s1.indexOf(b, 10) == -1; |
There was a problem hiding this comment.
In cbmc, it's generally not enough to check for assertion success. After all, cbmc's job is to violate assertions, so if there's nothing to violate, we can't tell if cbmc did anything at all.
I recommend looking at the tests in https://github.com/diffblue/cbmc/tree/develop/jbmc/regression/jbmc-strings/CompareToConstantEvaluation that exercise failing assertions.
There was a problem hiding this comment.
Thanks for the great advice and reference. Indeed, I had a test.desc for this test that does not use models-library, which is verification is expected to be failed. Is it better to add the test? The detailed verification failure is https://diffblue.atlassian.net/browse/TG-8284?focusedCommentId=23418&page=com.atlassian.jira.plugin.system.issuetabpanels%3Acomment-tabpanel#comment-23418
There was a problem hiding this comment.
That test you link doesn't look like one you would want to add. It fails on a NullPointerException, which is not what you're looking for. Happy to discuss in person.
There was a problem hiding this comment.
@allredj , I added a test to check assertion failure. Could you re-review?
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 723312f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120479078
yumibagge
force-pushed
the
yb/jbmc-regression-tg-8284
branch
from
723312f to
9cddf5d
Compare
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 9cddf5d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120755220
| Main.class | ||
| --function Main.constantIndexOf | ||
| ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$ | ||
| ^VERIFICATION FAILED$ |
There was a problem hiding this comment.
I think you should specify which assertion you want to fail. It's probably good to use the --property option too, as you don't want to analyse the assertions that you expect to be successful.
Look at the tests in https://github.com/diffblue/cbmc/tree/develop/jbmc/regression/jbmc-strings/CompareToConstantEvaluation
There was a problem hiding this comment.
Yes ... it was pointed out by @danpoe when he explained to me about regression tests. I was just being lazy 😅 property added.
yumibagge
force-pushed
the
yb/jbmc-regression-tg-8284
branch
from
9cddf5d to
5352996
Compare
allredj
left a comment
allredj
left a comment
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 5352996).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/120836927
4 participants
This PR addresses
regression folder rename
add regression test for models-library
add regression test for Character
n/a Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.