From 11b1d6a1421e7b80a9dd51fa7505b114f388a9d9 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 17 May 2024 13:15:11 +0200
Subject: [PATCH] [Kernel] allow _Pragma in function signature (as does GCC)
---
src/kernel_internals/parsing/cparser.mly | 12 +++++++-
.../plugin_entry_points/kernel.ml | 2 ++
.../plugin_entry_points/kernel.mli | 3 ++
tests/misc/oracle/audit-out.json | 5 ++--
.../syntax/oracle/pragma_operator.res.oracle | 30 +++++++++++++++++++
tests/syntax/pragma_operator.c | 13 ++++++++
6 files changed, 62 insertions(+), 3 deletions(-)
create mode 100644 tests/syntax/oracle/pragma_operator.res.oracle
create mode 100644 tests/syntax/pragma_operator.c
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 9da7b7b8aa9..414df24d404 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -1190,7 +1190,17 @@ decl_spec_wo_type: /* ISO 6.7 */
decl_spec_list:
| decl_spec_wo_type decl_spec_list_opt { fst $1 :: $2, snd $1 }
-| type_spec decl_spec_list_opt_no_named { SpecType(fst $1) :: $2, snd $1 }
+| type_spec pragma* (* pragma accepted by GCC *) decl_spec_list_opt_no_named
+ {
+ let pragmas = $2 in
+ if pragmas != [] then begin
+ let loc = Cabshelper.get_definitionloc (List.hd pragmas) in
+ Kernel.warning ~wkey:Kernel.wkey_parser_unsupported_pragma
+ ~once:true ~source:(fst loc)
+ "Discarding _Pragma's in function declaration"
+ end;
+ SpecType(fst $1) :: $3, snd $1
+ }
decl_spec_list_no_named:
| decl_spec_wo_type decl_spec_list_opt_no_named { fst $1 :: $2, snd $1 }
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 86bb74a82b3..d4fff3d5b98 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -223,6 +223,8 @@ let wkey_parser_unsupported = register_warn_category "parser:unsupported"
let wkey_parser_unsupported_attributes = register_warn_category "parser:unsupported:attributes"
+let wkey_parser_unsupported_pragma = register_warn_category "parser:unsupported:pragma"
+
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 940ff68224f..13e35743a12 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -220,6 +220,9 @@ val wkey_parser_unsupported: warn_category
val wkey_parser_unsupported_attributes: warn_category
(** Warning related to unsupported attributes during parsing. *)
+val wkey_parser_unsupported_pragma: warn_category
+(** Warning related to unsupported _Pragma's 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 da80b2ca653..0307758ad62 100644
--- a/tests/misc/oracle/audit-out.json
+++ b/tests/misc/oracle/audit-out.json
@@ -62,8 +62,9 @@
"linker:drop-conflicting-unused", "linker:weak", "parser",
"parser:conditional-feature", "parser:unnamed-typedef",
"parser:unsupported", "parser:unsupported:attributes",
- "plugin-not-loaded", "pp", "pp:compilation-db", "pp:line-directive",
- "too-large-array", "typing", "typing:implicit-conv-void-ptr",
+ "parser:unsupported:pragma", "plugin-not-loaded", "pp",
+ "pp:compilation-db", "pp:line-directive", "too-large-array",
+ "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/oracle/pragma_operator.res.oracle b/tests/syntax/oracle/pragma_operator.res.oracle
new file mode 100644
index 00000000000..9dfdd735b25
--- /dev/null
+++ b/tests/syntax/oracle/pragma_operator.res.oracle
@@ -0,0 +1,30 @@
+[kernel] Parsing pragma_operator.c (with preprocessing)
+[kernel:parser:unsupported:pragma] pragma_operator.c:3: Warning:
+ Discarding _Pragma's in function declaration
+[kernel:parser:unsupported:pragma] pragma_operator.c:7: Warning:
+ Discarding _Pragma's in function declaration
+[kernel:parser:unsupported:pragma] pragma_operator.c:9: Warning:
+ Discarding _Pragma's in function declaration
+[kernel:parser:unsupported:pragma] pragma_operator.c:12: Warning:
+ Discarding _Pragma's in function declaration
+/* Generated by Frama-C */
+int main(void)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+void main2(void);
+
+void main2(void)
+{
+ return;
+}
+
+void main3(void)
+{
+ return;
+}
+
+
diff --git a/tests/syntax/pragma_operator.c b/tests/syntax/pragma_operator.c
new file mode 100644
index 00000000000..93742b107c9
--- /dev/null
+++ b/tests/syntax/pragma_operator.c
@@ -0,0 +1,13 @@
+// The pragma below is allowed by GCC (14), but only on a .c file.
+// Clang (18) also accepts it on a .i file.
+int _Pragma("entrypoint") main( void) {
+ return 0;
+}
+
+void _Pragma("entrypoint") main2();
+
+void _Pragma("entrypoint") main2() {
+}
+
+void _Pragma("entrypoint") _Pragma("another pragma") _Pragma("") main3() {
+}
--
GitLab