From e2f4100259e06614c50ccd5daa2210d09556b781 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 15 Apr 2021 11:05:19 +0200
Subject: [PATCH] [printer] avoid double space when pretty-printing array
attributes
---
src/kernel_services/ast_printing/cil_printer.ml | 4 ++--
tests/syntax/oracle/array_formals.res.oracle | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 7034e9cd0ea..a71f6f3f5a9 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 50a68337f1d..c0e7c9b399f 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);
--
GitLab