diff options
Diffstat (limited to 'backend/SelectLong.vp')
| -rw-r--r-- | backend/SelectLong.vp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp index 76cc79d..09f29af 100644 --- a/backend/SelectLong.vp +++ b/backend/SelectLong.vp @@ -46,13 +46,13 @@ Record helper_functions : Type := mk_helper_functions { i64_sar: ident (**r shift right signed *) }. -Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong). -Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat). -Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle). -Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong). -Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong). -Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong). -Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong). +Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. +Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default. +Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default. +Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default. +Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default. +Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default. +Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default. Section SELECT. |