From 270ad686f2427d0c097fa9af97b844f9ff53da87 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 1 Aug 2024 10:56:28 +0200
Subject: [PATCH] [printer] Print noreturn attribute before fun type
---
src/kernel_services/ast_printing/cil_printer.ml | 3 ---
1 file changed, 3 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index b71187408a..31ead251db 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2237,9 +2237,6 @@ 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' =
--
GitLab