diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index a98a8021d4d29a6ad15946a930dd330743cd8802..82f3d1d0f06733038fde09914c47ac9d2ea069d7 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 0000000000000000000000000000000000000000..85ccba1b29fa8dae755ab965f391a5f7195ddd14
--- /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 0000000000000000000000000000000000000000..9335e5eff0420f9eac5aded501db77912a66d491
--- /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;
+}
+
+