diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index f99ddf62868dd2dadc831c14c2fdf5204d196304..4e6412b2e889cac067075e4c61d75eef677c7a3b 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -2759,7 +2759,7 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
prototypes. Logic specifications refer to the varinfo in this table. *)
begin
match vi.vtype with
- | TFun (_,Some formals , _, _ ) ->
+ | TFun (_,Some formals , _, _) ->
(try
let old_formals_env = getFormalsDecl oldvi in
List.iter2
@@ -2783,7 +2783,12 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
formals;
with
| Invalid_argument _ ->
- abort_context "Inconsistent formals" ;
+ abort_context
+ "Function %a redeclared with incompatible formals \
+ (original declaration was at %a)"
+ Cil_datatype.Varinfo.pretty vi
+ Cil_datatype.Location.pretty oldloc
+ ;
| Not_found ->
Cil.setFormalsDecl oldvi vi.vtype)
| _ -> ()
diff --git a/tests/syntax/oracle/ghost_parameters.10.res.oracle b/tests/syntax/oracle/ghost_parameters.10.res.oracle
index 4cfa52c3e8ef347cf27b3eef902756e4d2f5a02f..4da452094df32e2e2da684c45537fc72e9155088 100644
--- a/tests/syntax/oracle/ghost_parameters.10.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.10.res.oracle
@@ -2,7 +2,7 @@
[kernel] ghost_parameters.c:187: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:181 (different number of arguments).
[kernel] ghost_parameters.c:187: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:181)
185 }
186
187 void function(int a, int b) /*@ ghost(int c, int d) */ {
diff --git a/tests/syntax/oracle/ghost_parameters.3.res.oracle b/tests/syntax/oracle/ghost_parameters.3.res.oracle
index fbb313828d4826ad54d21734248b953f19747e72..38b53517ac2093f1177583a8fa98ed9e2a170e12 100644
--- a/tests/syntax/oracle/ghost_parameters.3.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.3.res.oracle
@@ -2,7 +2,7 @@
[kernel] ghost_parameters.c:92: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:88 (different number of arguments).
[kernel] ghost_parameters.c:92: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:88)
90 }
91
92 void function(int a, int b) /*@ ghost(int c, int d) */ {
diff --git a/tests/syntax/oracle/ghost_parameters.4.res.oracle b/tests/syntax/oracle/ghost_parameters.4.res.oracle
index 6fc15e643c37c4bd05d5d8caa37f168a77748d4e..f07d36bc7a2202eef036a55775edb332bb4a0bc7 100644
--- a/tests/syntax/oracle/ghost_parameters.4.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.4.res.oracle
@@ -2,7 +2,7 @@
[kernel] ghost_parameters.c:106: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:100 (different number of arguments).
[kernel] ghost_parameters.c:106: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:100)
104 }
105
106 void function(int a, int b) /*@ ghost(int c, int d) */ {
diff --git a/tests/syntax/oracle/ghost_parameters.5.res.oracle b/tests/syntax/oracle/ghost_parameters.5.res.oracle
index da3a4a8fca7024415abf47d88324746fed939d09..824a1c0380c7f7f9a77073c40643a3a58e2771fc 100644
--- a/tests/syntax/oracle/ghost_parameters.5.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.5.res.oracle
@@ -2,7 +2,7 @@
[kernel] ghost_parameters.c:119: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:115 (different number of ghost arguments).
[kernel] ghost_parameters.c:119: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:115)
117 }
118
119 void function(int a, int b) /*@ ghost(int c, int d) */ {
diff --git a/tests/syntax/oracle/ghost_parameters.6.res.oracle b/tests/syntax/oracle/ghost_parameters.6.res.oracle
index e94e03ed7c012c2ac70e38763d953bd255f253e9..6722a5254d4f99af476faa5cf46b1f2f8eb9816e 100644
--- a/tests/syntax/oracle/ghost_parameters.6.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.6.res.oracle
@@ -2,7 +2,7 @@
[kernel] ghost_parameters.c:133: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:127 (different number of ghost arguments).
[kernel] ghost_parameters.c:133: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:127)
131 }
132
133 void function(int a, int b) /*@ ghost(int c, int d) */ {
diff --git a/tests/syntax/oracle/ghost_parameters.7.res.oracle b/tests/syntax/oracle/ghost_parameters.7.res.oracle
index 8185ec1f58cfd27fcb1077ae8c83bb8006ebc7c9..9f9a551e2f6fa4d4fa1803eadce79f51d11b02e7 100644
--- a/tests/syntax/oracle/ghost_parameters.7.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.7.res.oracle
@@ -2,7 +2,7 @@
[kernel] ghost_parameters.c:146: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:142 (different number of arguments).
[kernel] ghost_parameters.c:146: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:142)
144 }
145
146 void function(int a, int b) /*@ ghost(int c, int d) */ {
diff --git a/tests/syntax/oracle/ghost_parameters.8.res.oracle b/tests/syntax/oracle/ghost_parameters.8.res.oracle
index c4b8f43294782b437e6ca7cfee8a7fbd8e5964ec..65509b4741fa55b4c21db801098c8b879636601c 100644
--- a/tests/syntax/oracle/ghost_parameters.8.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.8.res.oracle
@@ -2,7 +2,7 @@
[kernel] ghost_parameters.c:160: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:154 (different number of arguments).
[kernel] ghost_parameters.c:160: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:154)
158 }
159
160 void function(int a, int b) /*@ ghost(int c, int d) */ {
diff --git a/tests/syntax/oracle/ghost_parameters.9.res.oracle b/tests/syntax/oracle/ghost_parameters.9.res.oracle
index a27afa11a3c598d28b7450d04aa51672ce10b874..ba008d3a8c743a1da2c43e5d7fa25875ef1aea75 100644
--- a/tests/syntax/oracle/ghost_parameters.9.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.9.res.oracle
@@ -2,7 +2,7 @@
[kernel] ghost_parameters.c:173: User Error:
Declaration of function does not match previous declaration from ghost_parameters.c:169 (different number of arguments).
[kernel] ghost_parameters.c:173: User Error:
- Inconsistent formals
+ Function function redeclared with incompatible formals (original declaration was at ghost_parameters.c:169)
171 }
172
173 void function(int a, int b) /*@ ghost(int c, int d) */ {
diff --git a/tests/syntax/oracle/reject_use_decl_mismatch_bts728.0.res.oracle b/tests/syntax/oracle/reject_use_decl_mismatch_bts728.0.res.oracle
index 8bf3f8034fb35482c554e9fce89ad7e732402528..bf2f7f89e245cbd71d7a066e6ea9022572e2f2c6 100644
--- a/tests/syntax/oracle/reject_use_decl_mismatch_bts728.0.res.oracle
+++ b/tests/syntax/oracle/reject_use_decl_mismatch_bts728.0.res.oracle
@@ -5,7 +5,7 @@
[kernel] reject_use_decl_mismatch_bts728.c:19: User Error:
Declaration of f does not match previous declaration from reject_use_decl_mismatch_bts728.c:7 (different number of arguments).
[kernel] reject_use_decl_mismatch_bts728.c:19: User Error:
- Inconsistent formals
+ Function f redeclared with incompatible formals (original declaration was at reject_use_decl_mismatch_bts728.c:7)
17 }
18
19 int f(int x,int y, int z, int t,int t1,int t2,int t3,int t4,int t5,int t6) {
diff --git a/tests/syntax/oracle/reject_use_decl_mismatch_bts728.1.res.oracle b/tests/syntax/oracle/reject_use_decl_mismatch_bts728.1.res.oracle
index 1e4b063503a8d8763cea27368f2b61984d53617f..5d84c3028c2971a19e8d2a142c7ed3fe88e0d56a 100644
--- a/tests/syntax/oracle/reject_use_decl_mismatch_bts728.1.res.oracle
+++ b/tests/syntax/oracle/reject_use_decl_mismatch_bts728.1.res.oracle
@@ -4,7 +4,7 @@
[kernel] reject_use_decl_mismatch_bts728.c:19: User Error:
Declaration of f does not match previous declaration from reject_use_decl_mismatch_bts728.c:15 (different number of arguments).
[kernel] reject_use_decl_mismatch_bts728.c:19: User Error:
- Inconsistent formals
+ Function f redeclared with incompatible formals (original declaration was at reject_use_decl_mismatch_bts728.c:15)
17 }
18
19 int f(int x,int y, int z, int t,int t1,int t2,int t3,int t4,int t5,int t6) {
diff --git a/tests/syntax/oracle/syntactic_hook.res.oracle b/tests/syntax/oracle/syntactic_hook.res.oracle
index 19d5998e0ad1e79fd5a7fa4e388476c31f59be9d..22cd7bb63303436f32a7c1ebdd6e5cce200468ef 100644
--- a/tests/syntax/oracle/syntactic_hook.res.oracle
+++ b/tests/syntax/oracle/syntactic_hook.res.oracle
@@ -39,7 +39,7 @@
[kernel] syntactic_hook.i:30: Warning:
[SH]: conflict with declaration of f at line 8: different number of arguments
[kernel] syntactic_hook.i:30: User Error:
- Inconsistent formals
+ Function f redeclared with incompatible formals (original declaration was at syntactic_hook.i:8)
28 }
29
30 int f(int); //error: conflicting decls