Do not display ghost code in proto/fun args when empty

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