Allow function pointer arguments to be equal #5171
Conversation
for the function-call goto-harness. We add a new command-line option `treat-pointers-equal` that takes a list of formal parameter names and results in a harness that only generates constructor for one of the pointers. The other pointers are simply assigned with the constructed one.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 9db8bd4).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/134853929
xbauch
requested review from
chrisr-diffblue,
danpoe,
hannes-steffenhagen-diffblue,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
This is currently only capable of expressing that a single set of function params should be treated equal, I'd like this to be able to specify multiple (non-overlapping I'd hope?) sets of possibly equal pointers.
Also, these should be maybe equal, but as currently specified they'll definitely be equal, which is a bit unfortunate (as now we won't be covering the case where they're not equal, we'd have to generate a different harness for these again).
|
|
||
| bool recursive_initializationt::needs_freeing(const exprt &expr) const | ||
| { | ||
| if(expr.type().id() != ID_pointer) |
There was a problem hiding this comment.
Function pointers also shouldn't be freed but we're already fixing this in a follow up PR
Specified by a semi-colon separated list of comma separated names.
Codecov Report
@@ Coverage Diff @@
## develop #5171 +/- ##
===========================================
+ Coverage 67.32% 67.33% +0.01%
===========================================
Files 1155 1155
Lines 94643 94708 +65
===========================================
+ Hits 63715 63773 +58
- Misses 30928 30935 +7
Continue to review full report at Codecov.
|
|
@hannes-steffenhagen-diffblue both sets of equal pointers and conditional equality should be implemented now. |
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: dcf0ea3).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/136572662
| { | ||
| for(auto const &value : values) | ||
| { | ||
| for(auto const ¶m_cluster : split_string(value, ';')) |
There was a problem hiding this comment.
Super minor nitpick that ; might not necessarily be the best separator to use here because on most shells it’s also a terminator, but tbh I don’t think it’s big enough of a problem to worry about here.
|
|
||
| bool recursive_initializationt::needs_freeing(const exprt &expr) const | ||
| { | ||
| if(expr.type().id() != ID_pointer || expr.type().id() == ID_code) |
There was a problem hiding this comment.
This could just be return expr.type().id() = ID_pointer && expr.type().id() != ID_code;
| @@ -280,6 +321,19 @@ bool recursive_initializationt::should_be_treated_as_array( | |||
| initialization_config.pointers_to_treat_as_arrays.end(); | |||
| } | |||
|
|
|||
| optionalt<std::size_t> | |||
There was a problem hiding this comment.
Small preference to have a (strong?) typedef for this size_t so we know that it refers to an “equal cluster”
| initialization_config.arguments_may_be_equal) | ||
| { | ||
| // in equality cluster but not common origin -> free if equal to origin | ||
| const auto condition = |
There was a problem hiding this comment.
I don’t quite understand the logic, shouldn’t it be the other way round (i.e. don’t free if not common origin, unless your value is different than origin)?
There was a problem hiding this comment.
Off by negation: good catch. Fixed.
xbauch
force-pushed
the
feature/function-harness-param-equal
branch
from
019194f to
f95df53
Compare
between pointer arguments. Whether or not they will be equal is now a non-deterministic choice. Freeing pointer had to be extended.
xbauch
force-pushed
the
feature/function-harness-param-equal
branch
from
f95df53 to
49b86dc
Compare
…ondet-harness Function pointer non-det initialisation in goto-harness [depends-on: #5171]
for the function-call goto-harness.
We add a new command-line option
treat-pointers-equalthat takes a list offormal parameter names and results in a harness that only generates constructor
for one of the pointers. The other pointers are simply assigned with the
constructed one.