From 0e0d9c63c8ce854359e9024a002f2d6d82b9fd8a Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 6 Feb 2024 15:00:19 +0100
Subject: [PATCH] [Kernel] allow parsing of enums with attributes
This syntax is authorized by GCC/Clang and used in some libraries, such as
glib.
For now, we simply discard these attributes with a warning, since the examples
found so far are currently useless for Frama-C (e.g. 'deprecated').
---
src/kernel_internals/parsing/cparser.mly | 18 ++++++++++++++++++
.../plugin_entry_points/kernel.ml | 2 ++
.../plugin_entry_points/kernel.mli | 3 +++
tests/misc/oracle/audit-out.json | 5 +++--
tests/syntax/enum-attr-init.i | 10 ++++++++++
tests/syntax/oracle/enum-attr-init.res.oracle | 12 ++++++++++++
6 files changed, 48 insertions(+), 2 deletions(-)
create mode 100644 tests/syntax/enum-attr-init.i
create mode 100644 tests/syntax/oracle/enum-attr-init.res.oracle
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 2e54507bbb0..a023f02eea1 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -1296,9 +1296,27 @@ enumerator:
let loc = Cil_datatype.Location.of_lexing_loc $sloc in
($1, { expr_node = NOTHING; expr_loc = loc }, loc)
}
+| IDENT just_attributes {
+ let attrs = $2 in
+ let loc = Cil_datatype.Location.of_lexing_loc $sloc in
+ Kernel.warning ~wkey:Kernel.wkey_parser_unsupported_attributes
+ ~source:(fst loc)
+ "Discarding attributes in enumerator (unsupported feature): %a"
+ Cprint.print_attributes attrs;
+ ($1, { expr_node = NOTHING; expr_loc = loc }, loc)
+ }
| IDENT EQ expression {
($1, $3, Cil_datatype.Location.of_lexing_loc $sloc)
}
+| IDENT just_attributes EQ expression {
+ let attrs = $2 in
+ let loc = Cil_datatype.Location.of_lexing_loc $sloc in
+ Kernel.warning ~wkey:Kernel.wkey_parser_unsupported_attributes
+ ~source:(fst loc)
+ "Discarding attributes in enumerator (unsupported feature): %a"
+ Cprint.print_attributes attrs;
+ ($1, $4, loc)
+ }
;
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 033d10711ad..601957368df 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -210,6 +210,8 @@ let () = set_warn_status wkey_audit Log.Werror
let wkey_parser_unsupported = register_warn_category "parser:unsupported"
+let wkey_parser_unsupported_attributes = register_warn_category "parser:unsupported:attributes"
+
let wkey_asm = register_warn_category "asm:clobber"
let wkey_unnamed_typedef = register_warn_category "parser:unnamed-typedef"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 0137185ebb1..e069534e695 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -203,6 +203,9 @@ val wkey_audit: warn_category
val wkey_parser_unsupported: warn_category
(** Warning related to unsupported parsing-related features. *)
+val wkey_parser_unsupported_attributes: warn_category
+(** Warning related to unsupported attributes during parsing. *)
+
val wkey_asm: warn_category
(** Warnings related to assembly code. *)
diff --git a/tests/misc/oracle/audit-out.json b/tests/misc/oracle/audit-out.json
index 8713ec73990..0b62d732f05 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -61,8 +61,9 @@
"ghost:bad-use", "inline", "linker",
"linker:drop-conflicting-unused", "parser",
"parser:conditional-feature", "parser:unnamed-typedef",
- "parser:unsupported", "pp", "pp:compilation-db", "pp:line-directive",
- "typing", "typing:implicit-conv-void-ptr",
+ "parser:unsupported", "parser:unsupported:attributes", "pp",
+ "pp:compilation-db", "pp:line-directive", "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/syntax/enum-attr-init.i b/tests/syntax/enum-attr-init.i
new file mode 100644
index 00000000000..ada94efeba0
--- /dev/null
+++ b/tests/syntax/enum-attr-init.i
@@ -0,0 +1,10 @@
+//excerpt based on glib's gregex.h
+typedef enum {
+ G_REGEX_BSR_ANYCRLF = 1 << 23,
+ G_REGEX_JAVASCRIPT_COMPAT __attribute__((deprecated)) = 1 << 25
+} GRegexCompileFlags;
+
+enum enum2 {
+ FALSE __attribute__((false)),
+ TRUE __attribute__((true))
+};
diff --git a/tests/syntax/oracle/enum-attr-init.res.oracle b/tests/syntax/oracle/enum-attr-init.res.oracle
new file mode 100644
index 00000000000..b74990576c2
--- /dev/null
+++ b/tests/syntax/oracle/enum-attr-init.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing enum-attr-init.i (no preprocessing)
+[kernel:parser:unsupported:attributes] enum-attr-init.i:4: Warning:
+ Discarding attributes in enumerator (unsupported feature):
+ __attribute__((deprecated))
+[kernel:parser:unsupported:attributes] enum-attr-init.i:8: Warning:
+ Discarding attributes in enumerator (unsupported feature):
+ __attribute__((false))
+[kernel:parser:unsupported:attributes] enum-attr-init.i:9: Warning:
+ Discarding attributes in enumerator (unsupported feature):
+ __attribute__((true))
+/* Generated by Frama-C */
+
--
GitLab