I implemented the dependencies Makefile approach. With -MMD as an additional argument to the preprocessor, it creates a .d file on the side in Makefile format, listing all the included (non-system) dependencies of the preprocessed file in the same go. This is then parsed in Goblint and added to the json-messages output in the following way:

  "files": {
    "/home/simmo/Desktop/goblint-action-test/cmake-project/main.c": [
      "/home/simmo/dev/goblint/sv-comp/goblint/_opam/share/goblint/includes/assert.h",
      "/home/simmo/Desktop/goblint-action-test/cmake-project/lib/lib.h"
    ],
    "/home/simmo/dev/goblint/sv-comp/goblint/_opam/share/goblint/includes/stdlib.c":
      [],
    "/home/simmo/Desktop/goblint-action-test/cmake-project/lib/lib.c": [
      "/home/simmo/Desktop/goblint-action-test/cmake-project/lib/lib.h"
    ]
  },

Doing it in CIL might be a bit more general if we want to analyze already preprocessed programs that contain those line pragmas, because this wouldn't know about those. Although I don't think we should bother because we cannot reasonably handle such programs with GobPie etc anyway: the warning locations would be in possibly nonexistent physical files that were included, not in the physical file that was actually analyzed, so all the output would be a mess anyway.

Looks good!

Would this information also be sufficient to make the pre-processing (and potentially parsing into CIL files) incremental, in that if no input files have changed, no new run of cpp or no new computation of a CIl file is neccessary?

In order to guarantee this, transitive dependencies would probably have to be considered as well...

Would this information also be sufficient to make the pre-processing (and potentially parsing into CIL files) incremental, in that if no input files have changed, no new run of cpp or no new computation of a CIl file is neccessary?

I think it should be. The use case in GobPie is somewhat related.

In order to guarantee this, transitive dependencies would probably have to be considered as well...

This should cover all includes transitively, because they're inlined transitively during preprocessing, so the corresponding indirect dependency should be direct in this output.

Due to some MagpieBridge oddities this information cannot be used to its true extent in GobPie for the time being. But I'm merging it anyway since it might become useful.