[ghost] Take care of assertions when checking CFG

src/kernel_internals/typing/ghost_cfg.ml

@@ -29,6 +29,14 @@ module StmtSet = Stmt.Hptset
 
 let error = Kernel.warning ~wkey:Kernel.wkey_ghost_bad_use
 
+
+let annot_attr = "has_annot"
+
+(* For no ghost project, we add an attribute each stmt that has annotations. *)
+let has_annot stmt =
+  Annotations.code_annot stmt <> [] ||
+  Cil.hasAttribute annot_attr stmt.sattr
+
 let noGhostBlock b =
   let noGhostVisitor = object (self)
     inherit genericCilVisitor (refresh (Project.current()))
@@ -44,10 +52,15 @@ let noGhostBlock b =
       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
+            let cases = List.filter
+              (fun s -> not (self#original s).ghost) cases
+            in
             s.skind <- Switch(e, block, cases, loc) ;
             DoChildren
-          | _ -> DoChildren
+          | _ ->
+            let original = self#original s in
+            s.sattr <- if has_annot original then [AttrAnnot annot_attr] else [] ;
+            DoChildren
         end
 
     method getBehavior () = self#behavior
@@ -62,7 +75,7 @@ type follower =
 let sync stmt =
   match stmt.skind with
   (* We ignore blocks: their successors are their 1st stmt so we visit them *)
-  | Instr(Skip(_)) | Block(_) | Continue(_) | Break(_) -> false
+  | Instr(Skip(_)) | Block(_) | Continue(_) | Break(_) -> has_annot stmt
   | _ -> true
 
 let nextSync stmt =

tests/cil/ghost_cfg.c

@@ -93,6 +93,16 @@ int ghost_goto_ghost(){
   return 0;
 }
 
+void switch_loses_assertion (int c) {
+  //@ ghost int x = 1;
+  switch (c) {
+    case 0: return;
+    //@ ghost case 1: x++; /*@ assert x == 2; */ break;
+    default: /*@ assert x == 1; */ break;
+  }
+  return;
+}
+
 #endif
 
 #ifdef CANT_CHECK

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

@@ -19,5 +19,8 @@
 [kernel:ghost:bad-use] tests/cil/ghost_cfg.c:89: Warning: 
   Ghost code breaks CFG starting at:
   /*@ ghost goto X; */
+[kernel:ghost:bad-use] tests/cil/ghost_cfg.c:100: Warning: 
+  Ghost code breaks CFG starting at:
+  case 1: /*@ ghost x ++; */
 [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:101: User Error: 
+[kernel] tests/cil/ghost_cfg.c:111: 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.