diff options
| author | Michael Schmidt <github@mschmidt.me> | 2016-05-13 13:11:50 +0200 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2016-05-13 13:11:50 +0200 |
| commit | 672393ef623acb3e230a8019d51c87e051a7567a (patch) | |
| tree | 946250aa400103241d267d3eb04f2a9905abfeb3 | |
| parent | 9864e348a4771b9d7f91fdcc9e4954f2d51ba201 (diff) | |
| download | compcert-kvx-672393ef623acb3e230a8019d51c87e051a7567a.tar.gz compcert-kvx-672393ef623acb3e230a8019d51c87e051a7567a.zip | |
bug 18925, fix loading of symbols for thumb: :lower16: and :upper16: are restricted to 15bit signed immediate offsets
| -rw-r--r-- | arm/TargetPrinter.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 4120b188..d2ea16f7 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -239,7 +239,8 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = (* Generate code to load the address of id + ofs in register r *) let loadsymbol oc r id ofs = - if !Clflags.option_mthumb then begin + let o = camlint_of_coqint ofs in + if o >= -32768l && o <= 32767l && !Clflags.option_mthumb then begin fprintf oc " movw %a, #:lower16:%a\n" ireg r symbol_offset (id, ofs); fprintf oc " movt %a, #:upper16:%a\n" |