aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/TargetPrinter.ml
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-09-23 16:49:13 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2015-09-23 16:49:13 +0200
commitb448fbba97c1008599610d0c9bc834881b9dc219 (patch)
treef244430d915c0818c8ae66c1235316fdac1d683d /powerpc/TargetPrinter.ml
parent806102dd5492a39b33c2ebb88d6646237ba7f9e6 (diff)
downloadcompcert-b448fbba97c1008599610d0c9bc834881b9dc219.tar.gz
compcert-b448fbba97c1008599610d0c9bc834881b9dc219.zip
Added support for printing local variables and fixed issue with .text
Local variables are now added with bogus lexical scopes to reflect the actually lexical scopes. Also this commit fixes assembler problems of the das when a user section with the name ".text" is defined.
Diffstat (limited to 'powerpc/TargetPrinter.ml')
-rw-r--r--powerpc/TargetPrinter.ml9
1 files changed, 6 insertions, 3 deletions
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 2faaf2e3..21181215 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -269,8 +269,11 @@ module Diab_System : SYSTEM =
fprintf oc ".L%d: .d2filenum \"%s\"\n" label file);
fprintf oc " .d2_line_end\n";
StringSet.iter (fun s ->
- fprintf oc " %s\n" s;
- fprintf oc " .d2_line_end\n") !additional_debug_sections
+ if s <> (name_of_section Section_text) then
+ begin
+ fprintf oc " %s\n" s;
+ fprintf oc " .d2_line_end\n"
+ end) !additional_debug_sections
end
let print_file_loc oc (file,col) =
@@ -282,7 +285,7 @@ module Diab_System : SYSTEM =
match sec with
| Section_user (name,_,_) ->
let sec_name = name_of_section sec in
- if not (StringSet.mem sec_name !additional_debug_sections) then
+ if not (StringSet.mem sec_name !additional_debug_sections) && name <> ".text" then
begin
let name = ".debug_line"^name in
additional_debug_sections := StringSet.add sec_name !additional_debug_sections;