diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli index 8a50da386596a547d07725d512935d3873084b29..d5b6b3e495976d6eefd085fa85a3d83d4d9fe358 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 2709441e5420200abf87b7e0f8e88fe33a23dff7..7fb43878542d6eb4ecb59bb9537e98ae92e31cf1 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