Activate advanced debug information for arm, ia32.

The configuration advanced debug is removed and now full debug
information is also generated for ia32 and arm.
Bug 17609

7 files changed, 5 insertions, 20 deletions

diff --git a/Makefile b/Makefile
index 66fa90f6..73c13eeb 100644
--- a/Makefile
+++ b/Makefile
@@ -206,7 +206,6 @@ compcert.ini: Makefile.config
          echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \
          echo "has_standard_headers=$(HAS_STANDARD_HEADERS)"; \
          echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \
-         echo "advanced_debug=$(ADVANCED_DEBUG)"; \
          echo "struct_passing_style=$(STRUCT_PASSING)"; \
          echo "struct_return_style=$(STRUCT_RETURN)";) \
         > compcert.ini
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 96aa080e..8e43a050 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -30,7 +30,7 @@ module Printer(Target:TARGET) =
       s,e
 
     let print_debug_label oc l =
-      if !Clflags.option_g && Configuration.advanced_debug then
+      if !Clflags.option_g then
         fprintf oc "%a:\n" Target.label l
       else
         ()
@@ -49,7 +49,7 @@ module Printer(Target:TARGET) =
       if not (C2C.atom_is_static name) then
         fprintf oc "	.globl %a\n" Target.symbol name;
       Target.print_optional_fun_info oc;
-      let s,e = if !Clflags.option_g && Configuration.advanced_debug then
+      let s,e = if !Clflags.option_g then
         get_fun_addr name text
       else
         -1,-1 in
@@ -126,7 +126,7 @@ let print_program oc p =
   Target.print_prologue oc;
   List.iter (Printer.print_globdef oc) p.prog_defs;
   Target.print_epilogue oc;
-  if !Clflags.option_g && Configuration.advanced_debug then
+  if !Clflags.option_g then
     begin
       let atom_to_s s =
         let s = C2C.atom_sections s in
diff --git a/configure b/configure
index 2dc60d28..05e8c6f2 100755
--- a/configure
+++ b/configure
@@ -19,7 +19,6 @@ toolprefix=''
 target=''
 has_runtime_lib=true
 has_standard_headers=true
-advanced_debug=false
 clightgen=false
 
 usage='Usage: ./configure [options] target
@@ -119,7 +118,6 @@ case "$target" in
         asm_supports_cfi=false
         clinker="${toolprefix}dcc"
         libmath="-lm"
-        advanced_debug=true;;
       *)
         system="linux"
         cc="${toolprefix}gcc"
@@ -130,7 +128,6 @@ case "$target" in
         casmruntime="${toolprefix}gcc -c -Wa,-mregnames"
         clinker="${toolprefix}gcc"
         libmath="-lm"
-        advanced_debug=true;;
     esac;;
   arm*-*)
     arch="arm"
@@ -387,7 +384,6 @@ LIBMATH=$libmath
 HAS_RUNTIME_LIB=$has_runtime_lib
 HAS_STANDARD_HEADERS=$has_standard_headers
 ASM_SUPPORTS_CFI=$asm_supports_cfi
-ADVANCED_DEBUG=$advanced_debug
 CLIGHTGEN=$clightgen
 EOF
 else
diff --git a/debug/DebugInit.ml b/debug/DebugInit.ml
index 462ca2d3..b3fedb00 100644
--- a/debug/DebugInit.ml
+++ b/debug/DebugInit.ml
@@ -60,7 +60,7 @@ let init_none () =
   implem := default_implem
 
 let init () =
-  if !Clflags.option_g && Configuration.advanced_debug then
+  if !Clflags.option_g then
     init_debug ()
   else
     init_none ()
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 1914c1b3..e1a02573 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -108,7 +108,7 @@ let opt_config_list key =
   | Some v -> v
   | None -> []
 
-let prepro = 
+let prepro =
   tool_absolute_path (get_config_list "prepro")@(opt_config_list "prepro_options")
 let asm =
   tool_absolute_path (get_config_list "asm")@(opt_config_list "asm_options")
@@ -144,12 +144,6 @@ let asm_supports_cfi =
   | "false" -> false
   | v -> bad_config "asm_supports_cfi" [v]
 
-let advanced_debug =
-  match get_config_string "advanced_debug" with
-  | "true" -> true
-  | "false" -> false
-  | v -> bad_config "advanced_debug" [v]
-
 
 type struct_passing_style =
   | SP_ref_callee                       (* by reference, callee takes copy *)
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index abfd3ab4..dde9d6fd 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -43,9 +43,6 @@ val has_runtime_lib: bool
 val has_standard_headers: bool
   (** True if CompCert's standard header files is available. *)
 
-val advanced_debug: bool
-  (** True if advanced debug is implement for the Target *)
-
 
 type struct_passing_style =
   | SP_ref_callee                       (* by reference, callee takes copy *)
diff --git a/driver/Optionsprinter.ml b/driver/Optionsprinter.ml
index f046b40a..9dce8592 100644
--- a/driver/Optionsprinter.ml
+++ b/driver/Optionsprinter.ml
@@ -91,7 +91,6 @@ let print_configurations oc lib_path =
   p_jmember oc "stdlib_path" p_jstring lib_path;
   p_jmember oc "has_runtime_lib" p_jbool Configuration.has_runtime_lib;
   p_jmember oc "has_standard_headers" p_jbool Configuration.has_standard_headers;
-  p_jmember oc "advanced_debug" p_jbool Configuration.advanced_debug;
   p_jmember oc "struct_passing_style" print_struct_passing_style Configuration.struct_passing_style;
   p_jmember oc "struct_return_style" print_struct_return_style Configuration.struct_return_style;
   fprintf oc "\n}"