Add support for the detection of `CWE-562`

[mrstanb]

CWE-562 is concerned with the issue of returning an address of a stack variable.

Here's a minimal example of a program that has a CWE-562 weakness:

char *cwe562() {
  char *str;
  return str;
}

I'm not sure if there are any SV-COMP Memory Safety cases for this CWE number (most likely not, at least from what I recall). Nonetheless, I think it'd be useful to have a detection mechanism in Goblint for this type of weakness. In addition, it could potentially be even brought into SV-COMP's Memory Safety category if it'd make sense.

I'll make sure to open a separate PR for this soon.

[sim642]

In terms of SV-COMP, I think the act of returning such address wouldn't be considered a violation, but if it is then dereferenced, it would be an invalid dereference.

[mrstanb]

In terms of SV-COMP, I think the act of returning such address wouldn't be considered a violation, but if it is then dereferenced, it would be an invalid dereference.

Yes, absolutely. I think in relation to this, we could try to flag such returned memory in some way, so that whenever it's used we could directly flag the use as an invalid one. (Although, thinking about it, we might not need an extra flag, because we could just check if the memory has an address that is not pointing to something local or global and be done with it)

[mrstanb]

Yes, absolutely. I think in relation to this, we could try to flag such returned memory in some way, so that whenever it's used we could directly flag the use as an invalid one. (Although, thinking about it, we might not need an extra flag, because we could just check if the memory has an address that is not pointing to something local or global and be done with it)

We already have a check for such invalid dereferences which was implemented back during my thesis. So even in terms of SV-COMP, we should be safe here.

[jerhard]

Following a dicussion at Gobcon, I closed the PR #1256. We might look again at implementing this when having a look at the escaping of variables, for this see https://github.com/goblint/analyzer/issues/1544, https://github.com/goblint/analyzer/issues/1491.