From 29d0240b4d420b593aa95c30b679caca81e90624 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 27 Feb 2024 19:56:29 +0100
Subject: [PATCH] [typing] better error message
---
src/kernel_internals/typing/cabs2cil.ml | 9 +++++++--
tests/syntax/oracle/ghost_parameters.10.res.oracle | 2 +-
tests/syntax/oracle/ghost_parameters.3.res.oracle | 2 +-
tests/syntax/oracle/ghost_parameters.4.res.oracle | 2 +-
tests/syntax/oracle/ghost_parameters.5.res.oracle | 2 +-
tests/syntax/oracle/ghost_parameters.6.res.oracle | 2 +-
tests/syntax/oracle/ghost_parameters.7.res.oracle | 2 +-
tests/syntax/oracle/ghost_parameters.8.res.oracle | 2 +-
tests/syntax/oracle/ghost_parameters.9.res.oracle | 2 +-
.../oracle/reject_use_decl_mismatch_bts728.0.res.oracle | 2 +-
.../oracle/reject_use_decl_mismatch_bts728.1.res.oracle | 2 +-
tests/syntax/oracle/syntactic_hook.res.oracle | 2 +-
12 files changed, 18 insertions(+), 13 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index f99ddf62868..4e6412b2e88 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 4cfa52c3e8e..4da452094df 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 fbb313828d4..38b53517ac2 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 6fc15e643c3..f07d36bc7a2 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 da3a4a8fca7..824a1c0380c 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 e94e03ed7c0..6722a5254d4 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 8185ec1f58c..9f9a551e2f6 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 c4b8f432947..65509b4741f 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 a27afa11a3c..ba008d3a8c7 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 8bf3f8034fb..bf2f7f89e24 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 1e4b063503a..5d84c3028c2 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 19d5998e0ad..22cd7bb6330 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
--
GitLab