aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/TargetPrinter.ml
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c/TargetPrinter.ml')
-rw-r--r--mppa_k1c/TargetPrinter.ml10
1 files changed, 8 insertions, 2 deletions
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 4dc4b7c2..2bdd0978 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -39,8 +39,14 @@ module Target (*: TARGET*) =
| Idiv_stsud
| Idiv_fp;;
- let idiv_function_kind_32bit () = Idiv_fp;;
- let idiv_function_kind_64bit () = Idiv_stsud;;
+ let idiv_function_kind = function
+ "stsud" -> Idiv_stsud
+ | "system" -> Idiv_system
+ | "fp" -> Idiv_fp
+ | _ -> failwith "unknown integer division kind";;
+
+ let idiv_function_kind_32bit () = idiv_function_kind !Clflags.option_div_i32;;
+ let idiv_function_kind_64bit () = idiv_function_kind !Clflags.option_div_i64;;
let subst_symbol = function
"__compcert_i64_udiv" ->