aboutsummaryrefslogtreecommitdiffstats
path: root/backend
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-02-24 09:59:26 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-02-24 09:59:26 +0100
commit0cbfc9bd7d6b1878e5ff14fe8b8cc41ae07cdbec (patch)
treef35d22be77bd8e2bafede8b8f106a6aaedf1cad9 /backend
parent66de649c75bc5625f0eab42d299f2281a3872510 (diff)
downloadcompcert-kvx-0cbfc9bd7d6b1878e5ff14fe8b8cc41ae07cdbec.tar.gz
compcert-kvx-0cbfc9bd7d6b1878e5ff14fe8b8cc41ae07cdbec.zip
rm commented out block
Diffstat (limited to 'backend')
-rw-r--r--backend/SplitLong.vp32
1 files changed, 0 insertions, 32 deletions
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp
index 4464bcdb..dfe42df0 100644
--- a/backend/SplitLong.vp
+++ b/backend/SplitLong.vp
@@ -22,38 +22,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) Tlong cc_default.
-Definition sig_l_f := mksignature (Tlong :: nil) Tfloat cc_default.
-Definition sig_l_s := mksignature (Tlong :: nil) Tsingle cc_default.
-Definition sig_f_l := mksignature (Tfloat :: nil) Tlong cc_default.
-Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) Tlong cc_default.
-Definition sig_li_l := mksignature (Tlong :: Tint :: nil) Tlong cc_default.
-Definition sig_ii_l := mksignature (Tint :: Tint :: nil) Tlong cc_default.
-*)
-
Section SELECT.
Context {hf: helper_functions}.