diff options
| author | Michael Schmidt <github@mschmidt.me> | 2017-12-15 12:20:49 +0100 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2017-12-15 12:20:49 +0100 |
| commit | 9b98d49bbc105d998f9a63868d4b23bfab8d4cf7 (patch) | |
| tree | b024ffd96b52efd56b77008521a82a6c87c64698 /arm/TargetPrinter.ml | |
| parent | 73ab7968d862c4d4d883fb3d3215353eba905b0f (diff) | |
| download | compcert-kvx-9b98d49bbc105d998f9a63868d4b23bfab8d4cf7.tar.gz compcert-kvx-9b98d49bbc105d998f9a63868d4b23bfab8d4cf7.zip | |
Reintroduce informative comment for Ploadsymbol_lbl in target printer
Diffstat (limited to 'arm/TargetPrinter.ml')
| -rw-r--r-- | arm/TargetPrinter.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index bb7f24df..d402b4a8 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -515,8 +515,8 @@ struct fprintf oc " vmov.f32 %a, #%.15F\n" freg_single r1 (Int32.float_of_bits f) | Ploadsymbol_lbl (r1,lbl,id,ofs) -> - fprintf oc " ldr %a, %a\n" - ireg r1 print_label lbl + fprintf oc " ldr %a, %a %s %a\n" + ireg r1 print_label lbl comment symbol_offset (id, ofs) let get_section_names name = |