diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 604f00ef016190d6c3145df733d6d6f2dbee6237..e8af906672d83310d3e9e1e758b0a4259d7e88a6 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9590,6 +9590,12 @@ and doDecl local_env (isglobal: bool) : Cabs.definition -> chunk = function
and doTypedef ghost ((specs, nl): Cabs.name_group) =
(* Do the specifiers exactly once *)
+ if !scopes <> [] then
+ Kernel.warning
+ ~once:true ~current:true ~wkey:Kernel.wkey_parser_unsupported
+ "block-level typedefs currently unsupported;@ \
+ trying to convert it to a global-level typedef.@ \
+ Note that this may lead to incoherent error messages.";
let bt, sto, inl, attrs = doSpecList ghost (suggestAnonName nl) specs in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~current:true
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 657cd6c1e460b80b99eea472efa627a6e5a2d96a..dffe3cb4b69a0ed8e36137e4767117a5dd8c574e 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -199,6 +199,8 @@ let wkey_cmdline = register_warn_category "cmdline"
let wkey_audit = register_warn_category "audit"
let () = set_warn_status wkey_audit Log.Werror
+let wkey_parser_unsupported = register_warn_category "parser:unsupported"
+
(* ************************************************************************* *)
(** {2 Specialised functors for building kernel parameters} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 59dc0c0e9784f8e860279c0379e0fd90d0ad21b5..8a935ac016f350fb82646c09f6c36fda4f53def3 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -191,6 +191,9 @@ val wkey_cmdline: warn_category
val wkey_audit: warn_category
(** Warning related to options '-audit-*'. *)
+val wkey_parser_unsupported: warn_category
+(** Warning related to unsupported parsing-related features. *)
+
(* ************************************************************************* *)
(** {2 Functors for late option registration} *)
(** Kernel_function-related options cannot be registered in this module:
diff --git a/src/plugins/variadic/tests/known/printf_wrong_types.c b/src/plugins/variadic/tests/known/printf_wrong_types.c
index 85cfc9279a4d54d6d5856eb61003896518f8c424..b2d5c3da606cfd46df9593633f797d741ac15d5f 100644
--- a/src/plugins/variadic/tests/known/printf_wrong_types.c
+++ b/src/plugins/variadic/tests/known/printf_wrong_types.c
@@ -2,7 +2,7 @@
STDOPT: +"-then -variadic-no-translation -then -variadic-translation -variadic-no-strict"
*/
-
+typedef enum { OK, ERROR } RC;
#include <stdio.h>
int main(){
@@ -30,7 +30,7 @@ int main(){
printf("%s", i); // Wrong type
printf("%d", string); // Wrong type
- typedef enum { OK, ERROR } RC;
+
RC rc = OK;
printf("%u", rc); // Correct type with '-enums gcc-enums'
printf("%d", rc); // Wrong type (in strict mode)
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index e66c217886a6480270b73f72f1060e85a8bea2fd..50dc81713305db352d3360952a9447313a6433cf 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -57,8 +57,8 @@
"annot:multi-from", "annot-error", "audit", "check",
"check:volatile", "cmdline", "ghost", "ghost:bad-use", "inline",
"linker", "linker:drop-conflicting-unused", "parser",
- "parser:conditional-feature", "pp", "pp:compilation-db", "typing",
- "typing:implicit-conv-void-ptr",
+ "parser:conditional-feature", "parser:unsupported", "pp",
+ "pp:compilation-db", "typing", "typing:implicit-conv-void-ptr",
"typing:implicit-function-declaration",
"typing:incompatible-pointer-types",
"typing:incompatible-types-call", "typing:inconsistent-specifier",
diff --git a/tests/misc/oracle/widen_hints.0.res.oracle b/tests/misc/oracle/widen_hints.0.res.oracle
index 582badd66f55e69c4929f48ca8051a9533ecf31c..d226c11fde7efae5b3ba45b58237b722a3ad2b62 100644
--- a/tests/misc/oracle/widen_hints.0.res.oracle
+++ b/tests/misc/oracle/widen_hints.0.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing tests/misc/widen_hints.c (with preprocessing)
-[kernel:annot-error] tests/misc/widen_hints.c:16: Warning:
+[kernel:annot-error] tests/misc/widen_hints.c:17: Warning:
invalid widen_hints annotation: no hints. Ignoring code annotation
-[kernel:annot-error] tests/misc/widen_hints.c:21: Warning:
+[kernel:annot-error] tests/misc/widen_hints.c:22: Warning:
invalid widen_hints annotation: no hints. Ignoring code annotation
-[kernel:annot-error] tests/misc/widen_hints.c:26: Warning:
+[kernel:annot-error] tests/misc/widen_hints.c:27: Warning:
unbound logic variable b. Ignoring code annotation
-[eva] tests/misc/widen_hints.c:31: User Error:
+[eva] tests/misc/widen_hints.c:32: User Error:
could not parse widening hint: not_const
If it contains variables, they must be global const integers.
[kernel] Plug-in eva aborted: invalid user input.
diff --git a/tests/misc/widen_hints.c b/tests/misc/widen_hints.c
index 0148d513d8cad7072b213dc38041fa8d3a85163e..9ef8b753ed999f1e2449368d7e853e49c06d44d6 100644
--- a/tests/misc/widen_hints.c
+++ b/tests/misc/widen_hints.c
@@ -10,6 +10,7 @@ PLUGIN: @EVA_PLUGINS@
#define N 2
const int x = 9;
int not_const = 42; // cannot be used as widen hint
+typedef struct { int i; } istruct;
#ifdef SYNTAX_ERRORS
int main1() {
@@ -31,7 +32,6 @@ int main() {
/*@ widen_hints x, not_const; */ // error: not_const not a global constant
return 0;
}
-
#else
#ifdef ALLGLOBAL
@@ -112,7 +112,7 @@ int main() {
}
}
- typedef struct { int i; } istruct;
+
istruct iarray[2] = {{0}, {0}};
istruct *piarray[2] = {&iarray[0], &iarray[1]};
for (piarray[1]->i = 0; piarray[1]->i < n*2+1; (piarray[1]->i)++) {
diff --git a/tests/syntax/oracle/type_redef.0.res.oracle b/tests/syntax/oracle/type_redef.0.res.oracle
index 6f1e0e1576382b71f1f4e57dbfc42d823c5f94c6..ef323c93743c17ad20705ae48ad3d9db2aaeb667 100644
--- a/tests/syntax/oracle/type_redef.0.res.oracle
+++ b/tests/syntax/oracle/type_redef.0.res.oracle
@@ -23,8 +23,16 @@
[kernel] tests/syntax/type_redef.i:26: User Error:
redefinition of type 'st1' in the same scope with incompatible type.
Previous declaration was at tests/syntax/type_redef.i:15
+[kernel:parser:unsupported] tests/syntax/type_redef.i:30: Warning:
+ block-level typedefs currently unsupported;
+ trying to convert it to a global-level typedef.
+ Note that this may lead to incoherent error messages.
[kernel] tests/syntax/type_redef.i:30: Failure:
redefinition of a typedef in a non-global scope is currently unsupported
+[kernel:parser:unsupported] tests/syntax/type_redef.i:31: Warning:
+ block-level typedefs currently unsupported;
+ trying to convert it to a global-level typedef.
+ Note that this may lead to incoherent error messages.
[kernel] tests/syntax/type_redef.i:31: Failure:
redefinition of a typedef in a non-global scope is currently unsupported
[kernel] tests/syntax/type_redef.i:35: User Error:
@@ -45,12 +53,28 @@
[kernel] tests/syntax/type_redef.i:49: User Error:
redefinition of type 'stt' in the same scope with incompatible type.
Previous declaration was at tests/syntax/type_redef.i:47
+[kernel:parser:unsupported] tests/syntax/type_redef.i:53: Warning:
+ block-level typedefs currently unsupported;
+ trying to convert it to a global-level typedef.
+ Note that this may lead to incoherent error messages.
[kernel] tests/syntax/type_redef.i:53: Failure:
redefinition of a typedef in a non-global scope is currently unsupported
+[kernel:parser:unsupported] tests/syntax/type_redef.i:57: Warning:
+ block-level typedefs currently unsupported;
+ trying to convert it to a global-level typedef.
+ Note that this may lead to incoherent error messages.
[kernel] tests/syntax/type_redef.i:57: Failure:
redefinition of a typedef in a non-global scope is currently unsupported
+[kernel:parser:unsupported] tests/syntax/type_redef.i:62: Warning:
+ block-level typedefs currently unsupported;
+ trying to convert it to a global-level typedef.
+ Note that this may lead to incoherent error messages.
[kernel] tests/syntax/type_redef.i:62: Failure:
redefinition of a typedef in a non-global scope is currently unsupported
+[kernel:parser:unsupported] tests/syntax/type_redef.i:63: Warning:
+ block-level typedefs currently unsupported;
+ trying to convert it to a global-level typedef.
+ Note that this may lead to incoherent error messages.
[kernel] tests/syntax/type_redef.i:63: Failure:
redefinition of a typedef in a non-global scope is currently unsupported
[kernel] User Error: stopping on file "tests/syntax/type_redef.i" that has errors.
diff --git a/tests/syntax/oracle/type_redef.1.res.oracle b/tests/syntax/oracle/type_redef.1.res.oracle
index fe3ef39fce8b3f594c45d60eaa8bf3848249345e..a42f1b878aa669134ec2a103401d5bf4fb824ab4 100644
--- a/tests/syntax/oracle/type_redef.1.res.oracle
+++ b/tests/syntax/oracle/type_redef.1.res.oracle
@@ -17,8 +17,16 @@
[kernel] tests/syntax/type_redef.i:26: User Error:
redefinition of type 'st1' in the same scope with incompatible type.
Previous declaration was at tests/syntax/type_redef.i:15
+[kernel:parser:unsupported] tests/syntax/type_redef.i:30: Warning:
+ block-level typedefs currently unsupported;
+ trying to convert it to a global-level typedef.
+ Note that this may lead to incoherent error messages.
[kernel] tests/syntax/type_redef.i:30: Failure:
redefinition of a typedef in a non-global scope is currently unsupported
+[kernel:parser:unsupported] tests/syntax/type_redef.i:31: Warning:
+ block-level typedefs currently unsupported;
+ trying to convert it to a global-level typedef.
+ Note that this may lead to incoherent error messages.
[kernel] tests/syntax/type_redef.i:31: Failure:
redefinition of a typedef in a non-global scope is currently unsupported
[kernel] tests/syntax/type_redef.i:35: User Error:
@@ -33,12 +41,28 @@
[kernel] tests/syntax/type_redef.i:49: User Error:
redefinition of type 'stt' in the same scope with incompatible type.
Previous declaration was at tests/syntax/type_redef.i:47
+[kernel:parser:unsupported] tests/syntax/type_redef.i:53: Warning:
+ block-level typedefs currently unsupported;
+ trying to convert it to a global-level typedef.
+ Note that this may lead to incoherent error messages.
[kernel] tests/syntax/type_redef.i:53: Failure:
redefinition of a typedef in a non-global scope is currently unsupported
+[kernel:parser:unsupported] tests/syntax/type_redef.i:57: Warning:
+ block-level typedefs currently unsupported;
+ trying to convert it to a global-level typedef.
+ Note that this may lead to incoherent error messages.
[kernel] tests/syntax/type_redef.i:57: Failure:
redefinition of a typedef in a non-global scope is currently unsupported
+[kernel:parser:unsupported] tests/syntax/type_redef.i:62: Warning:
+ block-level typedefs currently unsupported;
+ trying to convert it to a global-level typedef.
+ Note that this may lead to incoherent error messages.
[kernel] tests/syntax/type_redef.i:62: Failure:
redefinition of a typedef in a non-global scope is currently unsupported
+[kernel:parser:unsupported] tests/syntax/type_redef.i:63: Warning:
+ block-level typedefs currently unsupported;
+ trying to convert it to a global-level typedef.
+ Note that this may lead to incoherent error messages.
[kernel] tests/syntax/type_redef.i:63: Failure:
redefinition of a typedef in a non-global scope is currently unsupported
[kernel] User Error: stopping on file "tests/syntax/type_redef.i" that has errors.