diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index 7034e9cd0ea59a9fa641891ff5407ff4becf303c..a71f6f3f5a9e64ed407958e9d70d2f5227de2a86 100644 --- a/src/kernel_services/ast_printing/cil_printer.ml +++ b/src/kernel_services/ast_printing/cil_printer.ml @@ -2021,8 +2021,8 @@ class cil_printer () = object (self) printAttributes atts_elem sep self#attrparam s | [Attr("static",[]); Attr("arraylen",[s])] | [Attr("arraylen", [s]); Attr("static", [])] -> - Format.fprintf fmt "static@ %a%t%a" - printAttributes atts_elem sep self#attrparam s + Format.fprintf fmt "static%a@ %a" + printAttributes atts_elem self#attrparam s | _ -> () in let name' fmt = diff --git a/tests/syntax/oracle/array_formals.res.oracle b/tests/syntax/oracle/array_formals.res.oracle index 50a68337f1d2c4de3d0cedf94d23c47768ab9708..c0e7c9b399f0091f06acaac341530fae162719cf 100644 --- a/tests/syntax/oracle/array_formals.res.oracle +++ b/tests/syntax/oracle/array_formals.res.oracle @@ -15,7 +15,7 @@ int g(int a[static 2]) return __retres; } -int h(int a[static const restrict 2]) +int h(int a[static const restrict 2]) { int __retres; __retres = *(a + 1);