Merge branch 'fix/kernel/ghost-else-error-msg' into 'master'

[ghost] Fixes error msg for ignored ghost-else

See merge request frama-c/frama-c!2604

src/kernel_internals/parsing/cparser.mly

@@ -923,7 +923,9 @@ else_part:
     %prec ghost_else_no_else /* To force the non ghost else to be attached to the current if */
 |   LGHOST_ELSE annotated_statement RGHOST ELSE annotated_statement
     {
-      Format.eprintf "Warning: %a: Invalid ghost else ignored@." Cil_datatype.Location.pretty $1 ;
+      let loc = Cil_datatype.Location.of_lexing_loc (Parsing.symbol_start_pos (), Parsing.symbol_end_pos ()) in
+      Kernel.warning ~wkey:Kernel.wkey_ghost_bad_use ~source:(fst loc)
+        "Invalid ghost else ignored@." ;
       in_block $5
     }
 

tests/syntax/ghost_else_bad.c

 /* run.config
    OPT: -no-autoload-plugins -cpp-extra-args="-DERROR_LOC_WITH_COMMENTS"
-   OPT: -no-autoload-plugins -cpp-extra-args="-DALREADY_HAS_ELSE" -print
+   OPT: -no-autoload-plugins -cpp-extra-args="-DALREADY_HAS_ELSE" -print -kernel-warn-key ghost:bad-use=feedback
    OPT: -no-autoload-plugins -cpp-extra-args="-DBAD_ANNOT_POSITION"
 */
 
@@ -22,7 +22,7 @@ void if_ghost_else_block_comments_then_error(int x, int y) {
 
 #endif
 
-#ifdef ALREADY_HAS_ELSE 
+#ifdef ALREADY_HAS_ELSE
 // Must warn that the ghost else cannot appear since there is already a else
 // Thus the ghost else is ignored and the resulting code does not comprise it
 

tests/syntax/oracle/ghost_else_bad.1.res.oracle

 [kernel] Parsing tests/syntax/ghost_else_bad.c (with preprocessing)
+[kernel:ghost:bad-use] tests/syntax/ghost_else_bad.c:32: 
+  Invalid ghost else ignored
 /* Generated by Frama-C */
 void if_ghost_else_block_bad(int x, int y)
 {