diff options
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 80eb641c..19712d2f 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -69,6 +69,8 @@ Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_defau Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default. Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default. Definition sig_ii_i := mksignature (Tint :: Tint :: nil) (Some Tint) cc_default. +Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default. +Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default. Class helper_functions := mk_helper_functions { i64_dtos: ident; (**r float64 -> signed long *) @@ -90,6 +92,8 @@ Class helper_functions := mk_helper_functions { i32_udiv: ident; (**r unsigned division *) i32_smod: ident; (**r signed remainder *) i32_umod: ident; (**r unsigned remainder *) + f64_div: ident; (**float division*) + f32_div: ident; (**float division*) }. Context {hf: helper_functions}. @@ -537,6 +541,11 @@ Nondetfunction builtin_arg (e: expr) := (* float division *) -Definition divfbase (e1: expr) (e2: expr) := - Eop Odivf (e1 ::: e2 ::: Enil). +Definition divf_base (e1: expr) (e2: expr) := + (* Eop Odivf (e1 ::: e2 ::: Enil). *) + Eexternal f64_div sig_ff_f (e1 ::: e2 ::: Enil). + +Definition divfs_base (e1: expr) (e2: expr) := + (* Eop Odivf (e1 ::: e2 ::: Enil). *) + Eexternal f32_div sig_ss_s (e1 ::: e2 ::: Enil). End SELECT. |