From 1fdf63b4d52e0ba96b4711622ddd0e65c56de095 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 4 Oct 2019 16:20:45 +0200
Subject: [PATCH] [AST Printing] Sligthly changes pretty printing of arguments

---
 .../ast_printing/cil_printer.ml               | 13 ++--
 .../oracle/empty-vpar-with-ghost.res.oracle   |  5 +-
 .../oracle/function-ptr-with-ghost.res.oracle |  6 +-
 .../oracle/no-va-with-ghost.res.oracle        |  4 +-
 .../oracle/rvalues-with-ghost.res.oracle      |  4 +-
 .../oracle/simple-with-ghost.res.oracle       |  5 +-
 .../typedefed_function-with-ghost.res.oracle  |  4 +-
 tests/cil/oracle/insert_formal.res.oracle     | 26 ++++----
 .../oracle/ghost_parameters.res.oracle        | 64 +++++++++----------
 tests/spec/oracle/assigns_from_kf.res.oracle  | 16 ++---
 ...ibutes-declarations-definitions.res.oracle | 16 ++---
 .../oracle/ghost_parameters.2.res.oracle      |  6 +-
 ...ghost_parameters_formals_status.res.oracle | 10 +--
 ...host_parameters_side_effect_arg.res.oracle | 20 +++---
 .../undeclared_local_bts1126.res.oracle       |  4 +-
 15 files changed, 104 insertions(+), 99 deletions(-)

diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 3a4e9b0c11b..13259d5a56c 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -890,16 +890,17 @@ class cil_printer () = object (self)
       in
 
       (* Now the arguments *)
+      Format.fprintf fmt "@[" ;
       Pretty_utils.pp_flowlist ~left:"(" ~sep:"," ~right:")" self#exp fmt args;
       (* Now the ghost arguments *)
       begin match ghosts with
         | [] -> ()
         | _ -> Pretty_utils.pp_flowlist
-                 ~left:"/*@@ ghost (" ~sep:"," ~right:") */"
+                 ~left:"@;/*@@ ghost (" ~sep:"," ~right:") */"
                  self#exp fmt ghosts
       end ;
       (* Now the terminator *)
-      fprintf fmt "%s" instr_terminator
+      fprintf fmt "@]%s" instr_terminator
     in
     match i with
     | Skip _ -> fprintf fmt ";"
@@ -1918,7 +1919,7 @@ class cil_printer () = object (self)
           Some args, ghost_args
       in
       let pp_params fmt (args, ghost_args) pp_args =
-        fprintf fmt "%t(@[%t@])" name'
+        fprintf fmt "%t@[<hv>(@[%t@])%t@]" name'
           (fun fmt ->
              match args with
              | (None | Some []) when isvararg -> fprintf fmt "..."
@@ -1927,9 +1928,9 @@ class cil_printer () = object (self)
              | Some args ->
                Pretty_utils.pp_list ~sep:",@ " pp_args fmt args;
                if isvararg then fprintf fmt "@ , ...")
-        ;
-        Pretty_utils.pp_list ~pre:"/*@@ ghost (" ~suf:") */" ~sep:", "
-          pp_args fmt ghost_args
+          (fun fmt ->
+             Pretty_utils.pp_list ~pre:"@;/*@@ ghost (@[" ~suf:"@]) */" ~sep:",@ "
+               pp_args fmt ghost_args)
       in
       let pp_params fmt = match fundecl with
         | None ->
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
index 66bd6f7bb1c..77d342b3dd8 100644
--- a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
@@ -18,14 +18,15 @@
     behavior bhv:
       requires c > 0;
       requires a ≤ 42; */
-void f(int const a, int, int c, void * const *__va_params)/*@ ghost (int x) */;
+void f(int const a, int, int c, void * const *__va_params)
+      /*@ ghost (int x) */;
 
 int main(void)
 {
   int __retres;
   {
     void *__va_args[1] = {(void *)0};
-    f(1,2,3,(void * const *)(__va_args))/*@ ghost (4) */;
+    f(1,2,3,(void * const *)(__va_args)) /*@ ghost (4) */;
   }
   __retres = 0;
   return __retres;
diff --git a/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
index b3aa3b62aef..f81ac2a39cf 100644
--- a/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
@@ -15,7 +15,7 @@
 [eva:final-states] Values at end of function main:
   __retres ∈ {0}
 /* Generated by Frama-C */
-void function(void (*p)(int , void * const *__va_params)/*@ ghost (int v) */,
+void function(void (*p)(int , void * const *__va_params) /*@ ghost (int v) */,
               int x)
 {
   {
@@ -23,13 +23,13 @@ void function(void (*p)(int , void * const *__va_params)/*@ ghost (int v) */,
     int __va_arg1 = 2;
     int __va_arg2 = 3;
     void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
-    (*p)(x,(void * const *)(__va_args))/*@ ghost (4) */;
+    (*p)(x,(void * const *)(__va_args)) /*@ ghost (4) */;
   }
   return;
 }
 
 /*@ assigns \nothing; */
-void va_f(int, void * const *__va_params)/*@ ghost (int x) */;
+void va_f(int, void * const *__va_params) /*@ ghost (int x) */;
 
 int main(void)
 {
diff --git a/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
index 472fa003177..71fffe6ce34 100644
--- a/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
@@ -11,12 +11,12 @@
 /* Generated by Frama-C */
 /*@ assigns \result;
     assigns \result \from a, b, c; */
-int f(int a, int b, int c)/*@ ghost (int x) */;
+int f(int a, int b, int c) /*@ ghost (int x) */;
 
 int main(void)
 {
   int tmp;
-  tmp = f(1,2,3)/*@ ghost (4) */;
+  tmp = f(1,2,3) /*@ ghost (4) */;
   return tmp;
 }
 
diff --git a/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
index ce15956f751..9dde9d6d2df 100644
--- a/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
@@ -22,7 +22,7 @@
 /* Generated by Frama-C */
 /*@ assigns \result;
     assigns \result \from a; */
-int f(int a, void * const *__va_params)/*@ ghost (int x) */;
+int f(int a, void * const *__va_params) /*@ ghost (int x) */;
 
 int main(void)
 {
@@ -31,7 +31,7 @@ int main(void)
   int __va_arg1 = 4 * 5;
   int *__va_arg2 = & x;
   void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
-  int i = f(1,(void * const *)(__va_args))/*@ ghost (x + 3) */;
+  int i = f(1,(void * const *)(__va_args)) /*@ ghost (x + 3) */;
   return i;
 }
 
diff --git a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
index 3a596a240dd..fa2e63b8a11 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
@@ -21,7 +21,8 @@
       requires a ≤ 42;
       ensures \result > 0;
  */
-int f(int const a, int, int c, void * const *__va_params)/*@ ghost (int x) */;
+int f(int const a, int, int c, void * const *__va_params)
+     /*@ ghost (int x) */;
 
 int main(void)
 {
@@ -31,7 +32,7 @@ int main(void)
     int __va_arg1 = 5;
     int __va_arg2 = 6;
     void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
-    tmp = f(1,2,3,(void * const *)(__va_args))/*@ ghost (7) */;
+    tmp = f(1,2,3,(void * const *)(__va_args)) /*@ ghost (7) */;
   }
   return tmp;
 }
diff --git a/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
index 2b4685e9792..3038502c8de 100644
--- a/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
@@ -13,7 +13,7 @@
 [eva:final-states] Values at end of function main:
   __retres ∈ {0}
 /* Generated by Frama-C */
-typedef void T(int , void * const *__va_params)/*@ ghost (int ) */;
+typedef void T(int , void * const *__va_params) /*@ ghost (int ) */;
 /*@ assigns \nothing; */
 extern T f;
 
@@ -24,7 +24,7 @@ int main(void)
     int __va_arg0 = 2;
     int __va_arg1 = 0;
     void *__va_args[2] = {& __va_arg0, & __va_arg1};
-    f(1,(void * const *)(__va_args))/*@ ghost (3) */;
+    f(1,(void * const *)(__va_args)) /*@ ghost (3) */;
   }
   __retres = 0;
   return __retres;
diff --git a/tests/cil/oracle/insert_formal.res.oracle b/tests/cil/oracle/insert_formal.res.oracle
index 935880bfc24..faefb89b047 100644
--- a/tests/cil/oracle/insert_formal.res.oracle
+++ b/tests/cil/oracle/insert_formal.res.oracle
@@ -5,7 +5,7 @@ void void_circumflex(int x)
   return;
 }
 
-void void_circumflex_g(void)/*@ ghost (int x) */
+void void_circumflex_g(void) /*@ ghost (int x) */
 {
   return;
 }
@@ -15,7 +15,7 @@ void void_dollar(int x)
   return;
 }
 
-void void_dollar_g(void)/*@ ghost (int x) */
+void void_dollar_g(void) /*@ ghost (int x) */
 {
   return;
 }
@@ -30,12 +30,12 @@ void a_dollar(int a, int x)
   return;
 }
 
-void a_circumflex_g(int a)/*@ ghost (int x) */
+void a_circumflex_g(int a) /*@ ghost (int x) */
 {
   return;
 }
 
-void a_dollar_g(int a)/*@ ghost (int x) */
+void a_dollar_g(int a) /*@ ghost (int x) */
 {
   return;
 }
@@ -45,27 +45,27 @@ void a_a(int a, int x)
   return;
 }
 
-void ghost_a_circumflex(int x)/*@ ghost (int a) */
+void ghost_a_circumflex(int x) /*@ ghost (int a) */
 {
   return;
 }
 
-void ghost_a_dollar(int x)/*@ ghost (int a) */
+void ghost_a_dollar(int x) /*@ ghost (int a) */
 {
   return;
 }
 
-void ghost_a_circumflex_g(void)/*@ ghost (int x, int a) */
+void ghost_a_circumflex_g(void) /*@ ghost (int x, int a) */
 {
   return;
 }
 
-void ghost_a_dollar_g(void)/*@ ghost (int a, int x) */
+void ghost_a_dollar_g(void) /*@ ghost (int a, int x) */
 {
   return;
 }
 
-void ghost_a_a(void)/*@ ghost (int a, int x) */
+void ghost_a_a(void) /*@ ghost (int a, int x) */
 {
   return;
 }
@@ -80,22 +80,22 @@ void b_a_c_a(int b, int a, int x, int c)
   return;
 }
 
-void all_ghost_a_b_c_a(void)/*@ ghost (int a, int x, int b, int c) */
+void all_ghost_a_b_c_a(void) /*@ ghost (int a, int x, int b, int c) */
 {
   return;
 }
 
-void all_ghost_b_a_c_a(void)/*@ ghost (int b, int a, int x, int c) */
+void all_ghost_b_a_c_a(void) /*@ ghost (int b, int a, int x, int c) */
 {
   return;
 }
 
-void a_ghost_b_c_a(int a, int x)/*@ ghost (int b, int c) */
+void a_ghost_b_c_a(int a, int x) /*@ ghost (int b, int c) */
 {
   return;
 }
 
-void b_ghost_a_c_a(int b)/*@ ghost (int a, int x, int c) */
+void b_ghost_a_c_a(int b) /*@ ghost (int a, int x, int c) */
 {
   return;
 }
diff --git a/tests/pretty_printing/oracle/ghost_parameters.res.oracle b/tests/pretty_printing/oracle/ghost_parameters.res.oracle
index 62cd045464b..79cdc64d68c 100644
--- a/tests/pretty_printing/oracle/ghost_parameters.res.oracle
+++ b/tests/pretty_printing/oracle/ghost_parameters.res.oracle
@@ -7,9 +7,9 @@ void def_function_void_no_ghost(void)
   return;
 }
 
-void decl_function_void_ghost(void)/*@ ghost (int y) */;
+void decl_function_void_ghost(void) /*@ ghost (int y) */;
 
-void def_function_void_ghost(void)/*@ ghost (int y) */
+void def_function_void_ghost(void) /*@ ghost (int y) */
 {
   return;
 }
@@ -21,26 +21,26 @@ void def_function_x_no_ghost(int x)
   return;
 }
 
-void decl_function_x_ghost(int x)/*@ ghost (int y) */;
+void decl_function_x_ghost(int x) /*@ ghost (int y) */;
 
-void def_function_x_ghost(int x)/*@ ghost (int y) */
+void def_function_x_ghost(int x) /*@ ghost (int y) */
 {
   return;
 }
 
-void decl_with_fptr(void (*ptr)(int x)/*@ ghost (int y) */);
+void decl_with_fptr(void (*ptr)(int x) /*@ ghost (int y) */);
 
-void def_with_fptr(void (*ptr)(int x)/*@ ghost (int y) */)
+void def_with_fptr(void (*ptr)(int x) /*@ ghost (int y) */)
 {
-  void (*local)(int )/*@ ghost (int ) */ = ptr;
-  (*local)(4)/*@ ghost (2) */;
+  void (*local)(int ) /*@ ghost (int ) */ = ptr;
+  (*local)(4) /*@ ghost (2) */;
   /*@ ghost (*local)(4,2); */
   return;
 }
 
-void decl_variadic(int x , ...)/*@ ghost (int y) */;
+void decl_variadic(int x , ...) /*@ ghost (int y) */;
 
-void def_variadic(int x , ...)/*@ ghost (int y) */
+void def_variadic(int x , ...) /*@ ghost (int y) */
 {
   return;
 }
@@ -50,16 +50,16 @@ int main(void)
   int __retres;
   decl_function_void_no_ghost();
   def_function_void_no_ghost();
-  decl_function_void_ghost()/*@ ghost (4) */;
-  def_function_void_ghost()/*@ ghost (4) */;
+  decl_function_void_ghost() /*@ ghost (4) */;
+  def_function_void_ghost() /*@ ghost (4) */;
   decl_function_x_no_ghost(2);
   def_function_x_no_ghost(2);
-  decl_function_x_ghost(2)/*@ ghost (4) */;
-  def_function_x_ghost(2)/*@ ghost (4) */;
+  decl_function_x_ghost(2) /*@ ghost (4) */;
+  def_function_x_ghost(2) /*@ ghost (4) */;
   decl_with_fptr(& decl_function_x_ghost);
   def_with_fptr(& decl_function_x_ghost);
-  decl_variadic(2,1,2,3,4)/*@ ghost (4) */;
-  def_variadic(2,1,2,3,4)/*@ ghost (4) */;
+  decl_variadic(2,1,2,3,4) /*@ ghost (4) */;
+  def_variadic(2,1,2,3,4) /*@ ghost (4) */;
   /*@ ghost decl_function_void_no_ghost(); */
   /*@ ghost def_function_void_no_ghost(); */
   /*@ ghost decl_function_void_ghost(4); */
@@ -101,9 +101,9 @@ void def_function_void_no_ghost(void)
   return;
 }
 
-void decl_function_void_ghost(void)/*@ ghost (int y) */;
+void decl_function_void_ghost(void) /*@ ghost (int y) */;
 
-void def_function_void_ghost(void)/*@ ghost (int y) */
+void def_function_void_ghost(void) /*@ ghost (int y) */
 {
   return;
 }
@@ -115,26 +115,26 @@ void def_function_x_no_ghost(int x)
   return;
 }
 
-void decl_function_x_ghost(int x)/*@ ghost (int y) */;
+void decl_function_x_ghost(int x) /*@ ghost (int y) */;
 
-void def_function_x_ghost(int x)/*@ ghost (int y) */
+void def_function_x_ghost(int x) /*@ ghost (int y) */
 {
   return;
 }
 
-void decl_with_fptr(void (*ptr)(int x)/*@ ghost (int y) */);
+void decl_with_fptr(void (*ptr)(int x) /*@ ghost (int y) */);
 
-void def_with_fptr(void (*ptr)(int x)/*@ ghost (int y) */)
+void def_with_fptr(void (*ptr)(int x) /*@ ghost (int y) */)
 {
-  void (*local)(int )/*@ ghost (int ) */ = ptr;
-  (*local)(4)/*@ ghost (2) */;
+  void (*local)(int ) /*@ ghost (int ) */ = ptr;
+  (*local)(4) /*@ ghost (2) */;
   /*@ ghost (*local)(4,2); */
   return;
 }
 
-void decl_variadic(int x , ...)/*@ ghost (int y) */;
+void decl_variadic(int x , ...) /*@ ghost (int y) */;
 
-void def_variadic(int x , ...)/*@ ghost (int y) */
+void def_variadic(int x , ...) /*@ ghost (int y) */
 {
   return;
 }
@@ -144,16 +144,16 @@ int main(void)
   int __retres;
   decl_function_void_no_ghost();
   def_function_void_no_ghost();
-  decl_function_void_ghost()/*@ ghost (4) */;
-  def_function_void_ghost()/*@ ghost (4) */;
+  decl_function_void_ghost() /*@ ghost (4) */;
+  def_function_void_ghost() /*@ ghost (4) */;
   decl_function_x_no_ghost(2);
   def_function_x_no_ghost(2);
-  decl_function_x_ghost(2)/*@ ghost (4) */;
-  def_function_x_ghost(2)/*@ ghost (4) */;
+  decl_function_x_ghost(2) /*@ ghost (4) */;
+  def_function_x_ghost(2) /*@ ghost (4) */;
   decl_with_fptr(& decl_function_x_ghost);
   def_with_fptr(& decl_function_x_ghost);
-  decl_variadic(2,1,2,3,4)/*@ ghost (4) */;
-  def_variadic(2,1,2,3,4)/*@ ghost (4) */;
+  decl_variadic(2,1,2,3,4) /*@ ghost (4) */;
+  def_variadic(2,1,2,3,4) /*@ ghost (4) */;
   /*@ ghost decl_function_void_no_ghost(); */
   /*@ ghost def_function_void_no_ghost(); */
   /*@ ghost decl_function_void_ghost(4); */
diff --git a/tests/spec/oracle/assigns_from_kf.res.oracle b/tests/spec/oracle/assigns_from_kf.res.oracle
index 17b16f05f99..ac10b7070c2 100644
--- a/tests/spec/oracle/assigns_from_kf.res.oracle
+++ b/tests/spec/oracle/assigns_from_kf.res.oracle
@@ -29,7 +29,7 @@ void something_non_ghost(int *p);
 
 /*@ assigns *p;
     assigns *p \from *p; */
-void something_ghost(void)/*@ ghost (int *p) */;
+void something_ghost(void) /*@ ghost (int *p) */;
 
 /*@ assigns \result, *p;
     assigns \result \from *p;
@@ -40,31 +40,31 @@ int something_non_ghost_r(int *p);
     assigns \result \from \nothing;
     assigns *p \from *p;
  */
-int something_ghost_r(void)/*@ ghost (int *p) */;
+int something_ghost_r(void) /*@ ghost (int *p) */;
 
 /*@ assigns *p, *gp;
     assigns *p \from *p, x;
     assigns *gp \from *p, *gp, x, gx;
  */
-void both(int *p, int x)/*@ ghost (int *gp, int gx) */;
+void both(int *p, int x) /*@ ghost (int *gp, int gx) */;
 
 /*@ assigns \result, *p, *gp;
     assigns \result \from *p, x;
     assigns *p \from *p, x;
     assigns *gp \from *p, *gp, x, gx;
  */
-int both_r(int *p, int x)/*@ ghost (int *gp, int gx) */;
+int both_r(int *p, int x) /*@ ghost (int *gp, int gx) */;
 
 void reference(void)
 {
   nothing();
   nothing_r();
   something_non_ghost((int *)0);
-  something_ghost()/*@ ghost ((int *)0) */;
+  something_ghost() /*@ ghost ((int *)0) */;
   something_non_ghost_r((int *)0);
-  something_ghost_r()/*@ ghost ((int *)0) */;
-  both((int *)0,1)/*@ ghost ((int *)0,2) */;
-  both_r((int *)0,1)/*@ ghost ((int *)0,2) */;
+  something_ghost_r() /*@ ghost ((int *)0) */;
+  both((int *)0,1) /*@ ghost ((int *)0,2) */;
+  both_r((int *)0,1) /*@ ghost ((int *)0,2) */;
   return;
 }
 
diff --git a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
index 196ad631a7a..5d89e874ee4 100644
--- a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
+++ b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
@@ -6,18 +6,18 @@
 /* Generated by Frama-C */
 typedef int __attribute__((__a1__)) aint;
 typedef int __attribute__((__p1__)) * __attribute__((__p2__)) iptr;
-int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
-                                                       __f2__, __f1__));
+int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
+(int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
+                                                        __f2__, __f1__));
 
 /*@ requires p3 ≥ 3;
     requires p3 ≥ 1;
     requires p3 ≥ 4; */
-int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
-                                                       __f2__, __f1__));
-int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p3)
+int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
+(int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
+                                                        __f2__, __f1__));
+int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
+(int const __attribute__((__arg3__)) p3)
 {
   int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) __retres;
   __retres = (int __attribute__((__tret3__, __tret2__, __tret1__)))p3;
diff --git a/tests/syntax/oracle/ghost_parameters.2.res.oracle b/tests/syntax/oracle/ghost_parameters.2.res.oracle
index 8904f3831af..21f52b26fea 100644
--- a/tests/syntax/oracle/ghost_parameters.2.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.2.res.oracle
@@ -1,14 +1,14 @@
 [kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
 /* Generated by Frama-C */
-void function(int a, int b)/*@ ghost (int c, int d) */;
+void function(int a, int b) /*@ ghost (int c, int d) */;
 
 void caller(void)
 {
-  function(1,2)/*@ ghost (3,4) */;
+  function(1,2) /*@ ghost (3,4) */;
   return;
 }
 
-void function(int a, int b)/*@ ghost (int c, int d) */
+void function(int a, int b) /*@ ghost (int c, int d) */
 {
   return;
 }
diff --git a/tests/syntax/oracle/ghost_parameters_formals_status.res.oracle b/tests/syntax/oracle/ghost_parameters_formals_status.res.oracle
index f3e03d1e39e..f57bed37aaa 100644
--- a/tests/syntax/oracle/ghost_parameters_formals_status.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters_formals_status.res.oracle
@@ -1,23 +1,25 @@
 [kernel] Parsing tests/syntax/ghost_parameters_formals_status.i (no preprocessing)
 [kernel] Type of caller is void (void).
   No Formals
-[kernel] Type of declaration_not_void is void (int a, int b)/*@ ghost (int x, int y) */.
+[kernel] Type of declaration_not_void is void (int a, int b)
+                                       /*@ ghost (int x, int y) */.
   Formals are 
                - a which is non-ghost
                - b which is non-ghost
                - x which is ghost
                - y which is ghost
-[kernel] Type of declaration_void is void (void)/*@ ghost (int x, int y) */.
+[kernel] Type of declaration_void is void (void) /*@ ghost (int x, int y) */.
   Formals are 
                - x which is ghost
                - y which is ghost
-[kernel] Type of definition_not_void is void (int a, int b)/*@ ghost (int x, int y) */.
+[kernel] Type of definition_not_void is void (int a, int b)
+                                      /*@ ghost (int x, int y) */.
   Formals are 
                - a which is non-ghost
                - b which is non-ghost
                - x which is ghost
                - y which is ghost
-[kernel] Type of definition_void is void (void)/*@ ghost (int x, int y) */.
+[kernel] Type of definition_void is void (void) /*@ ghost (int x, int y) */.
   Formals are 
                - x which is ghost
                - y which is ghost
diff --git a/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle b/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle
index a049a30bcfb..a74ded6cea5 100644
--- a/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle
@@ -1,8 +1,8 @@
 [kernel] Parsing tests/syntax/ghost_parameters_side_effect_arg.i (no preprocessing)
 /* Generated by Frama-C */
-void function(int x)/*@ ghost (int y) */;
+void function(int x) /*@ ghost (int y) */;
 
-int other(int x)/*@ ghost (int y) */;
+int other(int x) /*@ ghost (int y) */;
 
 void caller(void)
 {
@@ -25,27 +25,27 @@ void caller(void)
   tmp = x;
   x ++;
   ;
-  function(tmp)/*@ ghost (g_tmp) */;
+  function(tmp) /*@ ghost (g_tmp) */;
   /*@ ghost g = 42; */
   x = 2;
-  function(x)/*@ ghost (g) */;
+  function(x) /*@ ghost (g) */;
   /*@ ghost g += 42; */
   x += 2;
-  function(x)/*@ ghost (g) */;
-  function(- x)/*@ ghost (- g) */;
+  function(x) /*@ ghost (g) */;
+  function(- x) /*@ ghost (- g) */;
   /*@ ghost if (g == 0) g_tmp_0 = g; else g_tmp_0 = 42; */
   if (x == 0) tmp_0 = x; else tmp_0 = 42;
-  function(tmp_0)/*@ ghost (g_tmp_0) */;
+  function(tmp_0) /*@ ghost (g_tmp_0) */;
   /*@ ghost g_tmp_1 = g; */
   /*@ ghost g ++; */
   /*@ ghost ; */
   tmp_1 = x;
   x ++;
   ;
-  function(t[tmp_1])/*@ ghost (t[g_tmp_1]) */;
+  function(t[tmp_1]) /*@ ghost (t[g_tmp_1]) */;
   /*@ ghost g_tmp_2 = other(x,g); */
-  tmp_2 = other(x)/*@ ghost (g) */;
-  function(tmp_2)/*@ ghost (g_tmp_2) */;
+  tmp_2 = other(x) /*@ ghost (g) */;
+  function(tmp_2) /*@ ghost (g_tmp_2) */;
   /*@ ghost int i = 1; */
   /*@ ghost g_tmp_3 = i;
             i ++;
diff --git a/tests/syntax/oracle/undeclared_local_bts1126.res.oracle b/tests/syntax/oracle/undeclared_local_bts1126.res.oracle
index c1237aab0ad..4c135cc183f 100644
--- a/tests/syntax/oracle/undeclared_local_bts1126.res.oracle
+++ b/tests/syntax/oracle/undeclared_local_bts1126.res.oracle
@@ -32,8 +32,8 @@ extern int ( /* missing proto */ _gnutls_epoch_get)(struct gnutls_session_t x_0,
 
 extern int ( /* missing proto */ gnutls_assert_val)(int x_0);
 
-extern int ( /* missing proto */ _gnutls_cipher_suite_get_cipher_algo)(
-cipher_suite_st *x_0);
+extern int ( /* missing proto */ _gnutls_cipher_suite_get_cipher_algo)
+(cipher_suite_st *x_0);
 
 extern int ( /* missing proto */ _gnutls_cipher_suite_get_mac_algo)(cipher_suite_st *x_0);
 
-- 
GitLab