diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index fe50aa91f404c5a6d033d68356e33ea81fb93a33..c088eed195f8144256271503379efb0343b517fd 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 1116abafa18caf628cea7c9a72315e369b6c0e64..bcb8991186ad056f30b552187d9ab42c0e35fec8 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 c60e4d58b855bdaf7bba2936f9699c66d66e97a3..e77caab5c5cef1c8d13189efc6d896b5aa67be47 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