Fatal error in `strcmp` in callbacks passing through a function with missing definition

[jprotopopov-ut]

Goblint version: nightly sha256 68ef67776c7533bf4e89251efc5855c313dc92d7c257a7f357791595c8a8d7db

When analyzing the following snippet with Goblint in default configuration:

extern int strcmp(const char *, const char *);

static int hello_read(const char *path) {
    return strcmp(path, "Hello");
}

static const struct ops {
	int (*read)(const char *);
} hello_oper = {
	.read = hello_read,
};

extern int main_real(const struct ops *);

int main() {
	return main_real(&hello_oper);
}

it fails with

Fatal error: exception Failure("String function: not an address")

where one would expect Function definition missing for .... The issue is configuration-dependent. In particular with conf/svcomp25.json, the error message becomes

Fatal error: exception Invalid_argument("option is None")

Changing strcmp to non-special function or providing a body for main_real mitigates the issue. The issue occurred when trying to analyze libfuse examples.

[sim642]

The problem probably stems from how arguments are synthesized for the hello_read call which may be performed by main_real.
We might be just passing all supertop (VD.top ()) values, as opposed to top values based on the argument type.
One possibility would be to try to construct correctly-typed abstract values there, although that may be difficult for some reason.

Another possibility would be to just in this String function: not an address logic, interpret Top of ValueDomain as a top address (AD.top ()) instead.