From 5e7e4e4d19a3242c84a19b49ccee3d23427ecfbf Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 19 Sep 2024 15:19:35 +0200
Subject: [PATCH] [tests] Add a test for statement attributes
---
.../oracle/stmt_attributes.0.res.oracle | 9 +++++++++
.../oracle/stmt_attributes.1.res.oracle | 11 +++++++++++
tests/syntax/stmt_attributes.c | 19 +++++++++++++++++++
3 files changed, 39 insertions(+)
create mode 100644 tests/syntax/oracle/stmt_attributes.0.res.oracle
create mode 100644 tests/syntax/oracle/stmt_attributes.1.res.oracle
create mode 100644 tests/syntax/stmt_attributes.c
diff --git a/tests/syntax/oracle/stmt_attributes.0.res.oracle b/tests/syntax/oracle/stmt_attributes.0.res.oracle
new file mode 100644
index 0000000000..332ba0700a
--- /dev/null
+++ b/tests/syntax/oracle/stmt_attributes.0.res.oracle
@@ -0,0 +1,9 @@
+[kernel] Parsing stmt_attributes.c (with preprocessing)
+/* Generated by Frama-C */
+void f(void)
+{
+ foo: ;
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/stmt_attributes.1.res.oracle b/tests/syntax/oracle/stmt_attributes.1.res.oracle
new file mode 100644
index 0000000000..14c9766474
--- /dev/null
+++ b/tests/syntax/oracle/stmt_attributes.1.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing stmt_attributes.c (with preprocessing)
+[kernel] stmt_attributes.c:17:
+ syntax error:
+ Location: line 17, column 30, before or at token: ;
+ 15 attributes specifiers, which is forbidden, so a syntax error is raised.
+ 16 Statement attributes are not supported in frama-c except for labels. */
+ 17 __attribute__((fallthrough));
+ ^
+ 18 #endif
+ 19 }
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/stmt_attributes.c b/tests/syntax/stmt_attributes.c
new file mode 100644
index 0000000000..8b2e6ba682
--- /dev/null
+++ b/tests/syntax/stmt_attributes.c
@@ -0,0 +1,19 @@
+/* run.config
+ STDOPT:
+ EXIT: 1
+ STDOPT: #"-cpp-extra-args=-DNO_SPECIFIERS"
+*/
+
+void f() {
+
+ /* Label attributes are accepted in Frama-C's parser, but dumped when building
+ Cabs. */
+ foo: __attribute__((unused));
+
+ #ifdef NO_SPECIFIERS
+ /* Parser detect this as a declaration without any specifiers except for GCC's
+ attributes specifiers, which is forbidden, so a syntax error is raised.
+ Statement attributes are not supported in frama-c except for labels. */
+ __attribute__((fallthrough));
+ #endif
+}
--
GitLab