diff --git a/tests/syntax/oracle/temporary_location.res.oracle b/tests/syntax/oracle/temporary_location.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..8ba7b0ae166cd14b33bf0876e803391c5cd12cab --- /dev/null +++ b/tests/syntax/oracle/temporary_location.res.oracle @@ -0,0 +1,50 @@ +[kernel] Parsing tests/syntax/temporary_location.c (with preprocessing) +[kernel] __retres -> tests/syntax/temporary_location.c:7 +[kernel] __retres -> tests/syntax/temporary_location.c:7 +[kernel] __retres -> tests/syntax/temporary_location.c:7 +[kernel] __retres -> tests/syntax/temporary_location.c:17 +[kernel] tmp_0 -> tests/syntax/temporary_location.c:11 +[kernel] f -> tests/syntax/temporary_location.c:6 +[kernel] tmp_0 -> tests/syntax/temporary_location.c:11 +[kernel] __retres -> tests/syntax/temporary_location.c:17 +[kernel] x -> tests/syntax/temporary_location.c:15 +[kernel] tmp -> tests/syntax/temporary_location.c:16 +[kernel] x -> tests/syntax/temporary_location.c:15 +[kernel] x -> tests/syntax/temporary_location.c:15 +[kernel] x -> tests/syntax/temporary_location.c:15 +[kernel] x -> tests/syntax/temporary_location.c:15 +[kernel] y -> tests/syntax/temporary_location.c:16 +[kernel] tmp -> tests/syntax/temporary_location.c:16 +[kernel] __retres -> tests/syntax/temporary_location.c:17 +[kernel] y -> tests/syntax/temporary_location.c:16 +[kernel] __retres -> tests/syntax/temporary_location.c:17 +/* Generated by Frama-C */ +int f(void) +{ + int __retres; + __retres = 1; + return __retres; +} + +int main(void) +{ + int __retres; + int tmp_0; + tmp_0 = f(); + if (tmp_0) { + __retres = 0; + goto return_label; + } + else { + int tmp; + int x = 0; + tmp = x; + x ++; + int y = tmp + 1; + __retres = y + 3; + goto return_label; + } + return_label: return __retres; +} + + diff --git a/tests/syntax/temporary_location.c b/tests/syntax/temporary_location.c new file mode 100644 index 0000000000000000000000000000000000000000..765e6bccedee2df52e4d8551c4fac28faa06523e --- /dev/null +++ b/tests/syntax/temporary_location.c @@ -0,0 +1,19 @@ +/* run.config + EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs + OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs -print +*/ + +int f(void) { + return 1; +} + +int main(void) { + if(f()){ + return 0; + } + else { + int x = 0; + int y = x++ + 1; + return y + 3; + } +} diff --git a/tests/syntax/temporary_location.ml b/tests/syntax/temporary_location.ml new file mode 100644 index 0000000000000000000000000000000000000000..c6792bd916b11be0921473018addb73a3b3e714e --- /dev/null +++ b/tests/syntax/temporary_location.ml @@ -0,0 +1,18 @@ +open Cil_types + +class vis = object(_) + inherit Visitor.frama_c_inplace + + method! vvrbl vi = + Kernel.result "%s -> %a" vi.vname Printer.pp_location vi.vdecl; + Cil.DoChildren + +end + +let main () = + Ast.compute (); + Cil.visitCilFile (new vis :> Cil.cilVisitor) (Ast.get ()) + +let () = + Db.Main.extend main +