From b13a07aa9430e90ce957394e9083a7d6758ae14c Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 30 Mar 2021 15:46:00 +0200
Subject: [PATCH] [printer] honor print_cil_as_is flag for array formals
---
src/kernel_services/ast_printing/cil_printer.ml | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 82f3d1d0f06..65a709f093f 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -721,10 +721,12 @@ class cil_printer () = object (self)
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 =
- match v.vtype with
- | TPtr(t,a) when Cil.hasAttribute "arraylen" a ->
- { v with vtype = TArray(t, None, { scache = Not_Computed }, a)}
- | _ -> v
+ if state.print_cil_as_is then v else begin
+ match v.vtype with
+ | TPtr(t,a) when Cil.hasAttribute "arraylen" a ->
+ { v with vtype = TArray(t, None, { scache = Not_Computed }, a)}
+ | _ -> v
+ end
in
(* First the storage modifiers *)
fprintf fmt "%s%a%a%s%a%a"
--
GitLab