diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-06-28 17:04:56 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-06-28 17:04:56 +0200 |
| commit | 711cea9fc37e777487abc815730aacde2b00aef3 (patch) | |
| tree | f9480756132b098cb42d9853a5a188fdb156c697 /driver | |
| parent | 56a6795d82c5ff0af78872a3e807b48c556ce5fe (diff) | |
| download | compcert-kvx-711cea9fc37e777487abc815730aacde2b00aef3.tar.gz compcert-kvx-711cea9fc37e777487abc815730aacde2b00aef3.zip | |
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
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Configuration.ml | 8 | ||||
| -rw-r--r-- | driver/Configuration.mli | 3 | ||||
| -rw-r--r-- | driver/Optionsprinter.ml | 1 |
3 files changed, 1 insertions, 11 deletions
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}" |