[Kernel/test] queueInstr in ghost

tests/cil/oracle/queue_ghost_instr.res.oracle

+[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 ++; */
+  }
+  ;
+  __retres = 0;
+  return __retres;
+}
+
+

tests/cil/queue_ghost_instr.i

+/* 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++ ;
+  }
+}

tests/cil/queue_ghost_instr.ml

+class add_skip = object(this)
+  inherit Visitor.frama_c_inplace
+
+  method! vfunc f =
+    File.must_recompute_cfg f ;
+    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