[OT] Identifying unused include directives?

[Richard Kenner]

    I think the definition of unneeded is pretty clear. A reasonable definition
    would be that the removal of the #include would not affect the semantics
    of the resulting program. As I pointed out before, this is recursively
    undecidable in the general case.

A way to avoid the undecidability, and that seems to be closer to what most
programmers would view as the intuitive meaning, would be that the removal of
the #include would not cause compilation errors or change the generated code.
Normally we think of #include as being part of the *static* semantics.