[ghost] Changes parsing-error for \ghost qualifier

src/kernel_internals/parsing/clexer.mll

@@ -573,7 +573,7 @@ rule initial = parse
       end else begin
         let start = Lexing.lexeme_start_p lexbuf in
         let source = Cil_datatype.Position.of_lexing_pos start in
-        Kernel.abort ~source "Use of \\ghost out of ghost code"
+        E.parse_error ~source "Use of \\ghost out of ghost code"
       end
     }
 

src/kernel_internals/parsing/cparser.mly

@@ -1471,7 +1471,7 @@ cvspec:
       if String.compare annot "\\ghost" = 0 then begin
         let start = Parsing.symbol_start_pos () in
         let source = Cil_datatype.Position.of_lexing_pos start in
-        Kernel.abort ~source "Use of \\ghost out of ghost code"
+        Errorloc.parse_error ~source "Use of \\ghost out of ghost code"
       end else
         SpecCV(CV_ATTRIBUTE_ANNOT annot), loc
     }

tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle

 [kernel] Parsing tests/syntax/ghost_cv_parsing_errors.c (with preprocessing)
-[kernel] tests/syntax/ghost_cv_parsing_errors.c:13: User Error: 
-  Use of \ghost out of ghost code
-[kernel] User Error: stopping on file "tests/syntax/ghost_cv_parsing_errors.c" that has errors.
-  Add '-kernel-msg-key pp' for preprocessing command.
+[kernel] tests/syntax/ghost_cv_parsing_errors.c:11: 
+  Use of \ghost out of ghost code:
+  Location: between lines 11 and 13, before or at token: \ghost
+  9     #ifdef IN_TYPE
+  10    
+  
+  11    struct S {
+  12      int a ;
+  13    } \ghost ;
+  
+  14    
+  15    #endif
 [kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle

 [kernel] Parsing tests/syntax/ghost_cv_parsing_errors.c (with preprocessing)
-[kernel] tests/syntax/ghost_cv_parsing_errors.c:19: User Error: 
-  Use of \ghost out of ghost code
-[kernel] User Error: stopping on file "tests/syntax/ghost_cv_parsing_errors.c" that has errors.
-  Add '-kernel-msg-key pp' for preprocessing command.
+[kernel] tests/syntax/ghost_cv_parsing_errors.c:19: 
+  Use of \ghost out of ghost code:
+  Location: line 19, between columns 0 and 4, before or at token: \ghost
+  17    #ifdef IN_DECL
+  18    
+  19    int \ghost global ;
+        ^^^^^^^^^^^^^^^^^^^
+  20    
+  21    #endif
 [kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle

 [kernel] Parsing tests/syntax/ghost_cv_parsing_errors.c (with preprocessing)
-[kernel] tests/syntax/ghost_cv_parsing_errors.c:25: User Error: 
-  Use of \ghost out of ghost code
-[kernel] User Error: stopping on file "tests/syntax/ghost_cv_parsing_errors.c" that has errors.
-  Add '-kernel-msg-key pp' for preprocessing command.
+[kernel] tests/syntax/ghost_cv_parsing_errors.c:25: 
+  Use of \ghost out of ghost code:
+  Location: line 25, between columns 14 and 14
+  23    #ifdef IN_GHOST_ATTR
+  24    
+  25    int /*@ \ghost */ global ;
+        ^^^^^^^^^^^^^^^^^^^^^^^^^^
+  26    
+  27    #endif
 [kernel] Frama-C aborted: invalid user input.