added helper functions but strange

idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration

1 files changed, 0 insertions, 30 deletions

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}.