diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-12 00:42:04 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-12 00:42:04 +0200 |
| commit | 6e995893ccae975f49c250387182fcd3e3e6395a (patch) | |
| tree | 30a38957a31313a071bba8e903a1890cc8dd7b98 /mppa_k1c | |
| parent | 212b467687f0e3c0e3897b501cdc9e09a0d99233 (diff) | |
| download | compcert-kvx-6e995893ccae975f49c250387182fcd3e3e6395a.tar.gz compcert-kvx-6e995893ccae975f49c250387182fcd3e3e6395a.zip | |
directly branch to certain division functions from gcc
Diffstat (limited to 'mppa_k1c')
| -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 114297c9..3c46ef16 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) |