diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 4bfb3e211bbbab031226a59ebbfd9c59895caf74..aeda98b67563ea1b445e3b55d73c3f319106505d 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -1403,6 +1403,7 @@ let dropQualifiers = Cil.type_remove_qualifier_attributes (* true if the expression is known to be a boolean result, i.e. 0 or 1. *) let rec is_boolean_result e = + Cil.(isBoolType (typeOf e)) || match e.enode with | Const _ -> (match Cil.isInteger e with @@ -2932,7 +2933,7 @@ let rec castTo ?context ?(fromsource=false) | t, TInt(IBool,_) when is_scalar_type t -> if is_boolean_result e then begin Kernel.debug ~dkey "Explicit cast to Boolean: %a" Cil_printer.pp_exp e; - nt,Cil.mkCastT ~oldt:ot ~newt:nt e + result end else begin Kernel.debug ~dkey "bool conversion by checking !=0: %a" Cil_printer.pp_exp e; diff --git a/tests/syntax/oracle/bool_conversion.res.oracle b/tests/syntax/oracle/bool_conversion.res.oracle index 1dc3bc0af15b22422c906f8e3b3054e7194f9a18..11c18ae513c504250171e46ce9097d664ee2d07b 100644 --- a/tests/syntax/oracle/bool_conversion.res.oracle +++ b/tests/syntax/oracle/bool_conversion.res.oracle @@ -12,10 +12,10 @@ void main(void) _Bool tmp; _Bool tmp_1; tmp = get_bool(); - if ((_Bool)((int)tmp != 0)) tmp_0 = 0; else tmp_0 = 1; + if (tmp) tmp_0 = 0; else tmp_0 = 1; b_flag1 = pass_bool((_Bool)(tmp_0 != 0)); tmp_1 = get_bool(); - b_flag2 = pass_bool((_Bool)((int)tmp_1 != 0)); + b_flag2 = pass_bool(tmp_1); return; }