From b03da2d0c63868aa00143fe17980e9edb2e9f9bc Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 30 Aug 2022 17:16:35 +0200
Subject: [PATCH] [typing] small refactoring of debug messages for cast
insertion
---
src/kernel_internals/typing/cabs2cil.ml | 21 +++++++++++++--------
1 file changed, 13 insertions(+), 8 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 56bdc4be01f..166bab88bf1 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2903,13 +2903,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 +2922,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 +2930,19 @@ 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
+ 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
+ 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))))
+ end
| TInt(_,_), TInt(_,_) ->
(* We used to ignore attributes on integer-integer casts. Not anymore *)
(* if ikindo = ikindn then (nt, e) else *)
@@ -3046,12 +3051,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
--
GitLab