diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 23e9a64223935754b638f38147a59a69cf90bf1c..79da27bd41da6e97700185a0d1cf6801b9f1c812 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -265,6 +265,25 @@ let mkBlock (slst: stmt list) : block =
let mkBlockNonScoping l = let b = mkBlock l in b.bscoping <- false; b
+let rec enforceGhostStmtCoherence ?(force_ghost=false) stmt =
+ let force_ghost = force_ghost || stmt.ghost in
+ stmt.ghost <- force_ghost ;
+ begin match stmt.skind with
+ | Break(_) | Continue(_) | Goto(_) | Throw(_)
+ | Instr(_) | Return(_) -> ()
+ | UnspecifiedSequence(_) -> ()
+ | If(_, b1, b2, _) | TryFinally(b1, b2, _) | TryExcept(b1, _, b2, _) ->
+ enforceGhostBlockCoherence ~force_ghost b1 ;
+ enforceGhostBlockCoherence ~force_ghost b2
+ | Switch(_, b, _, _) | Loop(_, b, _, _, _) | Block(b) ->
+ enforceGhostBlockCoherence ~force_ghost b
+ | TryCatch(b, l, _) ->
+ enforceGhostBlockCoherence ~force_ghost b ;
+ List.iter (fun (_, b) -> enforceGhostBlockCoherence ~force_ghost b) l
+ end
+and enforceGhostBlockCoherence ?force_ghost block =
+ List.iter (enforceGhostStmtCoherence ?force_ghost) block.bstmts
+
let mkStmt ?(ghost=false) ?(valid_sid=false) ?(sattr=[]) (sk: stmtkind) : stmt =
{ skind = sk;
labels = [];
@@ -3359,6 +3378,7 @@ and childrenExp (vis: cilVisitor) (e: exp) : exp =
let res =
doVisitCil vis
vis#behavior.memo_stmt vis#vstmt (childrenStmt toPrepend) s in
+ let ghost = res.ghost in
(* Now see if we have saved some instructions *)
toPrepend := !toPrepend @ vis#unqueueInstr ();
(match !toPrepend with
@@ -3366,8 +3386,8 @@ and childrenExp (vis: cilVisitor) (e: exp) : exp =
| _ ->
let b =
mkBlockNonScoping
- ((List.map (fun i -> mkStmt (Instr i)) !toPrepend)
- @ [mkStmt res.skind])
+ ((List.map (fun i -> mkStmt ~ghost (Instr i)) !toPrepend)
+ @ [mkStmt ~ghost res.skind])
in
b.battrs <- addAttribute (Attr (vis_tmp_attr, [])) b.battrs;
(* Make our statement contain the instructions to prepend *)
@@ -3494,6 +3514,7 @@ and childrenExp (vis: cilVisitor) (e: exp) : exp =
else s.skind
in
if skind' != s.skind then s.skind <- skind';
+ enforceGhostStmtCoherence s ;
(* Visit the labels *)
let labels' =
let fLabel = function
@@ -6637,7 +6658,7 @@ let childrenFileSameGlobals vis f =
in
List.iter
(fun s ->
- match s.skind with
+ begin match s.skind with
| Instr i -> s.skind <- stmt_of_instr_list (doInstrList [i])
| If (_e, tb, eb, _) ->
peepHole1 doone tb.bstmts;
@@ -6657,7 +6678,9 @@ let childrenFileSameGlobals vis f =
peepHole1 doone b.bstmts;
peepHole1 doone h.bstmts;
s.skind <- TryExcept(b, (doInstrList il, e), h, l);
- | Return _ | Goto _ | Break _ | Continue _ | Throw _ -> ())
+ | Return _ | Goto _ | Break _ | Continue _ | Throw _ -> ()
+ end ;
+ enforceGhostStmtCoherence s)
ss
(* Process two statements and possibly replace them both *)
diff --git a/tests/cil/change_to_instr.i b/tests/cil/change_to_instr.i
new file mode 100644
index 0000000000000000000000000000000000000000..b83b32608f67b7918cae94834696592bc19cf770
--- /dev/null
+++ b/tests/cil/change_to_instr.i
@@ -0,0 +1,17 @@
+/* run.config
+OPT: -load-script tests/cil/change_to_instr.ml -print
+*/
+
+
+int main(){
+ int i = 0 ;
+ //@ ghost int j = 0 ;
+
+ i++ ;
+ //@ ghost j++ ;
+
+ {
+ //@ ghost int x = 0;
+ //@ ghost x++ ;
+ }
+}
diff --git a/tests/cil/change_to_instr.ml b/tests/cil/change_to_instr.ml
new file mode 100644
index 0000000000000000000000000000000000000000..04d2679952d844a376299eb5e32449b829314e9a
--- /dev/null
+++ b/tests/cil/change_to_instr.ml
@@ -0,0 +1,17 @@
+class add_skip = object(_)
+ inherit Visitor.frama_c_inplace
+
+ method! vfunc f =
+ File.must_recompute_cfg f ;
+ Cil.DoChildren
+
+ method! vinst i =
+ let open Cil_types in
+ Cil.ChangeTo [ Skip(Cil.CurrentLoc.get()) ; i ]
+end
+
+let run () =
+ Visitor.visitFramacFileSameGlobals (new add_skip) (Ast.get())
+
+let () =
+ Db.Main.extend run
diff --git a/tests/cil/oracle/change_to_instr.res.oracle b/tests/cil/oracle/change_to_instr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..590858bb9f0d672e6dd54e6ecdeb12302be7ea8c
--- /dev/null
+++ b/tests/cil/oracle/change_to_instr.res.oracle
@@ -0,0 +1,25 @@
+[kernel] Parsing tests/cil/change_to_instr.i (no preprocessing)
+/* Generated by Frama-C */
+int main(void)
+{
+ int __retres;
+ ;
+ int i = 0;
+ /*@ ghost ; */
+ /*@ ghost int j = 0; */
+ ;
+ i ++;
+ /*@ ghost ; */
+ /*@ ghost j ++; */
+ {
+ /*@ ghost ; */
+ /*@ ghost int x = 0; */
+ /*@ ghost ; */
+ /*@ ghost x ++; */
+ }
+ ;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/cil/oracle/queue_ghost_instr.res.oracle b/tests/cil/oracle/queue_ghost_instr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1066baea30d7eb9f0fadc390dfbc4ef28084385d
--- /dev/null
+++ b/tests/cil/oracle/queue_ghost_instr.res.oracle
@@ -0,0 +1,29 @@
+[kernel] Parsing tests/cil/queue_ghost_instr.i (no preprocessing)
+/* Generated by Frama-C */
+int main(void)
+{
+ int __retres;
+ ;
+ int i = 0;
+ /*@ ghost ; */
+ /*@ ghost int j = 0; */
+ ;
+ i ++;
+ /*@ ghost ; */
+ /*@ ghost j ++; */
+ {
+ /*@ ghost ; */
+ /*@ ghost int x = 0; */
+ /*@ ghost ; */
+ /*@ ghost x ++; */
+ }
+ ;
+ if (i) ;
+ /*@ ghost ; */
+ /*@ ghost if (j) ; */
+ ;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/cil/queue_ghost_instr.i b/tests/cil/queue_ghost_instr.i
new file mode 100644
index 0000000000000000000000000000000000000000..3bae2b6f40b0ef3824806fb03117f9af8f5e9610
--- /dev/null
+++ b/tests/cil/queue_ghost_instr.i
@@ -0,0 +1,26 @@
+/* run.config
+OPT: -load-script tests/cil/queue_ghost_instr.ml -print
+*/
+
+
+int main(){
+ int i = 0 ;
+ //@ ghost int j = 0 ;
+
+ i++ ;
+ //@ ghost j++ ;
+
+ {
+ //@ ghost int x = 0;
+ //@ ghost x++ ;
+ }
+
+ if(i){
+ ;
+ }
+
+ /*@ ghost if(j){
+
+ }
+ */
+}
diff --git a/tests/cil/queue_ghost_instr.ml b/tests/cil/queue_ghost_instr.ml
new file mode 100644
index 0000000000000000000000000000000000000000..22fcc753adaeea44ff4733b3971b4b2d53f12bce
--- /dev/null
+++ b/tests/cil/queue_ghost_instr.ml
@@ -0,0 +1,27 @@
+class add_skip = object(this)
+ inherit Visitor.frama_c_inplace
+
+ method! vfunc f =
+ File.must_recompute_cfg f ;
+ Cil.DoChildren
+
+ method! vstmt s =
+ let open Cil_types in
+ begin match s.skind with
+ | If(_) ->
+ this#queueInstr([Skip(Cil.CurrentLoc.get())])
+ | _ -> ()
+ end ;
+ Cil.DoChildren
+
+ method! vinst _ =
+ let open Cil_types in
+ this#queueInstr([Skip(Cil.CurrentLoc.get())]) ;
+ Cil.DoChildren
+end
+
+let run () =
+ Visitor.visitFramacFileSameGlobals (new add_skip) (Ast.get())
+
+let () =
+ Db.Main.extend run