aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-10-16 13:06:09 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-10-16 13:06:09 +0200
commit24b4159b6a29328c529e0e59405e03ea192aa99e (patch)
tree4b39da911a2eb037e3c9fb3950d53bb0bd6a41b2 /driver
parent1e52bb2001964d87086cea00d0cb779e270b99ce (diff)
downloadcompcert-24b4159b6a29328c529e0e59405e03ea192aa99e.tar.gz
compcert-24b4159b6a29328c529e0e59405e03ea192aa99e.zip
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.
Diffstat (limited to 'driver')
-rw-r--r--driver/Clflags.ml1
-rw-r--r--driver/Driver.ml8
2 files changed, 8 insertions, 1 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 9d3697bd..b0c24f08 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -46,6 +46,7 @@ let option_dmach = ref false
let option_dasm = ref false
let option_sdump = ref false
let option_g = ref false
+let option_gdwarf = ref 2
let option_o = ref (None: string option)
let option_E = ref false
let option_S = ref false
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-<opt> to turn off -f<opt>) :
-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-<opt> to turn off -f<opt>)
-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);