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