GCC -fanalyzer doesn't warn about leaks when returning from "main"; should it?

[davidmalcolm]

I see e.g.:
https://github.com/aufover/aufover-benchmark/blob/main/tests/single-c/mem-basic-malloc/0003-malloc-nonfreed/0003-test.c
that you have test cases for memory leaks where the leak happens when returning from "main".

GCC's -fanalyzer specialcases "main" here and deliberately doesn't warn about such leaks, since the process is about to exit. My feeling is that such warnings are likely to be treated as unhelpful by developers, but I suppose they might impact GCC's "score" in benchmarks. Is this OK, or should I implemented some kind of flag to warn anyway for such cases? Thanks!

[kdudka]

I would say that practically oriented tools should not warn about memory leaks on program exit. Benchmarks focused on static analyzers should take the fact into account. Such a flag could be useful if gcc -fanalyzer wanted to compete with formal verification tools. See the definition of G valid-memcleanup at https://sv-comp.sosy-lab.org/2023/rules.php