Correct nondet init of function pointer arguments

[xbauch]

At least until handling of function pointers is transferred to symex.

1. The nondet symbol factory only assigns nondet to function pointers, i.e. does
   not build the depth deep pointer tree.
2. The function pointer removal checks if the pointer is an argument to the
   entry point and if so, skips adding the assume(false) for cutting short the
   execution in case on function target was found.

add 2: On the GOTO level, the function call is replaced with return_value
which is never assigned to.

Notes:

• this is an alternative/extension to Stop generating nondet pointees for function pointers #4940 which only changed the factory.

• both PRs try to fix Non-deterministic initialisation of function pointers is broken #4937.

• Each commit message has a non-empty body, explaining why the change was made.

• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.

• 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).

• 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.

[hannes-steffenhagen-diffblue]

Can you explain here why this is better than #4940, which seems to be the more intuitive way to do this on the surface level at least? I guess this doesn’t handle functions where we don’t have functions with matching signatures, so you’re adding a new one here that can be called instead? That doesn’t seem like an unreasonable thing to do here either, but I suspect that the behaviour may be surprising for some people (it’s a bit hard to say what the correct behaviour for an arbitrary function pointer should be, and this makes this happen silently).

Does the function pointer removal currently add assertions to check that it can resolve the function pointer? If not, this could be one thing to “fix” to alert users to such a problem and maybe tell them to just write a function implementing the behaviour they want to test for themselves.

[xbauch]

Superseded by #4940 and to be closed, eventually.

[xbauch]

#4940 was merged, and solved the issue.