[AST Printing] Adds a test for pretty-printing of ghost parameters

tests/pretty_printing/ghost_parameters.c

+void decl_function_void_no_ghost(void);
+void def_function_void_no_ghost(void) {}
+void decl_function_void_ghost(void) /*@ ghost (int y) */;
+void def_function_void_ghost(void) /*@ ghost (int y) */ {}
+void decl_function_x_no_ghost(int x);
+void def_function_x_no_ghost(int x) {}
+void decl_function_x_ghost(int x) /*@ ghost (int y) */;
+void def_function_x_ghost(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 (*local)(int) /*@ ghost (int) */ = ptr;
+
+  (*local)(4) /*@ ghost(2) */;
+  //@ ghost (*local) (4, 2) ;
+}
+void decl_variadic(int x, ...) /*@ ghost(int y) */;
+void def_variadic(int x, ...) /*@ ghost(int y) */ {}
+
+int main(void) {
+  decl_function_void_no_ghost();
+  def_function_void_no_ghost();
+  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_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) */;
+
+  /*@ ghost
+    decl_function_void_no_ghost();
+    def_function_void_no_ghost();
+    decl_function_void_ghost(4);
+    def_function_void_ghost(4);
+    decl_function_x_no_ghost(2);
+    def_function_x_no_ghost(2);
+    decl_function_x_ghost(2,4);
+    def_function_x_ghost(2,4);
+    decl_with_fptr(&decl_function_x_ghost);
+    def_with_fptr(&decl_function_x_ghost);
+    decl_variadic(2, 1, 2, 3, 4, 4);
+    def_variadic(2, 1, 2, 3, 4, 4);
+  */
+}
\ No newline at end of file

tests/pretty_printing/oracle/ghost_parameters.res.oracle

+[kernel] Parsing tests/pretty_printing/ghost_parameters.c (with preprocessing)
+/* Generated by Frama-C */
+void decl_function_void_no_ghost(void);
+
+void def_function_void_no_ghost(void)
+{
+  return;
+}
+
+void decl_function_void_ghost(void)/*@ ghost (int y) */;
+
+void def_function_void_ghost(void)/*@ ghost (int y) */
+{
+  return;
+}
+
+void decl_function_x_no_ghost(int x);
+
+void def_function_x_no_ghost(int x)
+{
+  return;
+}
+
+void decl_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 def_with_fptr(void (*ptr)(int x)/*@ ghost (int y) */)
+{
+  void (*local)(int )/*@ ghost (int ) */ = ptr;
+  (*local)(4)/*@ ghost (2) */;
+  /*@ ghost (*local)(4,2); */
+  return;
+}
+
+void decl_variadic(int x , ...)/*@ ghost (int y) */;
+
+void def_variadic(int x , ...)/*@ ghost (int y) */
+{
+  return;
+}
+
+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_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_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) */;
+  /*@ ghost decl_function_void_no_ghost(); */
+  /*@ ghost def_function_void_no_ghost(); */
+  /*@ ghost decl_function_void_ghost(4); */
+  /*@ ghost def_function_void_ghost(4); */
+  /*@ ghost decl_function_x_no_ghost(2); */
+  /*@ ghost def_function_x_no_ghost(2); */
+  /*@ ghost decl_function_x_ghost(2,4); */
+  /*@ ghost def_function_x_ghost(2,4); */
+  /*@ ghost decl_with_fptr(& decl_function_x_ghost); */
+  /*@ ghost def_with_fptr(& decl_function_x_ghost); */
+  /*@ ghost decl_variadic(2,1,2,3,4,4); */
+  /*@ ghost def_variadic(2,1,2,3,4,4); */
+  __retres = 0;
+  return __retres;
+}
+
+
+[kernel] Parsing tests/pretty_printing/result/ghost_parameters.c (with preprocessing)
+[kernel] Parsing tests/pretty_printing/ghost_parameters.c (with preprocessing)
+[kernel] tests/pretty_printing/ghost_parameters.c:2: Warning: 
+  dropping duplicate def'n of func def_function_void_no_ghost at tests/pretty_printing/ghost_parameters.c:2 in favor of that at tests/pretty_printing/result/ghost_parameters.c:4
+[kernel] tests/pretty_printing/ghost_parameters.c:4: Warning: 
+  dropping duplicate def'n of func def_function_void_ghost at tests/pretty_printing/ghost_parameters.c:4 in favor of that at tests/pretty_printing/result/ghost_parameters.c:11
+[kernel] tests/pretty_printing/ghost_parameters.c:6: Warning: 
+  dropping duplicate def'n of func def_function_x_no_ghost at tests/pretty_printing/ghost_parameters.c:6 in favor of that at tests/pretty_printing/result/ghost_parameters.c:18
+[kernel] tests/pretty_printing/ghost_parameters.c:8: Warning: 
+  dropping duplicate def'n of func def_function_x_ghost at tests/pretty_printing/ghost_parameters.c:8 in favor of that at tests/pretty_printing/result/ghost_parameters.c:25
+[kernel] tests/pretty_printing/ghost_parameters.c:10: Warning: 
+  dropping duplicate def'n of func def_with_fptr at tests/pretty_printing/ghost_parameters.c:10 in favor of that at tests/pretty_printing/result/ghost_parameters.c:32
+[kernel] tests/pretty_printing/ghost_parameters.c:17: Warning: 
+  dropping duplicate def'n of func def_variadic at tests/pretty_printing/ghost_parameters.c:17 in favor of that at tests/pretty_printing/result/ghost_parameters.c:42
+[kernel] tests/pretty_printing/ghost_parameters.c:19: Warning: 
+  def'n of func main at tests/pretty_printing/ghost_parameters.c:19 (sum 21482) conflicts with the one at tests/pretty_printing/result/ghost_parameters.c:47 (sum 23256); keeping the one at tests/pretty_printing/result/ghost_parameters.c:47.
+/* Generated by Frama-C */
+void decl_function_void_no_ghost(void);
+
+void def_function_void_no_ghost(void)
+{
+  return;
+}
+
+void decl_function_void_ghost(void)/*@ ghost (int y) */;
+
+void def_function_void_ghost(void)/*@ ghost (int y) */
+{
+  return;
+}
+
+void decl_function_x_no_ghost(int x);
+
+void def_function_x_no_ghost(int x)
+{
+  return;
+}
+
+void decl_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 def_with_fptr(void (*ptr)(int x)/*@ ghost (int y) */)
+{
+  void (*local)(int )/*@ ghost (int ) */ = ptr;
+  (*local)(4)/*@ ghost (2) */;
+  /*@ ghost (*local)(4,2); */
+  return;
+}
+
+void decl_variadic(int x , ...)/*@ ghost (int y) */;
+
+void def_variadic(int x , ...)/*@ ghost (int y) */
+{
+  return;
+}
+
+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_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_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) */;
+  /*@ ghost decl_function_void_no_ghost(); */
+  /*@ ghost def_function_void_no_ghost(); */
+  /*@ ghost decl_function_void_ghost(4); */
+  /*@ ghost def_function_void_ghost(4); */
+  /*@ ghost decl_function_x_no_ghost(2); */
+  /*@ ghost def_function_x_no_ghost(2); */
+  /*@ ghost decl_function_x_ghost(2,4); */
+  /*@ ghost def_function_x_ghost(2,4); */
+  /*@ ghost decl_with_fptr(& decl_function_x_ghost); */
+  /*@ ghost def_with_fptr(& decl_function_x_ghost); */
+  /*@ ghost decl_variadic(2,1,2,3,4,4); */
+  /*@ ghost def_variadic(2,1,2,3,4,4); */
+  __retres = 0;
+  return __retres;
+}
+
+