diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 56bdc4be01fa55488dceaaea12694183e084388d..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
@@ -2903,13 +2904,14 @@ let areCompatibleTypes ?context t1 t2 =
(* Specify whether the cast is from the source code *)
let rec castTo ?context ?(fromsource=false)
(ot : typ) (nt : typ) (e : exp) : (typ * exp ) =
- Kernel.debug ~dkey:Kernel.dkey_typing_cast "@[%t: castTo:%s %a->%a@\n@]"
+ let dkey = Kernel.dkey_typing_cast in
+ Kernel.debug ~dkey "@[%t: castTo:%s %a->%a@\n@]"
Cil.pp_thisloc (if fromsource then "(source)" else "")
Cil_datatype.Typ.pretty ot Cil_datatype.Typ.pretty nt;
if not fromsource && not (need_cast ot nt) then begin
(* Do not put the cast if it is not necessary, unless it is from the
* source. *)
- Kernel.debug ~dkey:Kernel.dkey_typing_cast "no cast to perform";
+ Kernel.debug ~dkey "no cast to perform";
(ot, e)
end else begin
let nt = if fromsource then nt else !typeForInsertedCast e ot nt in
@@ -2921,8 +2923,7 @@ let rec castTo ?context ?(fromsource=false)
in
(* [BM] uncomment the following line to enable attributes static typing
ignore (check_strict_attributes true ot nt && check_strict_attributes false nt ot);*)
- Kernel.debug ~dkey:Kernel.dkey_typing_cast
- "@[castTo: ot=%a nt=%a\n result is %a@\n@]"
+ Kernel.debug ~dkey "@[castTo: ot=%a nt=%a\n result is %a@\n@]"
Cil_datatype.Typ.pretty ot Cil_datatype.Typ.pretty nt
Cil_printer.pp_exp (snd result);
(* Now see if we can have a cast here *)
@@ -2930,14 +2931,16 @@ let rec castTo ?context ?(fromsource=false)
| TNamed _, _
| _, TNamed _ -> Kernel.fatal ~current:true "unrollType failed in castTo"
| t, TInt(IBool,_) when is_scalar_type t ->
- if is_boolean_result e then result
- else
- nt,
- Cil.mkCastT
- ~oldt:ot ~newt:nt
- (constFold true
- (new_exp ~loc:e.eloc
- (BinOp(Ne,e,Cil.integer ~loc:e.eloc 0,intType))))
+ if is_boolean_result e then begin
+ Kernel.debug ~dkey "Explicit cast to Boolean: %a" Cil_printer.pp_exp e;
+ result
+ end else begin
+ Kernel.debug ~dkey
+ "bool conversion by checking !=0: %a" Cil_printer.pp_exp e;
+ 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 *)
(* if ikindo = ikindn then (nt, e) else *)
@@ -3046,12 +3049,12 @@ let rec castTo ?context ?(fromsource=false)
result
| (TInt _ | TPtr _), TBuiltin_va_list _ ->
- Kernel.debug ~dkey:Kernel.dkey_typing_cast ~current:true
+ Kernel.debug ~dkey ~current:true
"Casting %a to __builtin_va_list" Cil_datatype.Typ.pretty ot ;
result
| TPtr _, TEnum _ ->
- Kernel.debug ~dkey:Kernel.dkey_typing_cast ~current:true
+ Kernel.debug ~dkey ~current:true
"Casting a pointer into an enumeration type" ;
result
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index b12618051d597aabd339dd8b8be1b42905ffa0fb..740ca94c2c576e8051f3a7454075ab85eb96ec5b 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -6530,7 +6530,7 @@ unsigned long long __fc_atomic_fetch_and_explicit(void *obj,
_Bool atomic_flag_test_and_set(atomic_flag volatile *object)
{
- _Bool r = (_Bool)(object->__fc_val != 0);
+ _Bool r = (_Bool)((int)object->__fc_val != 0);
object->__fc_val = (unsigned char)1;
return r;
}
@@ -6538,7 +6538,7 @@ _Bool atomic_flag_test_and_set(atomic_flag volatile *object)
_Bool atomic_flag_test_and_set_explicit(atomic_flag volatile *object,
memory_order order)
{
- _Bool r = (_Bool)(object->__fc_val != 0);
+ _Bool r = (_Bool)((int)object->__fc_val != 0);
object->__fc_val = (unsigned char)1;
return r;
}
diff --git a/tests/syntax/bool_conversion.i b/tests/syntax/bool_conversion.i
new file mode 100644
index 0000000000000000000000000000000000000000..26f67d534a06c94ddb257626a6f0683aa3dbd28c
--- /dev/null
+++ b/tests/syntax/bool_conversion.i
@@ -0,0 +1,10 @@
+_Bool get_bool(void);
+_Bool pass_bool(_Bool b);
+
+_Bool b_flag1, b_flag2;
+
+void main(){
+
+ b_flag1 = pass_bool( !(_Bool)get_bool() );
+ b_flag2 = pass_bool( (_Bool)get_bool() );
+}
diff --git a/tests/syntax/oracle/bool_conversion.err.oracle b/tests/syntax/oracle/bool_conversion.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/syntax/oracle/bool_conversion.res.oracle b/tests/syntax/oracle/bool_conversion.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..11c18ae513c504250171e46ce9097d664ee2d07b
--- /dev/null
+++ b/tests/syntax/oracle/bool_conversion.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing bool_conversion.i (no preprocessing)
+/* Generated by Frama-C */
+_Bool get_bool(void);
+
+_Bool pass_bool(_Bool b);
+
+_Bool b_flag1;
+_Bool b_flag2;
+void main(void)
+{
+ int tmp_0;
+ _Bool tmp;
+ _Bool tmp_1;
+ tmp = get_bool();
+ 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(tmp_1);
+ return;
+}
+
+