diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-10-12 10:58:59 +0200 |
---|---|---|
committer | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-10-16 08:19:06 +0200 |
commit | ccf1983c3fe334fa82fa81ff7e3067e93b3d6c0c (patch) | |
tree | 9ba6409cddf963e63b91b4076e9881d09ac66ad0 | |
parent | 115825af0f765bf26270f9b9a2c550eddd76d7bd (diff) | |
download | compcert-ccf1983c3fe334fa82fa81ff7e3067e93b3d6c0c.tar.gz compcert-ccf1983c3fe334fa82fa81ff7e3067e93b3d6c0c.zip |
Do not generate object files for linking.
If CompCert is called to compile and link object files should not
be created.
Bug 22399
-rw-r--r-- | driver/Driver.ml | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 6996f537..4f27cb56 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -28,6 +28,9 @@ let sdump_folder = ref "" let jdump_magic_number = "CompCertJDUMP" ^ Version.version +let nolink () = + !option_c || !option_S || !option_E || !option_interp + let dump_jasm asm sourcename destfile = let oc = open_out_bin destfile in let pp = Format.formatter_of_out_channel oc in @@ -55,6 +58,11 @@ let dump_jasm asm sourcename destfile = Format.pp_print_flush pp (); close_out oc +let object_filename sourcename suff = + if nolink () then + output_filename ~final: !option_c sourcename suff ".o" + else + Filename.temp_file "compcert" ".o" (* From CompCert C AST to asm *) @@ -132,7 +140,7 @@ let process_c_file sourcename = compile_c_file sourcename preproname asmname; if not !option_dprepro then safe_remove preproname; - let objname = output_filename ~final: !option_c sourcename ".c" ".o" in + let objname = object_filename sourcename ".c" in assemble asmname objname; if not !option_dasm then safe_remove asmname; objname @@ -158,7 +166,7 @@ let process_i_file sourcename = then output_filename sourcename ".c" ".s" else Filename.temp_file "compcert" ".s" in compile_c_file sourcename sourcename asmname; - let objname = output_filename ~final: !option_c sourcename ".c" ".o" in + let objname = object_filename sourcename ".c" in assemble asmname objname; if not !option_dasm then safe_remove asmname; objname @@ -169,7 +177,7 @@ let process_i_file sourcename = let process_s_file sourcename = ensure_inputfile_exists sourcename; - let objname = output_filename ~final: !option_c sourcename ".s" ".o" in + let objname = object_filename sourcename ".s" in assemble sourcename objname; objname @@ -181,7 +189,7 @@ let process_S_file sourcename = end else begin let preproname = Filename.temp_file "compcert" ".s" in preprocess sourcename preproname; - let objname = output_filename ~final: !option_c sourcename ".S" ".o" in + let objname = object_filename sourcename ".S" in assemble preproname objname; safe_remove preproname; objname @@ -508,8 +516,7 @@ let _ = CPragmas.initialize(); parse_cmdline cmdline_actions; DebugInit.init (); (* Initialize the debug functions *) - let nolink = !option_c || !option_S || !option_E || !option_interp in - if nolink && !option_o <> None && !num_source_files >= 2 then begin + if nolink () && !option_o <> None && !num_source_files >= 2 then begin eprintf "Ambiguous '-o' option (multiple source files)\n"; exit 2 end; @@ -519,7 +526,7 @@ let _ = exit 2 end; let linker_args = time "Total compilation time" perform_actions () in - if (not nolink) && linker_args <> [] then begin + if not (nolink ()) && linker_args <> [] then begin linker (output_filename_default "a.out") linker_args end; if Cerrors.check_errors () then exit 2 |