Analysis coverage reports

[sim642]

In larger programs and real-world projects it's often difficult to know whether a certain part of code was actually analyzed or not. Dead code warnings provide only partial information because the lack of them does not ensure live code. When some code happens to be disabled by preprocessing or missing from input files (either manually listed or from compilation database), Goblint will never even see it and thus not output dead code warnings about it either.

A possibly more convenient way would be to generate code coverage reports based on analyzed lines in some standard code coverage formats. These could be viewed using existing IDE extensions along with the actual source code to quickly get an overview.

[michael-schwarz]

@sim642: I see you added the unsound tag here. In what sense is the analysis unsound here?

[sim642]

It's not an unsoundness bug but an usability feature regarding unsoundness.

[michael-schwarz]

I added a new tag for it, as I quite often show the list of issues tagged with unsound to demonstrate that where we still fall short of being sound, and this issue would make that list longer.