From 178d2a7659f38ec9a9c7a3c33889bc360d9b95da Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 15 May 2020 14:58:06 +0200
Subject: [PATCH] [printer] use attribute payload to pretty-print _Noreturn
when relevant
a _noreturn attribute with c11 tag will be rendered as _Noreturn keyword
---
src/kernel_internals/parsing/cparser.mly | 3 ++-
src/kernel_services/ast_printing/cil_printer.ml | 3 +++
tests/syntax/oracle/built.res.oracle | 2 +-
3 files changed, 6 insertions(+), 2 deletions(-)
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index d58c42823f1..8613ec75b57 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 fbfc904dc2a..085144c8958 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 37b533b358f..46acc5898e7 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;
--
GitLab