Thank you for the PR!

In the above example, p's memory is leaked (missing free), but it's also reported as unreachable (because it's not reachable via the globals, but only via a local var). Should we try to improve on that (maybe at least in the error reporting for the unreachable-from-globals-memory case) or are we ok with it as is?

Confusingly this is exactly the definition of valid-memtrack in SV-COMP (I was also surprised by this). See e.g.: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1464
So we cannot really improve here and actually need to report this as a violation of valid-memtrack.

I will start a run with the two suggestions from above applied to see what the results are.

With these two suggestions on top of #1234, we succeed on an additional 17 tasks:

Statistics:           3862 Files
  correct:            1175
    correct true:     1175
    correct false:       0
  incorrect:             0
    incorrect true:      0
    incorrect false:     0
  unknown:            2687
  Score:              2350 (max: 5857)

Tables: results.2023-11-08_10-02-03.zip

Confusingly this is exactly the definition of valid-memtrack in SV-COMP (I was also surprised by this). See e.g.: https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1464
So we cannot really improve here and actually need to report this as a violation of valid-memtrack.

I see, thanks for the clarification! It's a bit confusing, indeed. In this case I'll leave the reporting of this violation as is.

I added some changes regarding the check of whether some memory is still transitively reachable via the points-to set of a global struct variable (both of pointer and non-pointer type), as well as its fields and the contents of the points-to sets.

I also added two new regression test cases to check if the changes make sense (cf. 76/{13, 14}).

Maybe we should add a check that if earlyglobs is activated, then we should abort the analysis?

Iirc, we discussed with @jerhard that earlyglobs would stop us from obtaining meaningful information about what global vars can reference.

Maybe we should add a check that if earlyglobs is activated, then we should abort the analysis?

I don't think we use earlyglobs in sv-comp, so this doesn't seem too pressing.

I may have missed this, but in what sense are global structs special? As in, why aren't we also considering the contents of global arrays and whatnot?
Or are we just less precise for global array contents then?

I may have missed this, but in what sense are global structs special? As in, why aren't we also considering the contents of global arrays and whatnot?
Or are we just less precise for global array contents then?

I'm not really sure about arrays, because I haven't worked a lot with the array domain of Goblint and so I can't express an opinion on that.

I've thought about global unions, however I'm unsure about what should happen in a situation like the following. Consider:

typedef union {
    int i;
    char *str;
} un;

un *glob_var;

int main() {
    ...
}

What happens if the program first accesses str of glob_var and then subsequently accesses i of glob_var? Wouldn't str be "lost" so to speak? I mean the memory is there, but i is the thing that's now occupying the place of str, unless I'm thinking in the wrong direction.

Yeah, unions do not seem to be a good candidate here. We discussed the issue of arrays at our Gobcon yesterday, and decided that due to the abstraction we use for arrays, it is unlikely that things are must-reachable from arrays and have thus decided against implementing dedicated support for it for now.

We then need to explicitly limit the filtering to structs though. CIL's TComp represents both structs and unions.

I think we can now merge this into master as well? Wdyt @sim642?