From 70609c932e066ffab0d2e3a2a38d66e834399532 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 19:14:32 +0200 Subject: Transform non-recursive Fixpoint into Definition As detected by the new warning in Coq 8.12. The use of Fixpoint here is not warranted and either an oversight or a leftover from an earlier version. --- common/AST.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index fcbf0b34..ddd10ede 100644 --- a/common/AST.v +++ b/common/AST.v @@ -105,7 +105,7 @@ Lemma rettype_eq: forall (t1 t2: rettype), {t1=t2} + {t1<>t2}. Proof. generalize typ_eq; decide equality. Defined. Global Opaque rettype_eq. -Fixpoint proj_rettype (r: rettype) : typ := +Definition proj_rettype (r: rettype) : typ := match r with | Tret t => t | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => Tint -- cgit From 4cf2fc41657fac51d806c14fdf481c7047e39df3 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 25 Jul 2020 10:38:18 +0200 Subject: Add support for __builtin_fabsf --- common/Builtins0.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'common') diff --git a/common/Builtins0.v b/common/Builtins0.v index 8da98314..4afe6f1a 100644 --- a/common/Builtins0.v +++ b/common/Builtins0.v @@ -332,6 +332,7 @@ End LOOKUP. Inductive standard_builtin : Type := | BI_select (t: typ) | BI_fabs + | BI_fabsf | BI_fsqrt | BI_negl | BI_addl @@ -364,6 +365,7 @@ Definition standard_builtin_table : list (string * standard_builtin) := :: ("__builtin_sel", BI_select Tfloat) :: ("__builtin_sel", BI_select Tsingle) :: ("__builtin_fabs", BI_fabs) + :: ("__builtin_fabsf", BI_fabsf) :: ("__builtin_fsqrt", BI_fsqrt) :: ("__builtin_negl", BI_negl) :: ("__builtin_addl", BI_addl) @@ -396,6 +398,8 @@ Definition standard_builtin_sig (b: standard_builtin) : signature := mksignature (Tint :: t :: t :: nil) t cc_default | BI_fabs | BI_fsqrt => mksignature (Tfloat :: nil) Tfloat cc_default + | BI_fabsf => + mksignature (Tsingle :: nil) Tsingle cc_default | BI_negl => mksignature (Tlong :: nil) Tlong cc_default | BI_addl | BI_subl | BI_i64_umulh| BI_i64_smulh @@ -428,6 +432,7 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig | _ => None end) _ _ | BI_fabs => mkbuiltin_n1t Tfloat Tfloat Float.abs + | BI_fabsf => mkbuiltin_n1t Tsingle Tsingle Float32.abs | BI_fsqrt => mkbuiltin_n1t Tfloat Tfloat Float.sqrt | BI_negl => mkbuiltin_n1t Tlong Tlong Int64.neg | BI_addl => mkbuiltin_v2t Tlong Val.addl _ _ -- cgit From 77ce8ba291afa9f5629a160df440f9af6614f3ef Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 27 Jul 2020 09:54:00 +0200 Subject: Add __builtin_sqrt as synonymous for __builtin_fsqrt __builtin_sqrt (no "f") is the name used by GCC and Clang. --- common/Builtins0.v | 1 + 1 file changed, 1 insertion(+) (limited to 'common') diff --git a/common/Builtins0.v b/common/Builtins0.v index 4afe6f1a..d84c9112 100644 --- a/common/Builtins0.v +++ b/common/Builtins0.v @@ -367,6 +367,7 @@ Definition standard_builtin_table : list (string * standard_builtin) := :: ("__builtin_fabs", BI_fabs) :: ("__builtin_fabsf", BI_fabsf) :: ("__builtin_fsqrt", BI_fsqrt) + :: ("__builtin_sqrt", BI_fsqrt) :: ("__builtin_negl", BI_negl) :: ("__builtin_addl", BI_addl) :: ("__builtin_subl", BI_subl) -- cgit