sub-architectural options passed to preprocessor, assembler etc.

[monniaux]

Certain targets (ARM…) are are available as several sub-targets with different instruction sets. CompCert, when calling gcc as preprocessor, should pass the appropriate -march= option (*). Maybe there should be a configure option for setting that.

Of course one can always edit compcert.ini by hand.

(*) Because headers may test preprocessor flags for the availability of certain features, for instance accessible through inline assembly.