[kernel] Ghost_cfg do not share visited stmts when CFGs can be shared

src/kernel_internals/typing/ghost_cfg.ml

@@ -114,8 +114,8 @@ let alteredCFG stmt =
 let checkGhostCFG bhv withGhostStart noGhost =
   let rec do_check visited withGhostStart noGhostStart =
     match (nextSync withGhostStart), (nextSync noGhostStart) with
-    | Stmt withGhost, Stmt _ when StmtSet.mem withGhost visited -> visited
     | Stmt withGhost, Stmt noGhost ->
+      let is_visited = StmtSet.mem withGhost visited in
       let visited = StmtSet.add withGhost visited in
       let withGhost =
         StmtSet.contains_single_elt (nextNonGhostSync withGhost)
@@ -124,6 +124,9 @@ let checkGhostCFG bhv withGhostStart noGhost =
         | Some s1, s2 when not (Stmt.equal s1 (Get_orig.stmt bhv s2)) ->
           alteredCFG withGhostStart ; visited
 
+        (* Note: this test is deferred so that bad stmts are detected above *)
+        | Some _, _ when is_visited -> visited
+
         | Some ({ skind = If(_) } as withGhost), noGhost ->
           let wgThen, wgElse = Cil.separate_if_succs withGhost in
           let ngThen, ngElse = Cil.separate_if_succs noGhost in
@@ -141,7 +144,7 @@ let checkGhostCFG bhv withGhostStart noGhost =
           let visited = List.fold_left2 do_check visited wgSuccsNG ngSuccs in
           List.fold_left (fun v s -> do_check v s ngDef) visited mustDefault
 
-        | Some ({ skind=Loop(_,wgb,_,_,_) }), { skind=Loop (_, ngb,_,_,_) } ->
+        | Some ({ skind=Loop(_,wgb,_,_,_) }), { skind=Loop (_,ngb,_,_,_) } ->
           begin match wgb.bstmts, ngb.bstmts with
             | s1 :: _ , s2 :: _ -> do_check visited s1 s2
             | _, _ -> visited

tests/cil/ghost_cfg.c

@@ -109,6 +109,16 @@ int ghost_return() {
   return 0;
 }
 
+void shared_cfgs(int x) {
+  switch (x) {
+    /*@ ghost case 3: ; */
+  case 2: ;
+    x = 5;
+  default: ;
+    x ++;
+  }
+}
+
 #endif
 
 #ifdef CANT_CHECK

tests/cil/oracle/ghost_cfg.0.res.oracle

@@ -26,5 +26,8 @@
   Ghost code breaks CFG starting at:
   /*@ ghost __retres = 1; */
   /*@ ghost goto return_label; */
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:114: Warning: 
+  Ghost code breaks CFG starting at:
+  /*@ ghost case 3: ; */
 [kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
 [kernel] Frama-C aborted: invalid user input.

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

 [kernel] Parsing tests/cil/ghost_cfg.c (with preprocessing)
-[kernel] tests/cil/ghost_cfg.c:117: User Error: 
+[kernel] tests/cil/ghost_cfg.c:127: 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.