From c95c2dd3a4d6d1eb27388c98a5a2f27f232a6977 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 23 Aug 2023 12:16:10 +0200
Subject: [PATCH] Do not display ghost code in proto/fun args when empty
---
src/kernel_services/ast_printing/cprint.ml | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index 6fce5e0e850..91c72cd16cd 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -253,6 +253,9 @@ and print_decl (n: string) fmt = function
| ARRAY (d, al, e) ->
fprintf fmt "%a[@[%a%a@]]"
(print_decl n) d print_attributes al print_expression e
+ | PROTO(d, args, [], isva) ->
+ fprintf fmt "@[%a@;(%a) @]"
+ (print_decl n) d print_params (args,isva)
| PROTO(d, args, ghost_args, isva) ->
fprintf fmt "@[%a@;(%a) /*@@@ ghost (%a) */ @]"
(print_decl n) d print_params (args,isva) print_params (ghost_args, false)
@@ -380,6 +383,9 @@ and print_expression_level (lvl: int) fmt (exp : expression) =
[arg; { expr_node = TYPE_SIZEOF (bt, dt) } ], _) ->
fprintf fmt "__builtin_va_arg(@[%a,@ %a@])"
(print_expression_level 0) arg print_onlytype (bt, dt)
+ | CALL (exp, args, []) ->
+ fprintf fmt "%a(@[@;%a@])"
+ print_expression exp print_comma_exps args
| CALL (exp, args, ghost_args) ->
fprintf fmt "%a(@[@;%a@]) /*@@@ ghost (@[@;%a@]) */"
print_expression exp print_comma_exps args print_comma_exps ghost_args
--
GitLab