diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2018-01-05 12:54:53 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-01-05 12:54:53 +0100 |
commit | 91601d4bd435efdee12e08188573f0e9bd910a8a (patch) | |
tree | 1383b0a2804a5719a2829063e8917d0f03f7a6bb /driver | |
parent | 9ccb6a24541b3a06b600a70791950eecd46d1806 (diff) | |
download | compcert-91601d4bd435efdee12e08188573f0e9bd910a8a.tar.gz compcert-91601d4bd435efdee12e08188573f0e9bd910a8a.zip |
Added toolchain specific option for dcc. (#47)
CompCert now accepts the target configuration option of the diab
data compiler and passes it on to the preprocessor, assembler and
linker.
Bug 20521
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Driver.ml | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index b23a4e4f..9726f107 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -201,6 +201,13 @@ let target_help = else "" +let toolchain_help = + if not Configuration.gnu_toolchain then begin +{|Toolchain options: + -t tof:env Select target processor for the diab toolchain +|} end else + "" + let usage_string = version_string ^ {|Usage: ccomp [options] <source files> @@ -255,6 +262,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) -falign-cond-branches <n> Set alignment (in bytes) of conditional branches |} ^ target_help ^ + toolchain_help ^ assembler_help ^ linker_help ^ {|Tracing options: @@ -377,7 +385,14 @@ let cmdline_actions = else [ Exact "-mthumb", Set option_mthumb; Exact "-marm", Unset option_mthumb; ] - else []) @ + else []) @ +(* Toolchain options *) + (if not Configuration.gnu_toolchain then + [Exact "-t", String (fun arg -> push_linker_arg "-t"; push_linker_arg arg; + prepro_options := arg :: "-t" :: !prepro_options; + assembler_options := arg :: "-t" :: !assembler_options;)] + else + []) @ (* Assembling options *) assembler_actions @ (* Linking options *) |