diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 5151bcf30304ea2c28fecedb5796436f31c4abfb..6203cf3fa2fd022818193a35286962091e3eb32f 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5258,7 +5258,7 @@ and doType (ghost:bool) isFuncArg
        * our life a lot, and is what the standard requires. *)
       let turnArrayIntoPointer (bt: typ)
           (lo: exp option) (a: attributes) : typ =
-        let _real_a = dropAttribute "static" a in
+        let main_attrs = dropAttribute "static" a in
         let a' : attributes =
           match lo with
           | None -> []
@@ -5280,7 +5280,8 @@ and doType (ghost:bool) isFuncArg
                 end
             end
         in
-        TPtr(bt, a')
+        let attrs = Cil.addAttributes a' main_attrs in
+        TPtr(bt, attrs)
       in
       let rec fixupArgumentTypes (argidx: int) (args: varinfo list) : unit =
         match args with
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index f6a412f5b7d6b017c4b3ef0bb4ec972fc1cfc407..c394fa6c19e442ab15341a8fe5dc76d8b7268969 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2001,25 +2001,28 @@ class cil_printer () = object (self)
       self#typ (Some name'') fmt bt'
 
     | TArray (elemt, lo, _, a) ->
-      (* qualifiers attributes are not supposed to be on the TArray,
-         but on the base type. (Besides, GCC and Clang do not parse the
-         result if the qualifier is misplaced. *)
       let atts_elem, a = Cil.splitArrayAttributes a in
-      if atts_elem != [] then
-        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
+      (* qualifiers attributes are not supposed to be on the TArray,
+         but on the base type, except in the case of a formal declaration. *)
+      if atts_elem <> [] && size_info = [] then
+        Kernel.failure ~current:true
+          "Found some incorrect attributes for array (%a). Please report."
+          self#attributes atts_elem;
+      let sep fmt = if atts_elem <> [] then Format.pp_print_space fmt () in
       let print_size_info fmt =
         match size_info with
-        | [] -> ()
-        | [Attr("arraylen",[s])]-> self#attrparam fmt s
+        | [] -> printAttributes fmt a
+        | [Attr("arraylen",[s])]->
+          Format.fprintf fmt "%a%t%a"
+            printAttributes atts_elem sep self#attrparam s
         | [Attr("static",[]); Attr("arraylen",[s])]
         | [Attr("arraylen", [s]); Attr("static", [])] ->
-          Format.fprintf fmt "static@ %a" self#attrparam s
+          Format.fprintf fmt "static@ %a%t%a"
+            printAttributes atts_elem sep self#attrparam s
         | _ -> ()
       in
       let name' fmt =
diff --git a/tests/syntax/array_formals.i b/tests/syntax/array_formals.i
index 85ccba1b29fa8dae755ab965f391a5f7195ddd14..b9ad0f367832c6923c3314206598d3af2cfed58c 100644
--- a/tests/syntax/array_formals.i
+++ b/tests/syntax/array_formals.i
@@ -1,3 +1,5 @@
 int f(int a[2]) { return a[1]; }
 
 int g(int a[static 2]) { return a[1]; }
+
+int h(int a[static restrict const 2]) { return a[1]; }
diff --git a/tests/syntax/oracle/array_formals.res.oracle b/tests/syntax/oracle/array_formals.res.oracle
index 9335e5eff0420f9eac5aded501db77912a66d491..2adb96516469ff5479c3a32b2d84367b3e291939 100644
--- a/tests/syntax/oracle/array_formals.res.oracle
+++ b/tests/syntax/oracle/array_formals.res.oracle
@@ -14,4 +14,11 @@ int g(int a[static 2])
   return __retres;
 }
 
+int h(int a[static  const restrict 2])
+{
+  int __retres;
+  __retres = *(a + 1);
+  return __retres;
+}
+