diff --git a/Makefile b/Makefile
index 40e3547ea5d0d45704ea301abfced7fe406909dc..6d6b917ff4d52b2438ccc74e8b1f3764d95654d8 100644
--- a/Makefile
+++ b/Makefile
@@ -610,6 +610,7 @@ KERNEL_CMO=\
src/kernel_services/ast_queries/json_compilation_database.cmo \
src/kernel_services/ast_queries/file.cmo \
src/kernel_internals/typing/translate_lightweight.cmo \
+ src/kernel_internals/typing/ghost_cfg.cmo \
src/kernel_internals/typing/allocates.cmo \
src/kernel_internals/typing/unroll_loops.cmo \
src/kernel_internals/typing/asm_contracts.cmo \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index cf5dcb9aae8bafcca490092d56ebd4e977f08bf4..422e78690a6874f7d42f357cecbb1c25134dca93 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -391,6 +391,8 @@ src/kernel_internals/typing/cfg.ml: CIL
src/kernel_internals/typing/cfg.mli: CIL
src/kernel_internals/typing/frontc.ml: CIL
src/kernel_internals/typing/frontc.mli: CIL
+src/kernel_internals/typing/ghost_cfg.ml: CEA_LGPL
+src/kernel_internals/typing/ghost_cfg.mli: CEA_LGPL
src/kernel_internals/typing/infer_annotations.ml: CEA_LGPL
src/kernel_internals/typing/infer_annotations.mli: CEA_LGPL
src/kernel_internals/typing/logic_builtin.ml: CEA_INRIA_LGPL
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index 21e648adf5c318f6dd538eadb1f81ac982d868d4..844b419accab7c2fd535a5b0c192863cb4adbb5a 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -49,7 +49,6 @@ open Cil
open Cil_types
open Cil_datatype
-
(* All the nodes of the function visited, in a flat list *)
let nodeList : stmt list ref = ref []
@@ -228,6 +227,13 @@ and cfgStmt env (s: stmt) next break cont =
else
()
| Return _ | Throw _ -> ()
+ | Goto (p,_) when not s.ghost && !p.ghost ->
+ Kernel.warning
+ ~wkey:Kernel.wkey_ghost_bad_non_ghost
+ "%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 ;
+ addSucc !p
| Goto (p,_) -> addSucc !p
| Break _ -> addOptionSucc break
| Continue _ -> addOptionSucc cont
diff --git a/src/kernel_internals/typing/ghost_cfg.ml b/src/kernel_internals/typing/ghost_cfg.ml
new file mode 100644
index 0000000000000000000000000000000000000000..848e2a4529c97e5662a1de4dca85dff079ee9b71
--- /dev/null
+++ b/src/kernel_internals/typing/ghost_cfg.ml
@@ -0,0 +1,169 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil
+open Cil_types
+open Visitor_behavior
+
+module Stmt = Cil_datatype.Stmt
+module StmtSet = Stmt.Hptset
+module Location = Cil_datatype.Location
+
+let error = Kernel.warning ~wkey:Kernel.wkey_ghost_bad_use
+
+let noGhostBlock b =
+ let noGhostVisitor = object (self)
+ inherit genericCilVisitor (refresh (Project.current()))
+
+ method private original = Get_orig.stmt self#behavior
+
+ method! vstmt s =
+ if s.ghost then begin
+ s.skind <- Instr(Skip (Stmt.loc s)) ;
+ s.labels <- [] ;
+ s.ghost <- false ;
+ SkipChildren
+ end else
+ begin match s.skind with
+ | Switch(e, block, cases, loc) ->
+ let cases = List.filter (fun s -> not (self#original s).ghost) cases in
+ s.skind <- Switch(e, block, cases, loc) ;
+ DoChildren
+ | _ -> DoChildren
+ end
+
+ method getBehavior () = self#behavior
+ end in
+ (visitCilBlock (noGhostVisitor :> cilVisitor) b), (noGhostVisitor#getBehavior ())
+
+let the l = match l with [ stmt ] -> stmt | _ -> assert false
+
+let isSkip stmt =
+ match stmt.skind with
+ | Instr(Skip(_)) | Block(_) | Continue(_) | Break(_) -> true
+ | _ -> false
+
+type follower =
+ | Infinite | Exit | Stmt of stmt
+
+let rec skipSkip ?(visited=StmtSet.empty) s =
+ if StmtSet.mem s visited then Infinite
+ else match isSkip s with
+ | false -> Stmt s
+ | true when s.succs = [] -> Exit
+ | _ -> skipSkip ~visited:(StmtSet.add s visited) (the s.succs)
+
+let firstNonSkipNonGhosts stmt =
+ let rec do_find ~visited stmt =
+ if List.mem stmt !visited then []
+ else begin
+ visited := stmt :: !visited ;
+ if isSkip stmt then do_find ~visited (the stmt.succs)
+ else if not (stmt.ghost) then [ stmt ]
+ else List.flatten (List.map (do_find ~visited) stmt.succs)
+ end
+ in
+ do_find ~visited:(ref []) stmt
+
+let alteredCFG stmt =
+ error "Ghost code breaks CFG starting at: %a@.%a"
+ Location.pretty (Stmt.loc stmt)
+ Cil_printer.pp_stmt stmt
+
+let rec checkGhostCFG bhv ?(visited=ref StmtSet.empty) withGhostStart noGhost =
+ match (skipSkip withGhostStart), (skipSkip noGhost) with
+ | Stmt withGhost, Stmt noGhost -> begin
+ if StmtSet.mem withGhost !visited then ()
+ else begin
+ visited := StmtSet.add withGhost !visited ;
+ let withGhost = List.sort_uniq Stmt.compare (firstNonSkipNonGhosts withGhost) in
+ match withGhost, noGhost with
+ | [ s1 ], s2 when s1.sid <> (Get_orig.stmt bhv s2).sid ->
+ alteredCFG withGhostStart
+ | [ { skind = If(_) } as s1 ], s2 ->
+ checkIf bhv ~visited s1 s2
+ | [ { skind = Switch(_) } as s1 ], s2 ->
+ checkSwitch bhv ~visited s1 s2
+ | [ { skind = Loop(_) } as s1 ], s2 ->
+ checkLoop bhv ~visited s1 s2
+ | [ { succs = [next_s1] } ], { succs = [next_s2] } ->
+ checkGhostCFG bhv ~visited next_s1 next_s2
+ | [ { succs = [] } ], { succs = [] } -> ()
+ | _, _ ->
+ alteredCFG withGhostStart
+ end
+ end ;
+ | Exit, Exit | Infinite, Infinite -> ()
+ | _ , _ -> alteredCFG withGhostStart
+and checkIf bhv ~visited withGhost noGhost =
+ let withGhostThen, withGhostElse = Cil.separate_if_succs withGhost in
+ let noGhostThen , noGhostElse = Cil.separate_if_succs noGhost in
+ checkGhostCFG bhv ~visited withGhostThen noGhostThen ;
+ checkGhostCFG bhv ~visited withGhostElse noGhostElse
+and checkLoop bhv ~visited withGhost noGhost =
+ let withGhostBlock, noGhostBlock = match withGhost.skind, noGhost.skind with
+ | Loop(_, b1, _, _, _), Loop(_, b2, _, _, _) -> b1, b2
+ | _ -> assert false
+ in
+ match withGhostBlock.bstmts, noGhostBlock.bstmts with
+ | s1 :: _ , s2 :: _ -> checkGhostCFG bhv ~visited s1 s2
+ | _, _ -> ()
+and checkSwitch bhv ~visited withGhost noGhost =
+ let noGhostSuccs, noGhostDef = Cil.separate_switch_succs noGhost in
+ let withGhostAllSuccs, withGhostDef = Cil.separate_switch_succs withGhost in
+ let withGhostSuccsGhost, withGhostSuccsNonGhost =
+ List.partition (fun s -> s.ghost) withGhostAllSuccs
+ in
+ let mustDefault = withGhostDef :: withGhostSuccsGhost in
+ assert(List.length noGhostSuccs = List.length withGhostSuccsNonGhost) ;
+ List.iter2 (checkGhostCFG bhv ~visited) withGhostSuccsNonGhost noGhostSuccs ;
+ List.iter (fun s -> checkGhostCFG bhv ~visited s noGhostDef) mustDefault
+
+let checkGhostCFGInFun (fd : fundec) =
+ if fd.svar.vghost then ()
+ else begin
+ let noGhost, bhv = noGhostBlock fd.sbody in
+ let vname = "__ghost_cfg_handler_" ^ fd.svar.vname in
+ let vi = { fd.svar with vid = -1 ; vname ; vsource = false } in
+ let noGhostFD = {
+ svar = vi ; smaxid = 0; slocals = []; sformals = [];
+ smaxstmtid = None; sallstmts = []; sspec = empty_funspec();
+ sbody = noGhost;
+ } in
+ Cfg.clearCFGinfo ~clear_id:false noGhostFD ;
+ Cfg.cfgFun noGhostFD ;
+ checkGhostCFG bhv (List.hd fd.sbody.bstmts) (List.hd noGhostFD.sbody.bstmts)
+ end
+
+let checkGhostCFGInFile (f : file) =
+ let visitor = object
+ inherit Visitor.frama_c_inplace
+ method! vfunc f = checkGhostCFGInFun f ; SkipChildren
+ end in
+ Visitor.visitFramacFileSameGlobals visitor f
+
+let transform_category =
+ File.register_code_transformation_category "Ghost CFG checking"
+
+let () =
+ File.add_code_transformation_after_cleanup
+ transform_category checkGhostCFGInFile
diff --git a/src/kernel_internals/typing/ghost_cfg.mli b/src/kernel_internals/typing/ghost_cfg.mli
new file mode 100644
index 0000000000000000000000000000000000000000..1ff3bd8f076fe0200d1c9b41fc599428aa4876b2
--- /dev/null
+++ b/src/kernel_internals/typing/ghost_cfg.mli
@@ -0,0 +1,22 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+