[Kernel] improve mergecil warning about conflicting types

src/kernel_internals/typing/mergecil.ml

@@ -1237,27 +1237,31 @@ let matchTypeInfoGen (combineF : combineFunction)
 let conflict_detected = ref false
 
 let combines = {
-  typ_combine = (fun combF ->
+  typ_combine = (fun combF ~strictInteger ~strictReturnTypes what t1 t2 ->
       let find_names_file = H.find fileNames in
       let oldfidx = Fidx.get_oldfidx () in
       let fidx = Fidx.get_fidx () in
       let old_file = find_names_file oldfidx in
-      let new_file = find_names_file fidx in
-      let old_name_file = Filepath.Normalized.to_pretty_string old_file in
-      let new_name_file = Filepath.Normalized.to_pretty_string new_file in
-      let pre_msg = "Conflicting definitions are between files "^
-                    old_name_file^" and "^new_name_file in
+      let pre_msg =
+        Format.asprintf
+          "Conflicting definitions for types '%a' and '%a' \
+           (previous definition was in file %s)."
+          Cil_printer.pp_typ t1
+          Cil_printer.pp_typ t2
+          (Filepath.Normalized.to_pretty_string old_file)
+      in
       let emitwith _ =
         if (not !conflict_detected) && oldfidx <> fidx
         then
           begin
             conflict_detected := true;
-            Kernel.warning
+            Kernel.warning ~current:true
               ~wkey:Kernel.wkey_merge_conversion
               "%s" pre_msg
           end
       in
-      combineTypesGen ~emitwith combF);
+      combineTypesGen
+        ~emitwith combF ~strictInteger ~strictReturnTypes what t1 t2);
   enum_combine = (fun _ oldei ei ->
       matchEnumInfoGen oldei ei;
       oldei);

tests/cil/oracle/cpu_a.res.oracle

@@ -2,8 +2,8 @@
 [kernel] Parsing cpu_b.c (with preprocessing)
 [kernel:typing:int-conversion] cpu_b.c:7: Warning: 
   Integer compatibility is machine-dependent: unsigned short and unsigned int
-[kernel:typing:merge-conversion] Warning: 
-  Conflicting definitions are between files cpu_a.c and cpu_b.c
+[kernel:typing:merge-conversion] cpu_b.c:7: Warning: 
+  Conflicting definitions for types 'unsigned short' and 'unsigned int' (previous definition was in file cpu_a.c).
 /* Generated by Frama-C */
 typedef unsigned short DWORD;
 DWORD f(void)

tests/cil/oracle/cpu_b.res.oracle

@@ -2,8 +2,8 @@
 [kernel] Parsing cpu_a.c (with preprocessing)
 [kernel:typing:int-conversion] cpu_a.c:6: Warning: 
   Integer compatibility is machine-dependent: unsigned int and unsigned short
-[kernel:typing:merge-conversion] Warning: 
-  Conflicting definitions are between files cpu_b.c and cpu_a.c
+[kernel:typing:merge-conversion] cpu_a.c:6: Warning: 
+  Conflicting definitions for types 'unsigned int' and 'unsigned short' (previous definition was in file cpu_b.c).
 /* Generated by Frama-C */
 typedef unsigned int DWORD;
 DWORD f(void);

tests/spec/oracle/multiple_file_1.res.oracle

@@ -2,8 +2,8 @@
 [kernel] Parsing multiple_file_2.c (with preprocessing)
 [kernel:typing:int-conversion] multiple_file_2.c:28: Warning: 
   Array type comparison succeeds only based on machine-dependent constant evaluation: int [sizeof(struct i_s2)] and int [sizeof(struct i_s2)]
-[kernel:typing:merge-conversion] Warning: 
-  Conflicting definitions are between files multiple_file_1.c and multiple_file_2.c
+[kernel:typing:merge-conversion] multiple_file_2.c:28: Warning: 
+  Conflicting definitions for types 'int [sizeof(struct i_s2)]' and 'int [sizeof(struct i_s2)]' (previous definition was in file multiple_file_1.c).
 [kernel:typing:int-conversion] multiple_file_2.c:36: Warning: 
   Array type comparison succeeds only based on machine-dependent constant evaluation: int [sizeof(void *)] and int [sizeof(struct i_s2)]
 [kernel:typing:int-conversion] multiple_file_2.c:38: Warning: