diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-03 20:04:46 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-03 20:04:46 +0100 |
| commit | 48dc03004ba4078670b583561b108043085334b8 (patch) | |
| tree | a72314b395b026a35b5b2a2944c1c40fb9af63f2 | |
| parent | 8bb9da5166ff1a07d325cd378b977d5d6bf3105a (diff) | |
| download | compcert-kvx-48dc03004ba4078670b583561b108043085334b8.tar.gz compcert-kvx-48dc03004ba4078670b583561b108043085334b8.zip | |
some fixes for KVX
| -rw-r--r-- | kvx/Builtins1.v | 5 | ||||
| -rw-r--r-- | kvx/SelectOp.vp | 1 |
2 files changed, 0 insertions, 6 deletions
diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v index eeb578d0..441345bf 100644 --- a/kvx/Builtins1.v +++ b/kvx/Builtins1.v @@ -24,7 +24,6 @@ Inductive platform_builtin : Type := | BI_fmax | BI_fminf | BI_fmaxf -| BI_fabsf | BI_fma | BI_fmaf. @@ -35,7 +34,6 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__builtin_fmax", BI_fmax) :: ("__builtin_fminf", BI_fminf) :: ("__builtin_fmaxf", BI_fmaxf) - :: ("__builtin_fabsf", BI_fabsf) :: ("__builtin_fma", BI_fma) :: ("__builtin_fmaf", BI_fmaf) :: nil. @@ -46,8 +44,6 @@ Definition platform_builtin_sig (b: platform_builtin) : signature := mksignature (Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fminf | BI_fmaxf => mksignature (Tsingle :: Tsingle :: nil) Tsingle cc_default - | BI_fabsf => - mksignature (Tsingle :: nil) Tsingle cc_default | BI_fma => mksignature (Tfloat :: Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fmaf => @@ -60,7 +56,6 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl | BI_fmax => mkbuiltin_n2t Tfloat Tfloat Tfloat ExtFloat.max | BI_fminf => mkbuiltin_n2t Tsingle Tsingle Tsingle ExtFloat32.min | BI_fmaxf => mkbuiltin_n2t Tsingle Tsingle Tsingle ExtFloat32.max - | BI_fabsf => mkbuiltin_n1t Tsingle Tsingle Float32.abs | BI_fma => mkbuiltin_n3t Tfloat Tfloat Tfloat Tfloat Float.fma | BI_fmaf => mkbuiltin_n3t Tsingle Tsingle Tsingle Tsingle Float32.fma end. diff --git a/kvx/SelectOp.vp b/kvx/SelectOp.vp index 65dba3ac..aa241c1e 100644 --- a/kvx/SelectOp.vp +++ b/kvx/SelectOp.vp @@ -704,7 +704,6 @@ Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr | BI_fmax => Some (Eop Omaxf args) | BI_fminf => Some (Eop Ominfs args) | BI_fmaxf => Some (Eop Omaxfs args) - | BI_fabsf => Some (Eop Oabsfs args) | BI_fma => gen_fma args | BI_fmaf => gen_fmaf args end. |