diff --git a/tests/cil/oracle/queue_ghost_instr.res.oracle b/tests/cil/oracle/queue_ghost_instr.res.oracle index 7f8108c3d871da17c6f569e14c6e5b1883bb7974..1066baea30d7eb9f0fadc390dfbc4ef28084385d 100644 --- a/tests/cil/oracle/queue_ghost_instr.res.oracle +++ b/tests/cil/oracle/queue_ghost_instr.res.oracle @@ -18,6 +18,10 @@ int main(void) /*@ 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 index 04338f314ded7a99b0db8f66f390cdaaa921b5be..3bae2b6f40b0ef3824806fb03117f9af8f5e9610 100644 --- a/tests/cil/queue_ghost_instr.i +++ b/tests/cil/queue_ghost_instr.i @@ -14,4 +14,13 @@ int main(){ //@ 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 index c30ea64bd869549564ccaf54ed2d75b1340be2e6..22fcc753adaeea44ff4733b3971b4b2d53f12bce 100644 --- a/tests/cil/queue_ghost_instr.ml +++ b/tests/cil/queue_ghost_instr.ml @@ -5,6 +5,15 @@ class add_skip = object(this) 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())]) ;