diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll index 5d83bbc63c40b026f08077b505cf31ccab06d6f3..de31b52c9d6179cdb2d7fb033b4f3a3785654807 100644 --- a/src/kernel_internals/parsing/clexer.mll +++ b/src/kernel_internals/parsing/clexer.mll @@ -139,11 +139,28 @@ let init_lexicon _ = ("__inline__", fun loc -> INLINE loc); ("inline", fun loc -> INLINE loc); ("__inline", fun loc -> INLINE loc); - ("_inline", fun loc -> - if !Cprint.msvcMode then - INLINE loc - else - IDENT ("_inline")); + ("_inline", + fun loc -> + if !Cprint.msvcMode then + INLINE loc + else begin + Kernel.( + warning + ~wkey:wkey_conditional_feature + "_inline is a MSVC keyword, \ + use a msvc-specific machdep to enable it"); + IDENT ("_inline") + end); + ("_Noreturn", + fun loc -> + if Kernel.C11.get () then NORETURN loc + else begin + Kernel.( + warning + ~wkey:wkey_conditional_feature + "_Noreturn is a C11 keyword, use -c11 option to enable it"); + IDENT "_Noreturn" + end); ("__attribute__", fun loc -> ATTRIBUTE loc); ("__attribute", fun loc -> ATTRIBUTE loc); ("__blockattribute__", fun _ -> BLOCKATTRIBUTE); diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly index 6f2547db91ff1ebf4e193024ad1158e06428e887..8613ec75b579545f53ec9600e5e5514081b87ae4 100644 --- a/src/kernel_internals/parsing/cparser.mly +++ b/src/kernel_internals/parsing/cparser.mly @@ -367,7 +367,7 @@ let in_ghost_block ?(battrs=[]) l = %token<Cabs.cabsloc> IF TRY EXCEPT FINALLY %token ELSE -%token<Cabs.cabsloc> ATTRIBUTE INLINE ASM TYPEOF FUNCTION__ PRETTY_FUNCTION__ +%token<Cabs.cabsloc> ATTRIBUTE INLINE NORETURN ASM TYPEOF FUNCTION__ PRETTY_FUNCTION__ %token LABEL__ %token<Cabs.cabsloc> BUILTIN_VA_ARG %token BLOCKATTRIBUTE @@ -1116,6 +1116,8 @@ decl_spec_wo_type: /* ISO 6.7 */ | REGISTER { SpecStorage REGISTER, $1} /* ISO 6.7.4 */ | INLINE { SpecInline, $1 } +| NORETURN { SpecAttr + (("noreturn",[make_expr (VARIABLE "c11")])), $1 } | cvspec { $1 } | attribute_nocv { SpecAttr (fst $1), snd $1 } ; diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index fbfc904dc2a8963412e321eaa01982d36048325e..085144c8958e90e32ddf4d935a75bc010c1dd2f3 100644 --- a/src/kernel_services/ast_printing/cil_printer.ml +++ b/src/kernel_services/ast_printing/cil_printer.ml @@ -2115,6 +2115,9 @@ class cil_printer () = object (self) not state.print_cil_as_is && not (Kernel.is_debug_key_enabled Kernel.dkey_print_bitfields) -> false + | "noreturn", [ ACons ("c11",[]) ] + when not state.print_cil_as_is -> + fprintf fmt "_Noreturn"; false | _ -> (* This is the default case *) (* Add underscores to the name *) let an' = diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 41bde48cfc510df064794f528fca305d8401fee9..34b768c639c58304f241386fab6ded359df90534 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -142,6 +142,9 @@ let () = set_warn_status wkey_ghost_bad_use Log.Werror let wkey_acsl_float_compare = register_warn_category "acsl-float-compare" let () = set_warn_status wkey_acsl_float_compare Log.Winactive +let wkey_conditional_feature = + register_warn_category "parser:conditional-feature" + let wkey_drop_unused = register_warn_category "linker:drop-conflicting-unused" let wkey_implicit_conv_void_ptr = diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli index b641349af400fa143333b0491f449b498b1b5b0a..d887e0b363270a01a5e2eb2daf754cc9f4c54f95 100644 --- a/src/kernel_services/plugin_entry_points/kernel.mli +++ b/src/kernel_services/plugin_entry_points/kernel.mli @@ -141,6 +141,10 @@ val wkey_ghost_bad_use: warn_category val wkey_acsl_float_compare: warn_category +val wkey_conditional_feature: warn_category +(** parsing feature that is only supported in specific modes + (e.g. C11, gcc, ...). *) + val wkey_drop_unused: warn_category val wkey_implicit_conv_void_ptr: warn_category diff --git a/tests/syntax/built.i b/tests/syntax/built.i index 28f1ee5b7dcfa6b7da378ef24face8d449f1f6b1..f8eaf83db71b1b5316eb2bb25fbb199afe1c1e5c 100644 --- a/tests/syntax/built.i +++ b/tests/syntax/built.i @@ -1,10 +1,10 @@ /* run.config -STDOPT: +"-machdep gcc_x86_32" +STDOPT: +"-machdep gcc_x86_32 -c11" */ extern __attribute__((const, noreturn)) int ____ilog2_NaN(void); - +_Noreturn inline dummy_f(void) { while(1); } static inline __attribute__((no_instrument_function)) __attribute__((const)) int __ilog2_u32(int n); diff --git a/tests/syntax/oracle/built.res.oracle b/tests/syntax/oracle/built.res.oracle index 72f4c4a20b4e73347cdbdbe973ee2311ce97cd72..46acc5898e7b0b42e0ce3ed4560f3acf977ab98e 100644 --- a/tests/syntax/oracle/built.res.oracle +++ b/tests/syntax/oracle/built.res.oracle @@ -2,6 +2,14 @@ [kernel] tests/syntax/built.i:21: Case label -1 exceeds range of unsigned int for switch expression. Nothing to worry. /* Generated by Frama-C */ +__inline static _Noreturn int dummy_f__fc_inline(void); +__inline static int dummy_f__fc_inline(void) +{ + int __retres; + while (1) ; + return __retres; +} + char ___assert_task_state[1 - 2 * ! (! 0)]; int X; void main(int z)