From e8127be72ffc16f91de51c0b8dca3df0d3bd4745 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 6 Oct 2015 12:37:31 +0200 Subject: Push the linker args separate. --- driver/Driver.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 9b1a6e70..c7d9984e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -572,8 +572,10 @@ let cmdline_actions = Prefix "-L", Self push_linker_arg; Exact "-T", String (fun s -> if Configuration.system = "diab" then push_linker_arg ("-Wm"^s) - else - push_linker_arg ("-T "^s)); + else begin + push_linker_arg ("-T"); + push_linker_arg(s) + end); Prefix "-Wl,", Self push_linker_arg; (* Tracing options *) Exact "-dparse", Set option_dparse; -- cgit From 60ab550a952c3d9719b2a91ec90c9b58769f6717 Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:07:48 +0200 Subject: bug 17392: remove trailing whitespace in source files --- driver/Driver.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index c7d9984e..4b58fb4d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -188,7 +188,7 @@ let compile_c_ast sourcename csyntax ofile debug = | Errors.Error msg -> eprintf "%s: %a" sourcename print_error msg; exit 2 in - (* Dump Asm in binary and JSON format *) + (* Dump Asm in binary and JSON format *) if !option_sdump then begin dump_asm asm (output_filename sourcename ".c" ".sdump"); @@ -518,7 +518,7 @@ let unset_all opts = List.iter (fun r -> r := false) opts let num_source_files = ref 0 let num_input_files = ref 0 - + let cmdline_actions = let f_opt name ref = [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in @@ -570,8 +570,8 @@ let cmdline_actions = (* Linking options *) Prefix "-l", Self push_linker_arg; Prefix "-L", Self push_linker_arg; - Exact "-T", String (fun s -> if Configuration.system = "diab" then - push_linker_arg ("-Wm"^s) + Exact "-T", String (fun s -> if Configuration.system = "diab" then + push_linker_arg ("-Wm"^s) else begin push_linker_arg ("-T"); push_linker_arg(s) -- cgit From 24b4159b6a29328c529e0e59405e03ea192aa99e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Oct 2015 13:06:09 +0200 Subject: Implemented the usage of DW_AT_ranges for non-contiguous address ranges. The gcc produces DW_AT_ranges for non-contiguous address ranges, like compilation units containing functions which are placed in different ELF-sections or lexical scopes that are split up. With this commit CompCert also uses this DWARF v3 feature for gnu backend based targets. In order to ensure backward compability a flag is added which avoids this and produces debug info in DWARF v2 format. Bug 17392. --- driver/Driver.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 4b58fb4d..7459e030 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -444,6 +444,7 @@ Language support options (use -fno- to turn off -f) : -fnone Turn off all language support options above Debugging options: -g Generate debugging information + -gdwarf- (GCC only) Generate debug information in DWARF v2 or DWARF v3 -frename-static Rename static functions and declarations Optimization options: (use -fno- to turn off -f) -O Optimize the compiled code [on by default] @@ -549,7 +550,12 @@ let cmdline_actions = Exact "-fall", Self (fun _ -> set_all language_support_options); Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) - Exact "-g", Self (fun s -> option_g := true); + Exact "-g", Self (fun s -> option_g := true; + option_gdwarf := 3); + Exact "-gdwarf-2", Self (fun s -> option_g:=true; + option_gdwarf := 2); + Exact "-gdwarf-3", Self (fun s -> option_g := true; + option_gdwarf := 3); Exact "-frename-static", Self (fun s -> option_rename_static:= true); (* Code generation options -- more below *) Exact "-O0", Self (fun _ -> unset_all optimization_options); -- cgit From 8a95c3e07fd02eaa87f8cca447bc7d7c2642eb22 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 16 Oct 2015 15:19:24 +0200 Subject: Do not dump the .sdump files. Bug 16529. --- driver/Driver.ml | 17 ++--------------- 1 file changed, 2 insertions(+), 15 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index 7459e030..8fe6b07d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -144,17 +144,7 @@ let parse_c_file sourcename ifile = end; csyntax,None -(* Dump Asm code in binary format for the validator *) - -let sdump_magic_number = "CompCertSDUMP" ^ Version.version - -let dump_asm asm destfile = - let oc = open_out_bin destfile in - output_string oc sdump_magic_number; - output_value oc asm; - output_value oc Camlcoq.string_of_atom; - output_value oc C2C.decl_atom; - close_out oc +(* Dump Asm code in asm format for the validator *) let jdump_magic_number = "CompCertJDUMP" ^ Version.version @@ -190,10 +180,7 @@ let compile_c_ast sourcename csyntax ofile debug = exit 2 in (* Dump Asm in binary and JSON format *) if !option_sdump then - begin - dump_asm asm (output_filename sourcename ".c" ".sdump"); - dump_jasm asm (output_filename sourcename ".c" ".json") - end; + dump_jasm asm (output_filename sourcename ".c" ".json"); (* Print Asm in text form *) let oc = open_out ofile in PrintAsm.print_program oc asm debug; -- cgit