diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 166bab88bf123e829412ac3c1e7d8524a0ba5329..4bfb3e211bbbab031226a59ebbfd9c59895caf74 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -2936,12 +2936,9 @@ let rec castTo ?context ?(fromsource=false) end else begin Kernel.debug ~dkey "bool conversion by checking !=0: %a" Cil_printer.pp_exp e; - nt, - Cil.mkCastT - ~oldt:ot ~newt:nt - (constFold true - (new_exp ~loc:e.eloc - (BinOp(Ne,e,Cil.integer ~loc:e.eloc 0,intType)))) + let cmp = Cil.mkBinOp ~loc:e.eloc Ne e (Cil.integer ~loc:e.eloc 0) in + let oldt = Cil.typeOf cmp in + nt, Cil.mkCastT ~oldt ~newt:nt cmp end | TInt(_,_), TInt(_,_) -> (* We used to ignore attributes on integer-integer casts. Not anymore *) diff --git a/tests/syntax/oracle/bool_conversion.res.oracle b/tests/syntax/oracle/bool_conversion.res.oracle index 1e0bd4fc5100eb6639efc96115d662fcbf8a6409..1dc3bc0af15b22422c906f8e3b3054e7194f9a18 100644 --- a/tests/syntax/oracle/bool_conversion.res.oracle +++ b/tests/syntax/oracle/bool_conversion.res.oracle @@ -1,3 +1,4 @@ +[kernel] Parsing bool_conversion.i (no preprocessing) /* Generated by Frama-C */ _Bool get_bool(void); @@ -11,10 +12,10 @@ void main(void) _Bool tmp; _Bool tmp_1; tmp = get_bool(); - if (tmp != 0) tmp_0 = 0; else tmp_0 = 1; + if ((_Bool)((int)tmp != 0)) tmp_0 = 0; else tmp_0 = 1; b_flag1 = pass_bool((_Bool)(tmp_0 != 0)); tmp_1 = get_bool(); - b_flag2 = pass_bool(tmp_1 != 0); + b_flag2 = pass_bool((_Bool)((int)tmp_1 != 0)); return; }