diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-06-24 13:57:27 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-06-24 13:57:27 +0200 |
commit | 410a5db3d48e84f2157c2c4f4bc29056c0e174b9 (patch) | |
tree | 800974ebbe73921f27c0c563e56eb0c899efd7f5 /driver/Driveraux.ml | |
parent | 01354123b9df5d3cbb9d43298eea94ddda30acdf (diff) | |
download | compcert-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/Driveraux.ml')
-rw-r--r-- | driver/Driveraux.ml | 25 |
1 files changed, 17 insertions, 8 deletions
diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml index b5d155d4..3fe22fac 100644 --- a/driver/Driveraux.ml +++ b/driver/Driveraux.ml @@ -94,17 +94,26 @@ let print_error oc msg = List.iter print_one_error msg; output_char oc '\n' -let gnu_option s = - if Configuration.system <> "diab" then - true - else begin - eprintf "ccomp: warning: option %s only supported for gcc backend\n" s; - false - end - +let gnu_system = Configuration.system <> "diab" (* Command-line parsing *) let explode_comma_option s = match Str.split (Str.regexp ",") s with | [] -> assert false | _ :: tl -> tl + +(* Record actions to be performed after parsing the command line *) + +let actions : ((string -> string) * string) list ref = ref [] + +let push_action fn arg = + actions := (fn, arg) :: !actions + +let push_linker_arg arg = + push_action (fun s -> s) arg + +let perform_actions () = + let rec perform = function + | [] -> [] + | (fn, arg) :: rem -> let res = fn arg in res :: perform rem + in perform (List.rev !actions) |