From 6e8d42a29ee2e21b474c1cfd600b8aa79f25c649 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 30 Mar 2021 15:39:38 +0200
Subject: [PATCH] [printer] correctly print array info for formals turned into
pointers
---
.../ast_printing/cil_printer.ml | 21 ++++++++++++++++++-
tests/syntax/array_formals.i | 3 +++
tests/syntax/oracle/array_formals.res.oracle | 17 +++++++++++++++
3 files changed, 40 insertions(+), 1 deletion(-)
create mode 100644 tests/syntax/array_formals.i
create mode 100644 tests/syntax/oracle/array_formals.res.oracle
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index a98a8021d4d..82f3d1d0f06 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -720,6 +720,12 @@ class cil_printer () = object (self)
let stom, rest = Cil.separateStorageModifiers v.vattr 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 =
+ match v.vtype with
+ | TPtr(t,a) when Cil.hasAttribute "arraylen" a ->
+ { v with vtype = TArray(t, None, { scache = Not_Computed }, a)}
+ | _ -> v
+ in
(* First the storage modifiers *)
fprintf fmt "%s%a%a%s%a%a"
(if v.vinline then "__inline " else "")
@@ -2000,6 +2006,19 @@ class cil_printer () = object (self)
Kernel.failure ~current:true
"Found some incorrect attributes for array (%a). Please report."
self#attributes atts_elem;
+ let size_info,a =
+ List.partition
+ (fun a -> List.mem (Cil.attributeName a) ["arraylen"; "static"]) a
+ in
+ let print_size_info fmt =
+ match size_info with
+ | [] -> ()
+ | [Attr("arraylen",[s])]-> self#attrparam fmt s
+ | [Attr("static",[]); Attr("arraylen",[s])]
+ | [Attr("arraylen", [s]); Attr("static", [])] ->
+ Format.fprintf fmt "static@ %a" self#attrparam s
+ | _ -> ()
+ in
let name' fmt =
if a = [] then pname fmt false
else if nameOpt = None then
@@ -2013,7 +2032,7 @@ class cil_printer () = object (self)
name'
(fun fmt ->
match lo with
- | None -> ()
+ | None -> print_size_info fmt
| Some e -> self#exp fmt e)
))
fmt
diff --git a/tests/syntax/array_formals.i b/tests/syntax/array_formals.i
new file mode 100644
index 00000000000..85ccba1b29f
--- /dev/null
+++ b/tests/syntax/array_formals.i
@@ -0,0 +1,3 @@
+int f(int a[2]) { return a[1]; }
+
+int g(int a[static 2]) { return a[1]; }
diff --git a/tests/syntax/oracle/array_formals.res.oracle b/tests/syntax/oracle/array_formals.res.oracle
new file mode 100644
index 00000000000..9335e5eff04
--- /dev/null
+++ b/tests/syntax/oracle/array_formals.res.oracle
@@ -0,0 +1,17 @@
+[kernel] Parsing tests/syntax/array_formals.i (no preprocessing)
+/* Generated by Frama-C */
+int f(int a[2])
+{
+ int __retres;
+ __retres = *(a + 1);
+ return __retres;
+}
+
+int g(int a[static 2])
+{
+ int __retres;
+ __retres = *(a + 1);
+ return __retres;
+}
+
+
--
GitLab