diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-12 22:57:31 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-12 22:57:31 +0100 |
| commit | 761a1e046b4fb276ee0b63785ed20a35c26641c9 (patch) | |
| tree | 58b3ed3d492577e969d2fc6137519b2630060648 /kvx/Builtins1.v | |
| parent | 728c4dfe489b78b9816d2efb039618168eada263 (diff) | |
| download | compcert-kvx-761a1e046b4fb276ee0b63785ed20a35c26641c9.tar.gz compcert-kvx-761a1e046b4fb276ee0b63785ed20a35c26641c9.zip | |
fix assembly syntax
Diffstat (limited to 'kvx/Builtins1.v')
| -rw-r--r-- | kvx/Builtins1.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/kvx/Builtins1.v b/kvx/Builtins1.v index 441345bf..de0d9885 100644 --- a/kvx/Builtins1.v +++ b/kvx/Builtins1.v @@ -25,7 +25,9 @@ Inductive platform_builtin : Type := | BI_fminf | BI_fmaxf | BI_fma -| BI_fmaf. +| BI_fmaf +| BI_lround_ne +| BI_luround_ne. Local Open Scope string_scope. @@ -36,6 +38,8 @@ Definition platform_builtin_table : list (string * platform_builtin) := :: ("__builtin_fmaxf", BI_fmaxf) :: ("__builtin_fma", BI_fma) :: ("__builtin_fmaf", BI_fmaf) + :: ("__builtin_lround_ne", BI_lround_ne) + :: ("__builtin_luround_ne", BI_luround_ne) :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := @@ -48,6 +52,8 @@ Definition platform_builtin_sig (b: platform_builtin) : signature := mksignature (Tfloat :: Tfloat :: Tfloat :: nil) Tfloat cc_default | BI_fmaf => mksignature (Tsingle :: Tsingle :: Tsingle :: nil) Tsingle cc_default + | BI_lround_ne | BI_luround_ne => + mksignature (Tfloat :: nil) Tlong cc_default end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := @@ -58,4 +64,6 @@ Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (pl | BI_fmaxf => mkbuiltin_n2t Tsingle Tsingle Tsingle ExtFloat32.max | BI_fma => mkbuiltin_n3t Tfloat Tfloat Tfloat Tfloat Float.fma | BI_fmaf => mkbuiltin_n3t Tsingle Tsingle Tsingle Tsingle Float32.fma + | BI_lround_ne => mkbuiltin_n1p Tfloat Tlong Float.to_long_ne + | BI_luround_ne => mkbuiltin_n1p Tfloat Tlong Float.to_longu_ne end. |