From 13c7d4ab4039ce814d3d708e7e2de53d85bce631 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 1 Aug 2024 16:32:06 +0200
Subject: [PATCH] [printer] Print noreturn attribute before function type
---
src/kernel_services/ast_printing/cil_printer.ml | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 6038cc494b..b71187408a 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -722,8 +722,12 @@ class cil_printer () = object (self)
(* variable declaration *)
method vdecl fmt (v:varinfo) =
let stom, rest = Cil.separateStorageModifiers v.vattr in
+ (* Small hack to keep printing noreturn attribute before function type. *)
+ let noreturn_attrs = Cil.(filterAttributes "noreturn" (typeAttr v.vtype)) in
+ let stom_noreturn = stom @ noreturn_attrs in
+ let vtype_no_noreturn = Cil.typeRemoveAttributes ["noreturn"] v.vtype in
let fundecl = if Cil.isFunctionType v.vtype then Some v else None in
- let v = { v with vtype = self#no_ghost_at_first_level v.vtype } in
+ let v = { v with vtype = self#no_ghost_at_first_level vtype_no_noreturn } in
let v =
if v.vformal && not state.print_cil_as_is then begin
match v.vtype with
@@ -744,8 +748,8 @@ class cil_printer () = object (self)
fprintf fmt "%s%a%a%s%a%a"
(if v.vinline then "__inline " else "")
self#storage v.vstorage
- self#attributes stom
- (if stom = [] then "" else " ")
+ self#attributes stom_noreturn
+ (if stom_noreturn = [] then "" else " ")
(self#typ ?fundecl name) v.vtype
self#attributes rest
--
GitLab