Adds a test to check that ghost parameters lead to ghost formals

tests/syntax/ghost_parameters_formals_status.i

+/* run.config
+EXECNOW: make -s tests/syntax/ghost_parameters_formals_status.cmxs
+OPT: -load-module tests/syntax/ghost_parameters_formals_status.cmxs
+*/
+
+void declaration_void(void) /*@ ghost (int x, int y) */ ;
+void declaration_not_void(int a, int b) /*@ ghost (int x, int y) */ ;
+
+void definition_void(void) /*@ ghost(int x, int y) */ {
+
+}
+
+void definition_not_void(int a, int b) /*@ ghost(int x, int y) */ {
+
+}
+
+void caller(){
+  declaration_void() /*@ ghost (1, 2) */ ;
+  declaration_not_void(1, 2) /*@ ghost (3, 4) */ ;
+  definition_void() /*@ ghost (1, 2) */ ;
+  definition_not_void(1, 2) /*@ ghost (3, 4) */ ;
+}

tests/syntax/ghost_parameters_formals_status.ml

+open Cil_types
+
+let run () =
+  let print_info kf =
+    let pretty_formal fmt vi =
+      assert(vi.vformal) ;
+      Format.fprintf fmt "@\n- %a which is %s"
+        Cil_datatype.Varinfo.pretty vi
+        (if vi.vghost then "ghost" else "non-ghost")
+    in
+    let pretty_formal_list fmt l =
+      match l with
+      | [] ->
+        Format.fprintf fmt "No Formals"
+      | _ ->
+        Format.fprintf fmt "Formals are %a"
+          (Pretty_utils.pp_flowlist ~left:"" ~sep:"" ~right:"" pretty_formal) l
+    in
+    let vi = Kernel_function.get_vi kf in
+    let formals = Cil.getFormalsDecl vi in    
+    Kernel.feedback "Type of %s is %a.@ %a"
+      vi.vname
+      Cil_datatype.Typ.pretty vi.vtype
+      pretty_formal_list formals
+  in
+  Globals.Functions.iter print_info
+  
+let () = Db.Main.extend run

tests/syntax/oracle/ghost_parameters_formals_status.res.oracle

+[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) */.
+  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) */.
+  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) */.
+  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) */.
+  Formals are 
+               - x which is ghost
+               - y which is ghost