aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bschommer@users.noreply.github.com>2018-01-05 12:54:53 +0100
committerGitHub <noreply@github.com>2018-01-05 12:54:53 +0100
commit91601d4bd435efdee12e08188573f0e9bd910a8a (patch)
tree1383b0a2804a5719a2829063e8917d0f03f7a6bb
parent9ccb6a24541b3a06b600a70791950eecd46d1806 (diff)
downloadcompcert-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
-rw-r--r--driver/Driver.ml17
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 *)