From 159736b13d362a65945ba095535c056eddbd35ec Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 20 Sep 2024 09:10:41 +0200
Subject: [PATCH] [Kernel] improve mergecil warning about conflicting types
---
src/kernel_internals/typing/mergecil.ml | 20 ++++++++++++--------
tests/cil/oracle/cpu_a.res.oracle | 4 ++--
tests/cil/oracle/cpu_b.res.oracle | 4 ++--
tests/spec/oracle/multiple_file_1.res.oracle | 4 ++--
4 files changed, 18 insertions(+), 14 deletions(-)
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index 1ef46b685b7..a1f9fafc0c4 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 02859882344..1ee62144a15 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 80bec54ee47..47b3250e65a 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 bd727cfaaa2..b1c1d0014a1 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:
--
GitLab