diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-30 19:10:42 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-08-30 19:10:42 +0200 |
| commit | caac487ae23a9785602cf235f5b4a2b6749f2c18 (patch) | |
| tree | e81ae59a6e06a0373afdfbf8f1ee94f16a2770f2 /mppa_k1c/Builtins1.v | |
| parent | 1522f289301f37da0324570297c65256d8a32316 (diff) | |
| download | compcert-kvx-caac487ae23a9785602cf235f5b4a2b6749f2c18.tar.gz compcert-kvx-caac487ae23a9785602cf235f5b4a2b6749f2c18.zip | |
fma
Diffstat (limited to 'mppa_k1c/Builtins1.v')
| -rw-r--r-- | mppa_k1c/Builtins1.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/mppa_k1c/Builtins1.v b/mppa_k1c/Builtins1.v index 5187ea7d..6186961f 100644 --- a/mppa_k1c/Builtins1.v +++ b/mppa_k1c/Builtins1.v @@ -24,7 +24,9 @@ Inductive platform_builtin : Type := | BI_fmax | BI_fminf | BI_fmaxf -| BI_fabsf. +| BI_fabsf +| BI_fma +| BI_fmaf. Local Open Scope string_scope. @@ -34,6 +36,8 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__builtin_fminf", BI_fminf) :: ("__builtin_fmaxf", BI_fmaxf) :: ("__builtin_fabsf", BI_fabsf) + :: ("__builtin_fma", BI_fma) + :: ("__builtin_fmaf", BI_fmaf) :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := @@ -44,6 +48,10 @@ Definition platform_builtin_sig (b: platform_builtin) : signature := mksignature (Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default | BI_fabsf => mksignature (Tsingle :: nil) (Some Tsingle) cc_default + | BI_fma => + mksignature (Tfloat :: Tfloat :: Tfloat :: nil) (Some Tfloat) cc_default + | BI_fmaf => + mksignature (Tsingle :: Tsingle :: Tsingle :: nil) (Some Tsingle) cc_default end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) := @@ -53,4 +61,6 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_re | 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. |