[ghost] changes an error kind

src/kernel_internals/typing/cfg.ml

@@ -163,9 +163,9 @@ and cfgStmt env (s: stmt) next break cont =
   if s.sid = -1 then s.sid <- Cil_const.Sid.next ();
   nodeList := s :: !nodeList;
   if s.succs <> [] then
-    Kernel.fatal 
+    Kernel.fatal
       "CFG must be cleared before being computed! Stmt %d '%a' \
-       has %d successors" 
+       has %d successors"
       s.sid Cil_printer.pp_stmt s (List.length s.succs);
   let addSucc (n: stmt) =
     s.succs <- n::s.succs;
@@ -228,8 +228,7 @@ and cfgStmt env (s: stmt) next break cont =
         ()
   | Return _  | Throw _ -> ()
   | Goto (p,_) when not s.ghost && !p.ghost ->
-    Kernel.warning
-      ~wkey:Kernel.wkey_ghost_bad_non_ghost
+    Kernel.error
       "%a:@ '%a' cannot see target label (ghost), removing ghost status of the label."
       Location.pretty (Stmt.loc s) Cil_printer.pp_stmt s ;
     (!p).ghost <- false ;
@@ -591,7 +590,7 @@ let xform_switch_block ?(keepSwitch=false) b =
                               (* begin replacement: *)
 	                    let pred =
 		              match ce.enode with
-		                  Const (CInt64 (z,_,_)) 
+		                  Const (CInt64 (z,_,_))
                                     when Integer.equal z Integer.zero
                                       ->
 		                    new_exp ~loc:ce.eloc (UnOp(LNot,e,intType))

src/kernel_services/plugin_entry_points/kernel.ml

@@ -132,9 +132,6 @@ let dkey_visitor = register_category "visitor"
 let wkey_annot_error = register_warn_category "annot-error"
 let () = set_warn_status wkey_annot_error Log.Wabort
 
-let wkey_ghost_bad_non_ghost = register_warn_category "ghost:bad-non-ghost"
-let () = set_warn_status wkey_ghost_bad_non_ghost Log.Werror
-
 let wkey_ghost_bad_use = register_warn_category "ghost:bad-use"
 let () = set_warn_status wkey_ghost_bad_use Log.Werror
 

src/kernel_services/plugin_entry_points/kernel.mli

@@ -130,9 +130,6 @@ val dkey_visitor: category
 val wkey_annot_error: warn_category
 (** error in annotation. If only a warning, annotation will just be ignored. *)
 
-val wkey_ghost_bad_non_ghost: warn_category
-(** error in non ghost code related to the use of ghost elements *)
-
 val wkey_ghost_bad_use: warn_category
 (** error in ghost code *)
 

tests/cil/oracle/ghost_cfg.1.res.oracle

 [kernel] Parsing tests/cil/ghost_cfg.c (with preprocessing)
-[kernel:ghost:bad-non-ghost] Warning: 
-  tests/cil/ghost_cfg.c:101:
+[kernel] User Error: tests/cil/ghost_cfg.c:101:
   'goto X;' cannot see target label (ghost), removing ghost status of the label.
-[kernel] Warning: warning ghost:bad-non-ghost treated as deferred error. See above messages for more information.
+[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
 [kernel] Frama-C aborted: invalid user input.