[ghost] Better error msg in Cfg

.Makefile.lint

@@ -12,8 +12,6 @@ ML_LINT_KO+=src/kernel_internals/runtime/messages.mli
 ML_LINT_KO+=src/kernel_internals/runtime/special_hooks.ml
 ML_LINT_KO+=src/kernel_internals/typing/allocates.ml
 ML_LINT_KO+=src/kernel_internals/typing/asm_contracts.ml
-ML_LINT_KO+=src/kernel_internals/typing/cfg.ml
-ML_LINT_KO+=src/kernel_internals/typing/cfg.mli
 ML_LINT_KO+=src/kernel_internals/typing/frontc.mli
 ML_LINT_KO+=src/kernel_internals/typing/infer_annotations.ml
 ML_LINT_KO+=src/kernel_internals/typing/logic_builtin.ml

src/kernel_internals/typing/cfg.mli

@@ -57,7 +57,7 @@ val computeFileCFG: file -> unit
 val clearFileCFG: ?clear_id:bool -> file -> unit
 
 (** Compute a control flow graph for fd.  Stmts in fd have preds and succs
-  filled in *)
+    filled in *)
 val cfgFun : fundec -> unit
 
 (** clear the sid, succs, and preds fields of each statement in a function *)
@@ -76,4 +76,3 @@ val prepareCFG: ?keepSwitch:bool -> fundec -> unit
 
 (**/**)
 val clear_sid_info_ref: (unit -> unit) ref
-

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

 [kernel] Parsing tests/cil/ghost_cfg.c (with preprocessing)
-[kernel] User Error: tests/cil/ghost_cfg.c:101:
-  'goto X;' cannot see target label (ghost), removing ghost status of the label.
+[kernel] tests/cil/ghost_cfg.c:101: User Error: 
+  'goto X;' would jump from normal statement to ghost code
 [kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
 [kernel] Frama-C aborted: invalid user input.