From 89d2228eb3947f4da96aa358207ad2e3409191bf Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 3 Jan 2025 16:42:11 +0100
Subject: [PATCH] [Kernel] ignore unsupported attributes to avoid warnings
---
src/kernel_internals/typing/cabs2cil.ml | 12 +++-
tests/syntax/attributes-exotic.i | 46 +++++++++++++++
.../oracle/attributes-exotic.res.oracle | 58 +++++++++++++++++++
3 files changed, 115 insertions(+), 1 deletion(-)
create mode 100644 tests/syntax/attributes-exotic.i
create mode 100644 tests/syntax/oracle/attributes-exotic.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 8ca38fc507..1e7de52f40 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -161,7 +161,17 @@ let () =
Cil.registerAttribute "FC_OLDSTYLEPROTO" (AttrName false);
Cil.registerAttribute "static" (AttrName false);
Cil.registerAttribute "missingproto" (AttrName false);
- Cil.registerAttribute "dummy" AttrIgnored
+ Cil.registerAttribute "dummy" AttrIgnored;
+ Cil.registerAttribute "signal" AttrIgnored; (* AVR-specific attribute *)
+ Cil.registerAttribute "leaf" AttrIgnored;
+ Cil.registerAttribute "nonnull" AttrIgnored;
+ Cil.registerAttribute "deprecated" AttrIgnored;
+ Cil.registerAttribute "access" AttrIgnored;
+ Cil.registerAttribute "returns_twice" AttrIgnored;
+ Cil.registerAttribute "pure" AttrIgnored;
+ Cil.registerAttribute "cleanup" AttrIgnored;
+ Cil.registerAttribute "warning" AttrIgnored;
+ ()
(** A hook into the code that creates temporary local vars. By default this
is the identity function, but you can overwrite it if you need to change the
diff --git a/tests/syntax/attributes-exotic.i b/tests/syntax/attributes-exotic.i
new file mode 100644
index 0000000000..2e5096c4b3
--- /dev/null
+++ b/tests/syntax/attributes-exotic.i
@@ -0,0 +1,46 @@
+/* run.config*
+ COMMENT: see below
+ STDOPT:
+*/
+
+/* This test contains attributes that may appear in glibc, musl, case studies,
+ etc. Most of these can be safely ignored by Frama-C (e.g. they provide
+ hints to the compiler). Plug-ins such as E-ACSL may need to include such
+ files and thus we want to avoid unnecessary warnings.
+ This file should be periodically updated to follow libc/case study changes.
+ Update hints:
+ - copy function signatures directly, to more closely match what is found
+ in the wild;
+ - rename libc functions, to avoid conflicts with reserved identifiers;
+ - include a reference to the source.
+*/
+
+// from glibc
+extern int libc_remove (const char *__filename)
+ __attribute__ ((__nothrow__ , __leaf__)) { return 0; }
+
+// from glibc
+extern int libc_fclose (int *__stream) __attribute__ ((__nonnull__ (1)))
+ { return 0; }
+
+// from glibc
+extern int __sigsetjmp_cancel (void *__env[1], int __savemask)
+ __asm__ ("" "__sigsetjmp") __attribute__ ((__nothrow__))
+ __attribute__ ((__returns_twice__)) { return 0; }
+
+// from gmp
+extern int mpz_fits_sint_p (void *) __attribute__ ((__pure__)) { return 0; }
+
+// from papabench (AVR-specific)
+void signame (void) __attribute__ ((signal)) {}
+
+// from curl
+void
+__attribute__((__warning__("curl_easy_setopt expects a long argument")))
+__attribute__((__unused__))
+__attribute__((__noinline__)) _curl_easy_setopt_err (void) {}
+
+void body(void) {
+ // from 8cc
+ int save_hook __attribute__((unused, cleanup(pop_function)));
+}
diff --git a/tests/syntax/oracle/attributes-exotic.res.oracle b/tests/syntax/oracle/attributes-exotic.res.oracle
new file mode 100644
index 0000000000..f89bf9de36
--- /dev/null
+++ b/tests/syntax/oracle/attributes-exotic.res.oracle
@@ -0,0 +1,58 @@
+[kernel] Parsing attributes-exotic.i (no preprocessing)
+/* Generated by Frama-C */
+extern __attribute__((__nothrow__)) int libc_remove(char const *__filename) __attribute__((
+__leaf__));
+extern int libc_remove(char const *__filename)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+extern int libc_fclose(int *__stream) __attribute__((__nonnull__(1)));
+extern int libc_fclose(int *__stream)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+extern __attribute__((__nothrow__)) int __sigsetjmp_cancel(void *__env[1],
+ int __savemask) __asm__("__sigsetjmp") __attribute__((
+__returns_twice__));
+extern int __sigsetjmp_cancel(void *__env[1], int __savemask)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+extern int mpz_fits_sint_p(void *) __attribute__((__pure__));
+extern int mpz_fits_sint_p(void *)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+void signame(void) __attribute__((__signal__));
+void signame(void)
+{
+ return;
+}
+
+void __attribute__((__warning__("curl_easy_setopt expects a long argument"))) ( __attribute__((
+__noinline__)) _curl_easy_setopt_err)(void) __attribute__((__unused__));
+void __attribute__((__warning__("curl_easy_setopt expects a long argument"))) ( __attribute__((
+__noinline__)) _curl_easy_setopt_err)(void)
+{
+ return;
+}
+
+void body(void)
+{
+ int save_hook __attribute__((__unused__, __cleanup__(pop_function)));
+ return;
+}
+
+
--
GitLab