diff options
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 3c46ef16..15f05960 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -39,6 +39,8 @@ module Target (*: TARGET*) = | "__compcert_i64_sdiv" -> "__divdi3" | "__compcert_i64_umod" -> "__umoddi3" | "__compcert_i64_smod" -> "__moddi3" + | "__compcert_f64_div" -> "__divdf3" + | "__compcert_f32_div" -> "__divsf3" | x -> x;; let symbol oc symb = |