Add support for -MD

[didickman]

Most of the -M options are supported by CompCert but -MD is one that shows up often in build systems I use and seems to be missing from CompCert. It would be nice to have support for -MD as well.

[xavierleroy]

Right, it looks like we missed the -MD and -MMD options of GCC and Clang, while we support the other -M options. I'll add the missing options.

[xavierleroy]

Implemented in 76f7fea.

The GCC info page says:

     If ‘-MD’ is used in conjunction with ‘-E’, any ‘-o’ switch is
     understood to specify the dependency output file,
     but if used without ‘-E’, each ‘-o’ is understood to
     specify a target object file.

This behavior is not implemented in CompCert: ccomp -MD -E -o foo.deps foo.c outputs the dependencies to foo.d and the preprocessed code to foo.deps.

However, this behavior is not implemented in GCC 13 nor in Clang 18 either: they produce the dependencies in foo.d regardless of the -E -o options. So, CompCert is consistent with GCC and Clang.

The -MF foo.deps option (output the dependencies to foo.deps) was already honored by CompCert.