aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Linker.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-06-24 13:57:27 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2016-06-24 13:57:27 +0200
commit410a5db3d48e84f2157c2c4f4bc29056c0e174b9 (patch)
tree800974ebbe73921f27c0c563e56eb0c899efd7f5 /driver/Linker.ml
parent01354123b9df5d3cbb9d43298eea94ddda30acdf (diff)
downloadcompcert-kvx-410a5db3d48e84f2157c2c4f4bc29056c0e174b9.tar.gz
compcert-kvx-410a5db3d48e84f2157c2c4f4bc29056c0e174b9.zip
Moved assembler and linker into own files.
The function to call the assembler and the linker are now in own files like the preprocessor. Bug 19197
Diffstat (limited to 'driver/Linker.ml')
-rw-r--r--driver/Linker.ml81
1 files changed, 81 insertions, 0 deletions
diff --git a/driver/Linker.ml b/driver/Linker.ml
new file mode 100644
index 00000000..501a2ae3
--- /dev/null
+++ b/driver/Linker.ml
@@ -0,0 +1,81 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+open Clflags
+open Commandline
+open Driveraux
+
+
+(* Linking *)
+
+let linker exe_name files =
+ let cmd = List.concat [
+ Configuration.linker;
+ ["-o"; exe_name];
+ files;
+ (if Configuration.has_runtime_lib
+ then ["-L" ^ !stdlib_path; "-lcompcert"]
+ else [])
+ ] in
+ let exc = command cmd in
+ if exc <> 0 then begin
+ command_error "linker" exc;
+ exit 2
+ end
+
+
+let gnu_linker_help =
+" -nostartfiles Do not use the standard system startup files when\n\
+\ linking\n\
+\ -nodefaultlibs Do not use the standard system libraries when\n\
+\ linking\n\
+\ -nostdlib Do not use the standard system startup files or\n\
+\ libraries when linking\n"
+
+let linker_help =
+"Linking options:\n\
+\ -l<lib> Link library <lib>\n\
+\ -L<dir> Add <dir> to search path for libraries\n" ^
+ (if gnu_system then gnu_linker_help else "") ^
+" -s Remove all symbol table and relocation information from the\n\
+\ executable\n\
+\ -static Prevent linking with the shared libraries\n\
+\ -T <file> Use <file> as linker command file\n\
+\ -Wl,<opt> Pass option <opt> to the linker\n\
+\ -WUl,<opt> Pass option <opt> to the gcc or dcc used for linking\n\
+\ -Xlinker <opt> Pass <opt> as an option to the linker\n\
+\ -u <symb> Pretend the symbol <symb> is undefined to force linking of\n\
+\ library modules to define it.\n"
+
+let linker_actions =
+ [ Prefix "-l", Self push_linker_arg;
+ Prefix "-L", Self push_linker_arg; ] @
+ if gnu_system then
+ [ Exact "-nostartfiles", Self push_linker_arg;
+ Exact "-nodefaultlibs", Self push_linker_arg;
+ Exact "-nostdlib", Self push_linker_arg;]
+ else [] @
+ [ Exact "-s", Self push_linker_arg;
+ Exact "-static", Self push_linker_arg;
+ Exact "-T", String (fun s -> if gnu_system then begin
+ push_linker_arg ("-T");
+ push_linker_arg(s)
+ end else
+ push_linker_arg ("-Wm"^s));
+ Exact "-Xlinker", String (fun s -> if Configuration.system = "diab" then
+ push_linker_arg ("-Wl,"^s)
+ else
+ push_linker_arg s);
+ Prefix "-Wl,", Self push_linker_arg;
+ Prefix "-WUl,", Self (fun s -> List.iter push_linker_arg (explode_comma_option s));
+ Exact "-u", Self push_linker_arg;]