diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 09:44:00 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 09:44:00 +0100 |
| commit | 82be9309276a2de2cff6ab96ef7f7b74bb34ffbb (patch) | |
| tree | 8fd1a4ebd992c7accd7c6f51874f0f1beaa3ac3a /backend | |
| parent | 4437accc3ce393a7dbeda34b51f3507ba6c4f47f (diff) | |
| download | compcert-kvx-82be9309276a2de2cff6ab96ef7f7b74bb34ffbb.tar.gz compcert-kvx-82be9309276a2de2cff6ab96ef7f7b74bb34ffbb.zip | |
during merge; still some typing issues
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/OpHelpers.v | 20 | ||||
| -rw-r--r-- | backend/SplitLong.vp | 2 |
2 files changed, 12 insertions, 10 deletions
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. |