diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-13 11:28:03 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-13 11:28:03 +0200 |
| commit | b1b7a68222ada09b8dfaf9a5dbe2306b5fc44684 (patch) | |
| tree | 8b7941d00009dde811cf3ba3a84510ff6a2ef819 | |
| parent | f1e22ac1ba0e78455cc25bac0f901effc764bc5a (diff) | |
| parent | 28b4c273e3ec4d7022dd2994bfeed0a046c0727f (diff) | |
| download | compcert-kvx-b1b7a68222ada09b8dfaf9a5dbe2306b5fc44684.tar.gz compcert-kvx-b1b7a68222ada09b8dfaf9a5dbe2306b5fc44684.zip | |
Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| -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) |