Add support for void* pointers in goto-harness #5290
Conversation
thk123
requested review from
chrisr-diffblue,
danpoe,
martin-cs and
peterschrammel
as code owners
Currently goto-harness crashes with this example.
This ensures they are simply set to null, avoiding a crash (or any strange initlization of memory of an unknown type)
Reduces duplication between the code that produces the different branches that return null
thk123
force-pushed
the
goto-harness-void-star-pointers
branch
from
9987033 to
46ce648
Compare
The current behaviour trips over an invariant. This is the only sesnible behaviour, as cannot sensibly malloc an array of void
thk123
force-pushed
the
goto-harness-void-star-pointers
branch
from
46ce648 to
ce0ec56
Compare
| if(type.subtype().id() == ID_empty) | ||
| { | ||
| // always initalize void* pointers as NULL | ||
| return build_null_pointer(result_symbol); |
There was a problem hiding this comment.
This is OK for now, but longer term we'll have to think of a better solution for this (although meaningful void* arguments are tricky, and tbh shouldn't be appearing very often in the sort of harnesses we're trying to generate right now).
There was a problem hiding this comment.
Feel free to raise a ticket - though tbh I'm not really sure what other useful behaviour exists. A non-det switch over all types? I guess we could do something similar to JBMC where we look at the subsequent casts to pick a type.
Here the array contains pointers, so we can sensibly create a non-null array here.
thk123
force-pushed
the
goto-harness-void-star-pointers
branch
from
ce0ec56 to
11a48f4
Compare
On Travis, these are printed out as assert 0 rather than assert false
| { | ||
| __CPROVER_assume(input_array != 0); | ||
| assert(input_array[0] == 0); | ||
| assert(false); |
There was a problem hiding this comment.
👍 A lot of tests forget this step
Codecov Report
@@ Coverage Diff @@
## develop #5290 +/- ##
========================================
Coverage 67.95% 67.95%
========================================
Files 1170 1170
Lines 96362 96371 +9
========================================
+ Hits 65478 65487 +9
Misses 30884 30884
Continue to review full report at Codecov.
|
Uh oh!
There was an error while loading. Please reload this page.