From 50ea35fceb52c5f66ccbc4f709df3a3471b12647 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 19 Mar 2019 19:28:03 +0100 Subject: added helper functions but strange idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration --- backend/SplitLong.vp | 30 ------------------------------ 1 file changed, 30 deletions(-) (limited to 'backend/SplitLong.vp') diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index de954482..6a7d4f5c 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -21,36 +21,6 @@ Require Import SelectOp. Local Open Scope cminorsel_scope. Local Open Scope string_scope. -(** Some operations on 64-bit integers are transformed into calls to - runtime library functions. The following type class collects - the names of these functions. *) - -Class helper_functions := mk_helper_functions { - i64_dtos: ident; (**r float64 -> signed long *) - i64_dtou: ident; (**r float64 -> unsigned long *) - i64_stod: ident; (**r signed long -> float64 *) - i64_utod: ident; (**r unsigned long -> float64 *) - i64_stof: ident; (**r signed long -> float32 *) - i64_utof: ident; (**r unsigned long -> float32 *) - i64_sdiv: ident; (**r signed division *) - i64_udiv: ident; (**r unsigned division *) - i64_smod: ident; (**r signed remainder *) - i64_umod: ident; (**r unsigned remainder *) - i64_shl: ident; (**r shift left *) - i64_shr: ident; (**r shift right unsigned *) - i64_sar: ident; (**r shift right signed *) - i64_umulh: ident; (**r unsigned multiply high *) - i64_smulh: ident; (**r signed multiply high *) -}. - -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. Context {hf: helper_functions}. -- cgit