diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index d58c42823f1bd91a8345b13c5d21f2e7df3de59b..8613ec75b579545f53ec9600e5e5514081b87ae4 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -1116,7 +1116,8 @@ decl_spec_wo_type:                         /* ISO 6.7 */
 |   REGISTER         { SpecStorage REGISTER, $1}
                                         /* ISO 6.7.4 */
 |   INLINE           { SpecInline, $1 }
-|   NORETURN         { SpecAttr (("noreturn",[])), $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/tests/syntax/oracle/built.res.oracle b/tests/syntax/oracle/built.res.oracle
index 37b533b358f28b7893a6be131ff396d13890af87..46acc5898e7b0b42e0ce3ed4560f3acf977ab98e 100644
--- a/tests/syntax/oracle/built.res.oracle
+++ b/tests/syntax/oracle/built.res.oracle
@@ -2,7 +2,7 @@
 [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  __attribute__((__noreturn__)) int dummy_f__fc_inline(void);
+__inline static  _Noreturn int dummy_f__fc_inline(void);
 __inline static int dummy_f__fc_inline(void)
 {
   int __retres;