diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 8ca38fc5074160939c7b5a83a1ec2ce56d50cbc6..1e7de52f4090674e95c265a7522f11992713d8a6 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 0000000000000000000000000000000000000000..2e5096c4b3091c7369b6c1d7677007b06d90fcd0 --- /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 0000000000000000000000000000000000000000..f89bf9de36a17fa44cff873ec8fca27a4beb781a --- /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; +} + +