From 96eb60c9c9b17e6c8f1c76f8d34d0c41a072222c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 31 Mar 2020 10:59:01 +0200
Subject: [PATCH] [kernel] unsupported long double builtins
---
src/kernel_services/ast_queries/logic_utils.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index c79a9d15400..b3fa33f9651 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -394,7 +394,8 @@ let is_boolean_binop op =
let float_builtin prefix fkind =
let name = match fkind with
| FFloat -> Printf.sprintf "\\%s_float" prefix
- | FDouble | FLongDouble -> Printf.sprintf "\\%s_double" prefix
+ | FDouble -> Printf.sprintf "\\%s_double" prefix
+ | FLongDouble -> Kernel.not_yet_implemented "Builtins for long double type"
in match Logic_env.find_all_logic_functions name with
| [ lf ] -> Some lf
| _ -> Kernel.fatal "Missing or ambiguous builtin %S" name
--
GitLab