diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-12 09:26:02 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-12 09:26:02 +0200 |
| commit | 41cac0e437d63399f46ac3c4b5c7ad2c23f88c5e (patch) | |
| tree | 2c01f5a7caa7e48d0b6256fed2f876f89a3dff33 /mppa_k1c/TargetPrinter.ml | |
| parent | 005093b87250b6b27b320eb789574da4bda616c0 (diff) | |
| parent | 28b4c273e3ec4d7022dd2994bfeed0a046c0727f (diff) | |
| download | compcert-kvx-41cac0e437d63399f46ac3c4b5c7ad2c23f88c5e.tar.gz compcert-kvx-41cac0e437d63399f46ac3c4b5c7ad2c23f88c5e.zip | |
Merge remote-tracking branch 'origin/mppa-work' into mppa-msub
Diffstat (limited to 'mppa_k1c/TargetPrinter.ml')
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 2d870c01..8a5a39cb 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -34,9 +34,22 @@ module Target (*: TARGET*) = let comment = "#" - let symbol = elf_symbol - let symbol_offset = elf_symbol_offset - let label = elf_label + let subst_symbol = function + "__compcert_i64_udiv" -> "__udivdi3" + | "__compcert_i64_sdiv" -> "__divdi3" + | "__compcert_i64_umod" -> "__umoddi3" + | "__compcert_i64_smod" -> "__moddi3" + | x -> x;; + + let symbol oc symb = + fprintf oc "%s" (subst_symbol (extern_atom symb)) + + let symbol_offset oc (symb, ofs) = + symbol oc symb; + let ofs = camlint64_of_ptrofs ofs in + if ofs <> 0L then fprintf oc " + %Ld" ofs + + let label = elf_label let print_label oc lbl = label oc (transl_label lbl) |