diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml index 1ef46b685b7ea640fac086d71229c8f65a397055..a1f9fafc0c4da634416a94cbd24cb52b467afeaf 100644 --- a/src/kernel_internals/typing/mergecil.ml +++ b/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); diff --git a/tests/cil/oracle/cpu_a.res.oracle b/tests/cil/oracle/cpu_a.res.oracle index 02859882344d809e85673de3e68f05c572ab225d..1ee62144a1558d5fa9515d7c2247c64495ea3993 100644 --- a/tests/cil/oracle/cpu_a.res.oracle +++ b/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) diff --git a/tests/cil/oracle/cpu_b.res.oracle b/tests/cil/oracle/cpu_b.res.oracle index 80bec54ee4754e6fecfc3f17745a2d71082d28e5..47b3250e65adc30f3d568c7f8c7ddb8607ea4f4f 100644 --- a/tests/cil/oracle/cpu_b.res.oracle +++ b/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); diff --git a/tests/spec/oracle/multiple_file_1.res.oracle b/tests/spec/oracle/multiple_file_1.res.oracle index bd727cfaaa2c878d211d6f5b72503e1945c05538..b1c1d0014a12d8c78010c7518ffb9113fc881ce6 100644 --- a/tests/spec/oracle/multiple_file_1.res.oracle +++ b/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: