From 64c366a8b2e2db3d59fd94e26e1e98818ad26cd7 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 25 Apr 2019 08:27:40 +0200
Subject: [PATCH] [kernel] make is_bool part of the API
---
src/kernel_services/ast_queries/cil.ml | 9 +++++----
src/kernel_services/ast_queries/cil.mli | 10 ++++++++++
src/plugins/value/legacy/eval_terms.ml | 6 +-----
3 files changed, 16 insertions(+), 9 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index fe50aa91f40..c088eed195f 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -4500,12 +4500,13 @@ let isCharConstPtrType t =
( is_unrollable_ltdef tdef && isLogicBooleanType (unroll_ltdef t))
| Lreal | Lvar _ | Larrow _ -> false
+let isBoolType typ = match unrollType typ with
+ | TInt (IBool, _) -> true
+ | _ -> false
+
let rec isLogicPureBooleanType t =
match t with
- | Ctype t ->
- (match unrollType t with
- | TInt(IBool,_) -> true
- | _ -> false)
+ | Ctype t -> isBoolType t
| Ltype ({lt_name = name} as def,_) ->
name = Utf8_logic.boolean ||
(is_unrollable_ltdef def && isLogicPureBooleanType (unroll_ltdef t))
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 1116abafa18..bcb8991186a 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -537,6 +537,16 @@ val isCharArrayType: typ -> bool
(** True if the argument is an integral type (i.e. integer or enum) *)
val isIntegralType: typ -> bool
+(** True if the argument is [_Bool]
+ @since Frama-C+dev
+*)
+val isBoolType: typ -> bool
+
+(** True if the argument is [_Bool] or [boolean].
+ @since Frama-C+dev
+ *)
+val isLogicPureBooleanType: logic_type -> bool
+
(** True if the argument is an integral or pointer type. *)
val isIntegralOrPointerType: typ -> bool
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index c60e4d58b85..e77caab5c5c 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -613,10 +613,6 @@ let cast_to_bool r =
{ eover; eunder = under_from_over eover;
ldeps = r.ldeps; etype = TInt (IBool, []) }
-let is_bool typ = match Cil.unrollType typ with
- | TInt (IBool, _) -> true
- | _ -> false
-
(* -------------------------------------------------------------------------- *)
(* --- Inlining of defined logic functions and predicates --- *)
(* -------------------------------------------------------------------------- *)
@@ -851,7 +847,7 @@ let rec eval_term ~alarm_mode env t =
(* See if the cast does something. If not, we can keep eunder as is.*)
if is_noop_cast ~src_typ:t.term_type ~dst_typ:typ
then { r with etype = typ }
- else if is_bool typ
+ else if Cil.isBoolType typ
then cast_to_bool r
else
let eover = cast ~src_typ:r.etype ~dst_typ:typ r.eover in
--
GitLab