aboutsummaryrefslogtreecommitdiffstats
path: root/debug
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2016-11-25 11:06:15 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2016-11-25 11:06:15 +0100
commite8f2ef5c8c926462277afb520cacaa265b7e612c (patch)
tree7c3b552108da1d8fb3ae867e0076ab91663e7fa9 /debug
parent9521c220e157632972387ad0394010e89eff0aab (diff)
downloadcompcert-kvx-e8f2ef5c8c926462277afb520cacaa265b7e612c.tar.gz
compcert-kvx-e8f2ef5c8c926462277afb520cacaa265b7e612c.zip
Do not use hardcoded register number for sp.
Since the dwarf register names for x86_32 and x86_64 differ it is wrong to hardcode the dwarf register number for rsp to 4. Bug 20461
Diffstat (limited to 'debug')
-rw-r--r--debug/DwarfPrinter.ml20
1 files changed, 10 insertions, 10 deletions
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml
index 43505e12..1d336965 100644
--- a/debug/DwarfPrinter.ml
+++ b/debug/DwarfPrinter.ml
@@ -337,21 +337,21 @@ module DwarfPrinter(Target: DWARF_TARGET):
let print_loc_expr oc = function
| DW_OP_bregx (a,b) ->
- print_byte oc "" dw_op_bregx;
- print_uleb128 oc "" a;
- fprintf oc " .sleb128 %ld\n" b;
+ print_byte oc "DW_OP_bregx" dw_op_bregx;
+ print_uleb128 oc "Register number" a;
+ print_sleb128 oc "Offset" (Int32.to_int b);
| DW_OP_plus_uconst i ->
- print_byte oc "" dw_op_plus_uconst;
- print_uleb128 oc "" i
+ print_byte oc "DW_OP_plus_uconst" dw_op_plus_uconst;
+ print_uleb128 oc "Constant" i
| DW_OP_piece i ->
- print_byte oc "" dw_op_piece;
- print_uleb128 oc "" i
+ print_byte oc "DW_op_piece" dw_op_piece;
+ print_uleb128 oc "Piece" i
| DW_OP_reg i ->
if i < 32 then
- print_byte oc "" (dw_op_reg0 + i)
+ print_byte oc "DW_op_reg" (dw_op_reg0 + i)
else begin
- print_byte oc "" dw_op_regx;
- print_uleb128 oc "" i
+ print_byte oc "DW_op_regx" dw_op_regx;
+ print_uleb128 oc "Register number" i
end
let print_loc oc c loc =