From 82be9309276a2de2cff6ab96ef7f7b74bb34ffbb Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 24 Feb 2020 09:44:00 +0100 Subject: during merge; still some typing issues --- backend/OpHelpers.v | 20 ++++++++++---------- backend/SplitLong.vp | 2 ++ 2 files changed, 12 insertions(+), 10 deletions(-) (limited to 'backend') diff --git a/backend/OpHelpers.v b/backend/OpHelpers.v index 53414dab..b9b97903 100644 --- a/backend/OpHelpers.v +++ b/backend/OpHelpers.v @@ -6,16 +6,16 @@ Require Import Op CminorSel. runtime library functions. The following type class collects the names of these functions. *) -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. -Definition sig_ii_i := mksignature (Tint :: Tint :: nil) (Some Tint) cc_default. -Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default. -Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default. +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. +Definition sig_ii_i := mksignature (Tint :: Tint :: nil) Tint cc_default. +Definition sig_ff_f := mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default. +Definition sig_ss_s := mksignature (Tsingle :: Tsingle :: nil) Tsingle cc_default. Class helper_functions := mk_helper_functions { i64_dtos: ident; (**r float64 -> signed long *) diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index 73e22b98..4464bcdb 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -22,6 +22,7 @@ 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. *) @@ -51,6 +52,7 @@ 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. -- cgit