From d352db814aea8bb4107828ffd9665c8a5d75dbbe Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 27 Sep 2024 12:19:51 +0200
Subject: [PATCH] [doc] API + typo
---
src/kernel_services/ast_queries/logic_const.mli | 4 +++-
src/kernel_services/ast_queries/logic_typing.ml | 2 +-
2 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 8a50da3865..d5b6b3e495 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -299,7 +299,9 @@ val term : ?loc:Location.t -> term_node -> logic_type -> term
(** [..] of integers *)
val trange: ?loc:Location.t -> term option * term option -> term
-(** boolean constant *)
+(** boolean constant
+ @since Frama-C+dev
+*)
val tboolean: ?loc:Location.t -> bool -> term
(** integer constant *)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 2709441e54..7fb4387854 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1456,7 +1456,7 @@ struct
Logic_const.term
~loc (Tapp(truncate_info,[], [logic_coerce Lreal e])) Linteger
| Ctype t, Lreal when isArithmeticType t -> logic_coerce Lreal e
- | Ctype _, (Lreal | Linteger | Lboolean ) ->
+ | Ctype _, (Lreal | Linteger | Lboolean) ->
C.error loc "invalid implicit cast from %a to logic type %a"
Cil_printer.pp_logic_type e.term_type
Cil_printer.pp_logic_type newt
--
GitLab