diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 09:59:26 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 09:59:26 +0100 |
commit | 0cbfc9bd7d6b1878e5ff14fe8b8cc41ae07cdbec (patch) | |
tree | f35d22be77bd8e2bafede8b8f106a6aaedf1cad9 /backend | |
parent | 66de649c75bc5625f0eab42d299f2281a3872510 (diff) | |
download | compcert-kvx-0cbfc9bd7d6b1878e5ff14fe8b8cc41ae07cdbec.tar.gz compcert-kvx-0cbfc9bd7d6b1878e5ff14fe8b8cc41ae07cdbec.zip |
rm commented out block
Diffstat (limited to 'backend')
-rw-r--r-- | backend/SplitLong.vp | 32 |
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}. |