Feature nondet array initialization [blocks: #3572] #3750
Conversation
hannes-steffenhagen-diffblue
requested review from
kroening,
peterschrammel,
pkesseli,
smowton and
tautschnig
as code owners
hannes-steffenhagen-diffblue
changed the title
| /// \param malloc_symbol_name The name of the malloc function | ||
| const symbolt &gen_malloc_function(const irep_idt &malloc_symbol_name); | ||
|
|
||
| void gen_array_allocation( |
There was a problem hiding this comment.
Can we get some documentation on this?
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 2dc02c3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96936329
hannes-steffenhagen-diffblue
force-pushed
the
feature-nondet-array-initialization-split
branch
from
2dc02c3 to
23c1ab3
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 23c1ab3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96943865
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.
|
This expands the command line option set too significantly -- please do in goto-instrument! |
This adds a function that generates a malloc function that replicates the behaviour of malloc from CBMCs stdlib implementation. This is useful in situations in which we can't rely on malloc being present.
This enables derived classes to implement their own language specific options
Adds the --pointers-to-treat-as-arrays --associated-array-sizes --max-dynamic-array-size options. The intended behaviour is that the former should indicate which of the function parameters to an entry function that are pointers should be backed by an array, the parameter that should hold the size of that array (if any) and the maximum size of such an array (minimum 1) respectively. These options currently have no effect and will be implemented in a later commit
hannes-steffenhagen-diffblue
force-pushed
the
feature-nondet-array-initialization-split
branch
2 times, most recently
from
6cd1d6b to
b53db4f
Compare
This implements the behaviour of the --pointers-to-treat-as-arrays --associated-array-sizes --max-dynamic-array-size options.
hannes-steffenhagen-diffblue
force-pushed
the
feature-nondet-array-initialization-split
branch
from
b53db4f to
14e8833
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: b53db4f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97425323
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.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 14e8833).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97429703
|
@kroening has suggested putting the new command line options in goto-instrument instead of cbmc. |
|
To clarify: My understanding is that the idea was to create a new option to goto-instrument to create a harness for a function (i.e. something along the lines of |
|
@kroening @tautschnig @peterschrammel As a general note, given that the entry point/harness generation is language-specific, should there be a way of specifying in goto-instrument which language feature to use? We could have an option |
|
It was suggested by @tautschnig to move harness generation to a new command line tool entirely that would only do harness generation. Would you be alright with that as well? |
|
@hannes-steffenhagen-diffblue @johnnonweiler Indeed, #3251 should move along with this! |
|
I think it'd make more sense to have it take and output /change a goto binary the same way goto instrument works |
|
Closed as we decided to do this another way |
This PR adds options that let a user generate initialisation code for "dynamic" array parameters (i.e. pointers which point to an array, optionally coupled with a parameter holding their size). This is "opt-in", i.e. the user has to declare which of their function parameters are meant to be arrays (and which parameter holds the size of which array, if any).