From 5e6dbe9b51c23367fca140e9a6be5f5ec0bfdf24 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 5 Oct 2021 12:37:24 +0200
Subject: [PATCH] [Cabs2cil] warn about local typedefs
---
src/kernel_internals/typing/cabs2cil.ml | 6 +++++
.../plugin_entry_points/kernel.ml | 2 ++
.../plugin_entry_points/kernel.mli | 3 +++
.../variadic/tests/known/printf_wrong_types.c | 4 ++--
tests/misc/oracle/audit-out.json | 4 ++--
tests/misc/oracle/widen_hints.0.res.oracle | 8 +++----
tests/misc/widen_hints.c | 4 ++--
tests/syntax/oracle/type_redef.0.res.oracle | 24 +++++++++++++++++++
tests/syntax/oracle/type_redef.1.res.oracle | 24 +++++++++++++++++++
9 files changed, 69 insertions(+), 10 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 604f00ef016..e8af906672d 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 657cd6c1e46..dffe3cb4b69 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 59dc0c0e978..8a935ac016f 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 85cfc9279a4..b2d5c3da606 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 e66c217886a..50dc8171330 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 582badd66f5..d226c11fde7 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 0148d513d8c..9ef8b753ed9 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 6f1e0e15763..ef323c93743 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 fe3ef39fce8..a42f1b878aa 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.
--
GitLab