The observed behavior is the intended one, and is not (in our opinion) unsound. We sacrifice generality for precision and ease of use. More precisely, we make assumptions on what the functions without a body do, so that the analysis does not degenerate too early. It is up the user to check that those assumptions hold, or to stub the functions without a body appropriately.
## How to see that the analysis is unfinished:
First, notice that a warning is emitted to signal that the the analysis of 'f' may be/is probably incorrect:
unsound.c:12:[kernel] warning: Neither code nor specification for function f, generating default assigns from the prototype
If you inspect the statuses of those 'assigns' clauses afterwards, either in the GUI or with the Report plugin, you will see that they have 'Unknown' status. For the program to be deemed correct, they would need to have 'Valid' or 'Considered Valid' status.
## How to model the call to 'f'?
The two possibilities are either to write a C body, or to write assigns/from clauses. In this particular case, a proper clause is
//@ assigns **p \from \nothing;
void f(int **p);
## Where is this documented?
Section 5.2.8 of the manual is the most explicit (but should probably be made even clearer). Functions without body are also mentioned in Section 4.4.3. Detailed explanations on how to write proper assigns/from clauses are given in Section 7.2. I am interested in feedback on what could be improved regarding this topic.
> At the call to f(x), I think you should grab all the base addresses that are
> reachable by the arguments and set them to TOP.
Indeed, this would be sound. But:
1) this would include all global variables, resulting later on in an almost completely imprecise analysis
2) this cannot be expressed in ACSL for the global variables, and only with difficulty for the local ones.